2015
Controller Synthesis for MDPs and Frequency LTL\GU
FOREJT, Vojtěch, Jan KRČÁL a Jan KŘETÍNSKÝZákladní údaje
Originální název
Controller Synthesis for MDPs and Frequency LTL\GU
Autoři
FOREJT, Vojtěch (203 Česká republika, domácí), Jan KRČÁL (203 Česká republika) a Jan KŘETÍNSKÝ (203 Česká republika, domácí)
Vydání
Suva, Fiji, LPAR 2015, od s. 162-177, 16 s. 2015
Nakladatel
Springer
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Německo
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/15:00081286
Organizační jednotka
Fakulta informatiky
ISBN
978-3-662-48898-0
ISSN
UT WoS
000375574900012
Klíčová slova anglicky
frequency LTL; quantitative logics; MDP controller synthesis; automata characterization
Štítky
Změněno: 28. 4. 2016 15:33, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.
Návaznosti
| GBP202/12/G061, projekt VaV |
|