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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
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 0743-1619
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
Tags firank_A
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/2/2018 14:32.
Abstract
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 projectName: 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 projectName: Ří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 MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)
Investor: Masaryk University, Category A
PrintDisplayed: 26/8/2024 22:36