Forejt, Vojtěch ; Krčál, Jan ; Kretinsky, JanIST Austria
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.
This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).
162 - 177
LPAR: Logic for Programming, Artificial Intelligence, and Reasoning
2015-11-24 – 2015-11-28
Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12
Forejt, V., Krčál, J., & Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. https://doi.org/10.1007/978-3-662-48899-7_12
Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12.
V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.
Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450. 162–177.
Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU. Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.