@inproceedings{fed940d26b094e6298b2e35e944f9516,
title = "Controller synthesis for MDPS and frequency LTL\gu ",
abstract = "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.",
author = "Vojt{\v e}ch Forejt and Jan Kr{\v c}{\'a}l and Jan K{\v r}et{\'i}nsk{\'y}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2015.; 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 ; Conference date: 24-11-2015 Through 28-11-2015",
year = "2015",
doi = "10.1007/978-3-662-48899-7_12",
language = "English",
isbn = "9783662488980",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "162--177",
editor = "Andrei Voronkov and Ansgar Fehnker and Martin Davis and Annabelle McIver",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings",
}