On the revision problem of specification automata

Kangjin Kim, Georgios Fainekos, Sriram Sankaranarayanan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication2012 IEEE International Conference on Robotics and Automation, ICRA 2012
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages5171-5176
Number of pages6
ISBN (Print)9781467314039
DOIs
StatePublished - 2012
Event 2012 IEEE International Conference on Robotics and Automation, ICRA 2012 - Saint Paul, MN, United States
Duration: May 14 2012May 18 2012

Publication series

NameProceedings - IEEE International Conference on Robotics and Automation
ISSN (Print)1050-4729

Conference

Conference 2012 IEEE International Conference on Robotics and Automation, ICRA 2012
Country/TerritoryUnited States
CitySaint Paul, MN
Period5/14/125/18/12

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence
  • Electrical and Electronic Engineering
  • Control and Systems Engineering

Fingerprint

Dive into the research topics of 'On the revision problem of specification automata'. Together they form a unique fingerprint.

Cite this