D 2013

Minimum-violation LTL Planning with Conflicting Specifications

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

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

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

DOI

UT WoS

000327210200034

Klíčová slova anglicky

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

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 28. 2. 2018 14:32, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GAP202/11/0312, projekt VaV
Ná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 VaV
Ná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 MU
Ná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