TŮMOVÁ, Jana, Luis REYES CASTRO, Sertac KARAMAN, Emilio FRAZZOLI a Daniela RUS. Minimum-violation LTL Planning with Conflicting Specifications. In Proceedings of the American Control Conference. New York, (NY, USA): IEEE, 2013, s. 200-205. ISBN 978-1-4799-0177-7. Dostupné z: https://dx.doi.org/10.1109/ACC.2013.6579837.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Minimum-violation LTL Planning with Conflicting Specifications
Autoři TŮMOVÁ, Jana (203 Česká republika, garant, domácí), Luis REYES CASTRO (840 Spojené státy), Sertac KARAMAN (840 Spojené státy), Emilio FRAZZOLI (840 Spojené státy) a Daniela RUS (840 Spojené státy).
Vydání New York, (NY, USA), Proceedings of the American Control Conference, od s. 200-205, 6 s. 2013.
Nakladatel IEEE
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání paměťový nosič (CD, DVD, flash disk)
Kód RIV RIV/00216224:14330/13:00066721
Organizační jednotka Fakulta informatiky
ISBN 978-1-4799-0177-7
ISSN 0743-1619
Doi http://dx.doi.org/10.1109/ACC.2013.6579837
UT WoS 000327210200034
Klíčová slova anglicky formal methods; robotics; linear temporal logic; control strategy synthesis
Štítky firank_A
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 2. 2018 14:32.
Anotace
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.
Návaznosti
GAP202/11/0312, projekt VaVNázev: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
LH11065, projekt VaVNázev: Řízení a ověřování vlastností komplexních hybridních systémů (Akronym: Řízení a ověřování vlastností komplexních hybridní)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Řízení a ověřování vlastností komplexních hybridních systémů
MUNI/A/0760/2012, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 31. 7. 2024 00:20