On Frequency LTL in Probabilistic Systems
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F15%3A00081289" target="_blank" >RIV/00216224:14330/15:00081289 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.184" target="_blank" >10.4230/LIPIcs.CONCUR.2015.184</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
On Frequency LTL in Probabilistic Systems
Popis výsledku v původním jazyce
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 usualG 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 byseveral 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.
Název v anglickém jazyce
On Frequency LTL in Probabilistic Systems
Popis výsledku anglicky
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 usualG 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 byseveral 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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2015
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
CONCUR 2015
ISBN
9783939897910
ISSN
1868-8969
e-ISSN
—
Počet stran výsledku
14
Strana od-do
184-197
Název nakladatele
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Místo vydání
Madrid, Spain
Místo konání akce
Madrid, Spain
Datum konání akce
1. 1. 2015
Typ akce podle státní příslušnosti
CST - Celostátní akce
Kód UT WoS článku
—