Minimum-violation LTL Planning with Conflicting Specifications

D 2013

Minimum-violation LTL Planning with Conflicting Specifications

TŮMOVÁ, Jana, Luis REYES CASTRO, Sertac KARAMAN, Emilio FRAZZOLI, Daniela RUS et. al.

Basic information

Original name

Minimum-violation LTL Planning with Conflicting Specifications

Authors

TŮMOVÁ, Jana (203 Czech Republic, guarantor, belonging to the institution), Luis REYES CASTRO (840 United States of America), Sertac KARAMAN (840 United States of America), Emilio FRAZZOLI (840 United States of America) and Daniela RUS (840 United States of America)

Edition

New York, (NY, USA), Proceedings of the American Control Conference, p. 200-205, 6 pp. 2013

Publisher

IEEE

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

storage medium (CD, DVD, flash disk)

RIV identification code

RIV/00216224:14330/13:00066721

Organization unit

Faculty of Informatics

ISBN

978-1-4799-0177-7

ISSN

DOI

http://dx.doi.org/10.1109/ACC.2013.6579837

UT WoS

000327210200034

Keywords in English

formal methods; robotics; linear temporal logic; control strategy synthesis

Abstract

V originále

We consider the problem of automatic generation of control strategies for robotic vehicles given a set of high-level mission specifications, such as "Vehicle x must eventually visit a target region and then return to a base," "Regions A and B must be periodically surveyed," or " None of the vehicles can enter an unsafe region." We focus on instances when all of the given specifications cannot be reached simultaneously due to their incompatibility and/or environmental constraints. We aim to find the least-violating control strategy while considering different priorities of satisfying different parts of the mission. Formally, we consider the missions given in the form of linear temporal logic formulas, each of which is assigned a reward that is earned when the formula is satisfied. Leveraging ideas from the automata-based model checking, we propose an algorithm for finding an optimal control strategy that maximizes the sum of rewards earned if this control strategy is applied. We demonstrate the proposed algorithm on an illustrative case study.

Links

GAP202/11/0312, research and development project

Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)

Investor: Czech Science Foundation

LH11065, research and development project

Name: Řízení a ověřování vlastností komplexních hybridních systémů (Acronym: Řízení a ověřování vlastností komplexních hybridní)

Investor: Ministry of Education, Youth and Sports of the CR

MUNI/A/0760/2012, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)

Investor: Masaryk University, Category A

Citovat

TŮMOVÁ, Jana, Luis REYES CASTRO, Sertac KARAMAN, Emilio FRAZZOLI and Daniela RUS. Minimum-violation LTL Planning with Conflicting Specifications. In Proceedings of the American Control Conference. New York, (NY, USA): IEEE, 2013, p. 200-205. ISBN 978-1-4799-0177-7. Available from: https://dx.doi.org/10.1109/ACC.2013.6579837.

@inproceedings{1139241,
   author = {Tůmová, Jana and Reyes Castro, Luis and Karaman, Sertac and Frazzoli, Emilio and Rus, Daniela},
   address = {New York, (NY, USA)},
   booktitle = {Proceedings of the American Control Conference},
   doi = {http://dx.doi.org/10.1109/ACC.2013.6579837},
   keywords = {formal methods; robotics; linear temporal logic; control strategy synthesis},
   howpublished = {paměťový nosič},
   language = {eng},
   location = {New York, (NY, USA)},
   isbn = {978-1-4799-0177-7},
   pages = {200-205},
   publisher = {IEEE},
   title = {Minimum-violation LTL Planning with Conflicting Specifications},
   year = {2013}
}

TY  - JOUR
ID  - 1139241
AU  - Tůmová, Jana - Reyes Castro, Luis - Karaman, Sertac - Frazzoli, Emilio - Rus, Daniela
PY  - 2013
TI  - Minimum-violation LTL Planning with Conflicting Specifications
PB  - IEEE
CY  - New York, (NY, USA)
SN  - 9781479901777
KW  - formal methods
KW  - robotics
KW  - linear temporal logic
KW  - control strategy synthesis
N2  - We consider the problem of automatic generation of control strategies for robotic vehicles given a set of high-level mission specifications, such as "Vehicle x must eventually visit a target region and then return to a base," "Regions A and B must be periodically surveyed," or " None of the vehicles can enter an unsafe region." We focus on instances when all of the given specifications cannot be reached simultaneously due to their incompatibility and/or environmental constraints. We aim to find the least-violating control strategy while considering different priorities of satisfying different parts of the mission. Formally, we consider the missions given in the form of linear temporal logic formulas, each of which is assigned a reward that is earned when the formula is satisfied. Leveraging ideas from the automata-based model checking, we propose an algorithm for finding an optimal control strategy that maximizes the sum of rewards earned if this control strategy is applied. We demonstrate the proposed algorithm on an illustrative case study.
ER  -

TŮMOVÁ, Jana, Luis REYES CASTRO, Sertac KARAMAN, Emilio FRAZZOLI and Daniela RUS. Minimum-violation LTL Planning with Conflicting Specifications. In \textit{Proceedings of the American Control Conference}. New York, (NY, USA): IEEE, 2013, p.~200-205. ISBN~978-1-4799-0177-7. Available from: https://dx.doi.org/10.1109/ACC.2013.6579837.

Detailed Information on Publication Record