Controller synthesis for MDPs and frequency LTL\GU Conference Paper


Author(s): Forejt, Vojtěch; Krčál, Jan; Křetínský, Jan
Title: Controller synthesis for MDPs and frequency LTL\GU
Title Series: LNCS
Affiliation IST Austria
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.
Keywords: Controller synthesis; Markov Decision Processes; Deterministic automata; Probabilistic systems
Conference Title: LPAR: Logic for Programming, Artificial Intelligence, and Reasoning
Volume: 9450
Conference Dates: November 27-28, 2015
Conference Location: Suva, Fiji
ISBN: 978-3-642-45220-8
Publisher: Springer  
Date Published: 2015-11-22
Start Page: 162
End Page: 177
DOI: 10.1007/978-3-662-48899-7_12
Notes: 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).
Open access: no
IST Austria Authors
Related IST Austria Work