TY - GEN
T1 - On the revision problem of specification automata
AU - Kim, Kangjin
AU - Fainekos, Georgios
AU - Sankaranarayanan, Sriram
PY - 2012/1/1
Y1 - 2012/1/1
N2 - One of the important challenges in robotics is the automatic synthesis of provably correct controllers from high level specifications. One class of such algorithms operates in two steps: (i) high level discrete controller synthesis and (ii) low level continuous controller synthesis. In this class of algorithms, when phase (i) fails, then it is desirable to provide feedback to the designer in the form of revised specifications that can be achieved by the system. In this paper, we address the minimal revision problem for specification automata. That is, we construct automata specifications that are as "close" as possible to the initial user intent, by removing the minimum number of constraints from the specification that cannot be satisfied. We prove that the problem is computationally hard and we encode it as a satisfiability problem. Then, the minimal revision problem can be solved by utilizing efficient SAT solvers.
AB - One of the important challenges in robotics is the automatic synthesis of provably correct controllers from high level specifications. One class of such algorithms operates in two steps: (i) high level discrete controller synthesis and (ii) low level continuous controller synthesis. In this class of algorithms, when phase (i) fails, then it is desirable to provide feedback to the designer in the form of revised specifications that can be achieved by the system. In this paper, we address the minimal revision problem for specification automata. That is, we construct automata specifications that are as "close" as possible to the initial user intent, by removing the minimum number of constraints from the specification that cannot be satisfied. We prove that the problem is computationally hard and we encode it as a satisfiability problem. Then, the minimal revision problem can be solved by utilizing efficient SAT solvers.
UR - http://www.scopus.com/inward/record.url?scp=84864492195&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84864492195&partnerID=8YFLogxK
U2 - 10.1109/ICRA.2012.6224826
DO - 10.1109/ICRA.2012.6224826
M3 - Conference contribution
AN - SCOPUS:84864492195
SN - 9781467314039
T3 - Proceedings - IEEE International Conference on Robotics and Automation
SP - 5171
EP - 5176
BT - 2012 IEEE International Conference on Robotics and Automation, ICRA 2012
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2012 IEEE International Conference on Robotics and Automation, ICRA 2012
Y2 - 14 May 2012 through 18 May 2012
ER -