Minimal specification revision for weighted transition systems

Kangjin Kim, Georgios Fainekos

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

4 Scopus citations

Abstract

In this paper, we study the problem of revising Linear Temporal Logic (LTL) formulas that capture specifications for optimal planning over weighted transition systems. Namely, it is assumed that the model of the system is a weighted finite state transition system. The LTL specification captures the system requirements which must be satisfied by a plan which costs less than a certain cost budget. If the cost bounds cannot be satisfied with the initial specification, then it is desirable to return to the user a specification that can be satisfied on the system within the desired cost budget. We prove that the specification revision problem for automata-based optimal planning is NP-complete. In order to provide exact solutions to the problem, we present an Integer Linear Program (ILP) and a Mixed-Integer Linear Program (MILP) formulation for different versions of the problem. Finally, we indicate that a Linear Program (LP) relaxation can compute fast approximations to the problem.

Original languageEnglish (US)
Title of host publication2013 IEEE International Conference on Robotics and Automation, ICRA 2013
Pages4068-4074
Number of pages7
DOIs
StatePublished - Nov 14 2013
Event2013 IEEE International Conference on Robotics and Automation, ICRA 2013 - Karlsruhe, Germany
Duration: May 6 2013May 10 2013

Publication series

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

Other

Other2013 IEEE International Conference on Robotics and Automation, ICRA 2013
CountryGermany
CityKarlsruhe
Period5/6/135/10/13

ASJC Scopus subject areas

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

Fingerprint Dive into the research topics of 'Minimal specification revision for weighted transition systems'. Together they form a unique fingerprint.

  • Cite this

    Kim, K., & Fainekos, G. (2013). Minimal specification revision for weighted transition systems. In 2013 IEEE International Conference on Robotics and Automation, ICRA 2013 (pp. 4068-4074). [6631151] (Proceedings - IEEE International Conference on Robotics and Automation). https://doi.org/10.1109/ICRA.2013.6631151