Minimal specification revision for weighted transition systems

Kangjin Kim, Georgios Fainekos

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

4 Citations (Scopus)

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 publicationProceedings - IEEE International Conference on Robotics and Automation
Pages4068-4074
Number of pages7
DOIs
StatePublished - 2013
Event2013 IEEE International Conference on Robotics and Automation, ICRA 2013 - Karlsruhe, Germany
Duration: May 6 2013May 10 2013

Other

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

Fingerprint

Specifications
Temporal logic
Costs
Planning

ASJC Scopus subject areas

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

Cite this

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

Minimal specification revision for weighted transition systems. / Kim, Kangjin; Fainekos, Georgios.

Proceedings - IEEE International Conference on Robotics and Automation. 2013. p. 4068-4074 6631151.

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

Kim, K & Fainekos, G 2013, Minimal specification revision for weighted transition systems. in Proceedings - IEEE International Conference on Robotics and Automation., 6631151, pp. 4068-4074, 2013 IEEE International Conference on Robotics and Automation, ICRA 2013, Karlsruhe, Germany, 5/6/13. https://doi.org/10.1109/ICRA.2013.6631151
Kim K, Fainekos G. Minimal specification revision for weighted transition systems. In Proceedings - IEEE International Conference on Robotics and Automation. 2013. p. 4068-4074. 6631151 https://doi.org/10.1109/ICRA.2013.6631151
Kim, Kangjin ; Fainekos, Georgios. / Minimal specification revision for weighted transition systems. Proceedings - IEEE International Conference on Robotics and Automation. 2013. pp. 4068-4074
@inproceedings{66a9bc40e7004865b3b5eddd280b661a,
title = "Minimal specification revision for weighted transition systems",
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.",
author = "Kangjin Kim and Georgios Fainekos",
year = "2013",
doi = "10.1109/ICRA.2013.6631151",
language = "English (US)",
isbn = "9781467356411",
pages = "4068--4074",
booktitle = "Proceedings - IEEE International Conference on Robotics and Automation",

}

TY - GEN

T1 - Minimal specification revision for weighted transition systems

AU - Kim, Kangjin

AU - Fainekos, Georgios

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84887271556&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84887271556&partnerID=8YFLogxK

U2 - 10.1109/ICRA.2013.6631151

DO - 10.1109/ICRA.2013.6631151

M3 - Conference contribution

SN - 9781467356411

SP - 4068

EP - 4074

BT - Proceedings - IEEE International Conference on Robotics and Automation

ER -