Forejt, Vojtech ;
Krcal, Jan
On Frequency LTL in Probabilistic Systems
Abstract
We study frequency lineartime temporal logic (fLTL) which extends the lineartime temporal logic (LTL) with a path operator G^p expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequencyrelated extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended "until" and "globally" operator, leading to undecidability of most interesting problems.
For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound p to be 1 and negations not to be outside any G^p operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.
BibTeX  Entry
@InProceedings{forejt_et_al:LIPIcs:2015:5378,
author = {Vojtech Forejt and Jan Krcal},
title = {{On Frequency LTL in Probabilistic Systems}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {184197},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897910},
ISSN = {18688969},
year = {2015},
volume = {42},
editor = {Luca Aceto and David de Frutos Escrig},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5378},
URN = {urn:nbn:de:0030drops53789},
doi = {10.4230/LIPIcs.CONCUR.2015.184},
annote = {Keywords: Markov chains, Markov decision processes, LTL, controller synthesis}
}
26.08.2015
Keywords: 

Markov chains, Markov decision processes, LTL, controller synthesis 
Seminar: 

26th International Conference on Concurrency Theory (CONCUR 2015)

Issue date: 

2015 
Date of publication: 

26.08.2015 