Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1319887,
author = {Forejt, Vojtěch and Krčál, Jan and Křetínský, Jan},
address = {Suva, Fiji},
booktitle = {LPAR 2015},
doi = {http://dx.doi.org/10.1007/978-3-662-48899-7_12},
keywords = {frequency LTL; quantitative logics; MDP controller synthesis; automata characterization},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Suva, Fiji},
isbn = {978-3-662-48898-0},
pages = {162-177},
publisher = {Springer},
title = {Controller Synthesis for MDPs and Frequency LTL\GU},
year = {2015}
}
TY - JOUR
ID - 1319887
AU - Forejt, Vojtěch - Krčál, Jan - Křetínský, Jan
PY - 2015
TI - Controller Synthesis for MDPs and Frequency LTL\GU
PB - Springer
CY - Suva, Fiji
SN - 9783662488980
KW - frequency LTL
KW - quantitative logics
KW - MDP controller synthesis
KW - automata characterization
N2 - 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.
ER -
FOREJT, Vojtěch, Jan KRČÁL and Jan KŘETÍNSKÝ. Controller Synthesis for MDPs and Frequency LTL$\backslash$GU. In \textit{LPAR 2015}. Suva, Fiji: Springer, 2015, p.~162-177. ISBN~978-3-662-48898-0. Available from: https://dx.doi.org/10.1007/978-3-662-48899-7\_{}12.
|
