Identifikační kód | RIV/00216224:14330/13:00066721 |
Název v anglickém jazyce | Minimum-violation LTL Planning with Conflicting Specifications |
Druh | D - Článek ve sborníku |
Jazyk | eng - angličtina |
Obor - skupina | I - Informatika |
Obor | IN - Informatika |
Rok uplatnění | 2013 |
Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
Počet výskytů výsledku | 2 |
Počet tvůrců celkem | 5 |
Počet domácích tvůrců | 1 |
Výčet všech uvedených jednotlivých tvůrců | Jana Tůmová (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 4293738) Luis Reyes Castro (státní příslušnost: US - Spojené státy americké) Sertac Karaman (státní příslušnost: US - Spojené státy americké) Emilio Frazzoli (státní příslušnost: US - Spojené státy americké) Daniela Rus (státní příslušnost: US - Spojené státy americké) |
Popis výsledku v anglickém jazyce | 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. |
Klíčová slova oddělená středníkem | formal methods; robotics; linear temporal logic; control strategy synthesis |
Stránka www, na které se nachází výsledek | - |