J 2015

Optimal Temporal Logic Control for Deterministic Transition Systems with Probabilistic Penalties

SVOREŇOVÁ, Mária, Ivana ČERNÁ a Calin BELTA

Základní údaje

Originální název

Optimal Temporal Logic Control for Deterministic Transition Systems with Probabilistic Penalties

Autoři

SVOREŇOVÁ, Mária (703 Slovensko, domácí), Ivana ČERNÁ (203 Česká republika, garant, domácí) a Calin BELTA (840 Spojené státy)

Vydání

IEEE Transactions on Automatic Control, IEEE Control Systems Society, 2015, 0018-9286

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

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í

Impakt faktor

Impact factor: 2.777

Kód RIV

RIV/00216224:14330/15:00080609

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000355316200006

Klíčová slova anglicky

optimal control; linear temporal logic (LTL)

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 16. 7. 2018 15:56, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

We consider an optimal control problem for a weighted deterministic transition system required to satisfy a constraint expressed as a Linear Temporal Logic (LTL) formula over its labels. By assuming that the executions of the system incur time-varying penalties modeled as Markov chains, our goal is to minimize the expected average cumulative penalty incurred between consecutive satisfactions of a desired property. Using concepts from theoretical computer science, we provide two solutions to this problem. First, we derive a provably correct optimal strategy within the class of strategies that do not exploit values of penalties sensed in real time. Second, we show that by taking advantage of locally sensing the penalties, we can construct heuristic strategies leading to lower collected penalty. While still ensuring satisfaction of the LTL constraint, we cannot guarantee optimality in the latter case. We provide a user-friendly implementation of the proposed algorithms and analysis of two case studies.

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/1159/2014, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1206/2014, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty