| Identifikační kód | RIV/00216224:14330/15:00081289 |
|---|
| Název v anglickém jazyce | On Frequency LTL in Probabilistic Systems |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2015 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 2 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Vojtěch Forejt (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2477912)
Jan Krčál (státní příslušnost: CZ - Česká republika, vedidk: 9668780) |
|---|
| Popis výsledku v anglické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. |
|---|
| Klíčová slova oddělená středníkem | markov chains; markov decision processes; ltl; controller synthesis |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.4230/LIPIcs.CONCUR.2015.184 |
|---|