| Identifikační kód | RIV/00216224:14330/15:00081286 |
|---|
| Název v anglickém jazyce | Controller Synthesis for MDPs and Frequency LTLGU |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2015 |
|---|
| 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 | 1 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 2 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Vojtěch Forejt (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2477912)
Jan Krčál (státní příslušnost: CZ - Česká republika, vedidk: 9668780)
Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054) |
|---|
| Popis výsledku v anglickém jazyce | 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 are1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTLGU, 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 formulaeinto equivalent deterministic automata. |
|---|
| Klíčová slova oddělená středníkem | frequency LTL; quantitative logics; MDP controller synthesis; automata characterization |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-662-48899-7_12 |
|---|