2015
Controller Synthesis for MDPs and Frequency LTL\GU
FOREJT, Vojtěch; Jan KRČÁL and Jan KŘETÍNSKÝBasic information
Original name
Controller Synthesis for MDPs and Frequency LTL\GU
Authors
FOREJT, Vojtěch (203 Czech Republic, belonging to the institution); Jan KRČÁL (203 Czech Republic) and Jan KŘETÍNSKÝ (203 Czech Republic, belonging to the institution)
Edition
Suva, Fiji, LPAR 2015, p. 162-177, 16 pp. 2015
Publisher
Springer
Other information
Language
English
Type of outcome
Proceedings paper
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
is not subject to a state or trade secret
Publication form
printed version "print"
Impact factor
Impact factor: 0.402 in 2005
RIV identification code
RIV/00216224:14330/15:00081286
Organization unit
Faculty of Informatics
ISBN
978-3-662-48898-0
ISSN
UT WoS
000375574900012
EID Scopus
2-s2.0-84952685457
Keywords in English
frequency LTL; quantitative logics; MDP controller synthesis; automata characterization
Tags
Changed: 28/4/2016 15:33, RNDr. Pavel Šmerk, Ph.D.
Abstract
In the original language
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.
Links
| GBP202/12/G061, research and development project |
|