On Frequency LTL in Probabilistic Systems

D 2015

On Frequency LTL in Probabilistic Systems

FOREJT, Vojtěch a Jan KRČÁL

Základní údaje

Originální název

On Frequency LTL in Probabilistic Systems

Autoři

FOREJT, Vojtěch (203 Česká republika, domácí) a Jan KRČÁL (203 Česká republika)

Vydání

Madrid, Spain, CONCUR 2015, od s. 184-197, 14 s. 2015

Nakladatel

Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/15:00081289

Organizační jednotka

Fakulta informatiky

ISBN

978-3-939897-91-0

ISSN

DOI

http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184

Klíčová slova anglicky

markov chains; markov decision processes; ltl; controller synthesis

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2016 15:33, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We study frequency linear-time temporal logic (fLTL) which extends the linear-time 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. Frequency-related 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.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

Citovat

FOREJT, Vojtěch a Jan KRČÁL. On Frequency LTL in Probabilistic Systems. Online. In CONCUR 2015. Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015, s. 184-197. ISBN 978-3-939897-91-0. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184.

@inproceedings{1319891,
   author = {Forejt, Vojtěch and Krčál, Jan},
   address = {Madrid, Spain},
   booktitle = {CONCUR 2015},
   doi = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184},
   keywords = {markov chains; markov decision processes; ltl; controller synthesis},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Madrid, Spain},
   isbn = {978-3-939897-91-0},
   pages = {184-197},
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
   title = {On Frequency LTL in Probabilistic Systems},
   year = {2015}
}

TY  - JOUR
ID  - 1319891
AU  - Forejt, Vojtěch - Krčál, Jan
PY  - 2015
TI  - On Frequency LTL in Probabilistic Systems
PB  - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
CY  - Madrid, Spain
SN  - 9783939897910
KW  - markov chains
KW  - markov decision processes
KW  - ltl
KW  - controller synthesis
N2  - We study frequency linear-time temporal logic (fLTL) which extends the linear-time 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. Frequency-related 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.
ER  -

FOREJT, Vojtěch a Jan KRČÁL. On Frequency LTL in Probabilistic Systems. Online. In \textit{CONCUR 2015}. Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015, s.~184-197. ISBN~978-3-939897-91-0. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184.

Podrobný výpis o publikaci