Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
Parametric Markov chains have been introduced as a model for families of stochastic systems that rely on the same graph structure, but differ in the concrete transition probabilities. The latter are specified by polynomial constraints over a finite set of parameters. Important tasks in the analysis...
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Dokumenttyp: | Article (Journal) |
| Sprache: | Englisch |
| Veröffentlicht: |
2020
|
| In: |
Information and computation
Year: 2019, Jahrgang: 272, Pages: 104504 |
| ISSN: | 1090-2651 |
| DOI: | 10.1016/j.ic.2019.104504 |
| Online-Zugang: | Verlag, lizenzpflichtig, Volltext: https://doi.org/10.1016/j.ic.2019.104504 Verlag, lizenzpflichtig, Volltext: http://www.sciencedirect.com/science/article/pii/S0890540119301208 
|
| Verfasserangaben: | Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein |
MARC
| LEADER | 00000caa a2200000 c 4500 | ||
|---|---|---|---|
| 001 | 172668489X | ||
| 003 | DE-627 | ||
| 005 | 20220818172026.0 | ||
| 007 | cr uuu---uuuuu | ||
| 008 | 200810r20202019xx |||||o 00| ||eng c | ||
| 024 | 7 | |a 10.1016/j.ic.2019.104504 |2 doi | |
| 035 | |a (DE-627)172668489X | ||
| 035 | |a (DE-599)KXP172668489X | ||
| 035 | |a (OCoLC)1341354745 | ||
| 040 | |a DE-627 |b ger |c DE-627 |e rda | ||
| 041 | |a eng | ||
| 084 | |a 27 |2 sdnb | ||
| 100 | 1 | |a Baier, Christel |e VerfasserIn |0 (DE-588)12400301X |0 (DE-627)57713048X |0 (DE-576)293977097 |4 aut | |
| 245 | 1 | 0 | |a Parametric Markov chains |b PCTL complexity and fraction-free Gaussian elimination |c Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein |
| 264 | 1 | |c 2020 | |
| 336 | |a Text |b txt |2 rdacontent | ||
| 337 | |a Computermedien |b c |2 rdamedia | ||
| 338 | |a Online-Ressource |b cr |2 rdacarrier | ||
| 500 | |a Available online 16 december 2019 | ||
| 500 | |a Gesehen am 10.08.2020 | ||
| 520 | |a Parametric Markov chains have been introduced as a model for families of stochastic systems that rely on the same graph structure, but differ in the concrete transition probabilities. The latter are specified by polynomial constraints over a finite set of parameters. Important tasks in the analysis of parametric Markov chains are (1) computing closed-form solutions for reachability probabilities and other quantitative measures and (2) finding symbolic representations of the set of parameter valuations for which a given temporal logical formula holds as well as (3) the decision variant of (2) that asks whether there exists a parameter valuation where a temporal logical formula holds. Our contribution to (1) is to show that existing implementations for computing rational functions for reachability probabilities or expected costs in parametric Markov chains can be improved by using fraction-free Gaussian elimination, a long-known technique for linear equation systems with parametric coefficients. Our contribution to (2) and (3) is a complexity-theoretic discussion of the model-checking problem for parametric Markov chains and probabilistic computation tree logic (PCTL) formulas. We present an exponential-time algorithm for (2) and a PSPACE upper bound for (3). Moreover, we identify fragments of PCTL and subclasses of parametric Markov chains where (1) and (3) are solvable in polynomial time and establish NP-hardness for other PCTL fragments. | ||
| 534 | |c 2019 | ||
| 650 | 4 | |a Complexity | |
| 650 | 4 | |a Gaussian elimination | |
| 650 | 4 | |a Parametric Markov chain | |
| 650 | 4 | |a Parametric model checking | |
| 650 | 4 | |a PCTL | |
| 700 | 1 | |a Hensel, Christian |e VerfasserIn |4 aut | |
| 700 | 1 | |a Hutschenreiter, Lisa |e VerfasserIn |0 (DE-588)1215511388 |0 (DE-627)1726686280 |4 aut | |
| 700 | 1 | |a Junges, Sebastian |e VerfasserIn |4 aut | |
| 700 | 1 | |a Katoen, Joost-Pieter |e VerfasserIn |4 aut | |
| 700 | 1 | |a Klein, Joachim |e VerfasserIn |4 aut | |
| 773 | 0 | 8 | |i Enthalten in |t Information and computation |d Amsterdam : Elsevier, 1987 |g 272(2020), Seite 104504 |h Online-Ressource |w (DE-627)26688170X |w (DE-600)1468010-5 |w (DE-576)10337308X |x 1090-2651 |7 nnas |a Parametric Markov chains PCTL complexity and fraction-free Gaussian elimination |
| 773 | 1 | 8 | |g volume:272 |g year:2020 |g pages:104504 |a Parametric Markov chains PCTL complexity and fraction-free Gaussian elimination |
| 856 | 4 | 0 | |u https://doi.org/10.1016/j.ic.2019.104504 |x Verlag |x Resolving-System |z lizenzpflichtig |3 Volltext |
| 856 | 4 | 0 | |u http://www.sciencedirect.com/science/article/pii/S0890540119301208 |x Verlag |z lizenzpflichtig |3 Volltext |
| 951 | |a AR | ||
| 992 | |a 20200810 | ||
| 993 | |a Article | ||
| 994 | |a 2020 | ||
| 998 | |g 1215511388 |a Hutschenreiter, Lisa |m 1215511388:Hutschenreiter, Lisa |d 700000 |d 708070 |e 700000PH1215511388 |e 708070PH1215511388 |k 0/700000/ |k 1/700000/708070/ |p 3 | ||
| 999 | |a KXP-PPN172668489X |e 3737253927 | ||
| BIB | |a Y | ||
| SER | |a journal | ||
| JSO | |a {"name":{"displayForm":["Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein"]},"person":[{"family":"Baier","given":"Christel","display":"Baier, Christel","roleDisplay":"VerfasserIn","role":"aut"},{"family":"Hensel","given":"Christian","roleDisplay":"VerfasserIn","display":"Hensel, Christian","role":"aut"},{"given":"Lisa","family":"Hutschenreiter","role":"aut","display":"Hutschenreiter, Lisa","roleDisplay":"VerfasserIn"},{"role":"aut","roleDisplay":"VerfasserIn","display":"Junges, Sebastian","given":"Sebastian","family":"Junges"},{"family":"Katoen","given":"Joost-Pieter","display":"Katoen, Joost-Pieter","roleDisplay":"VerfasserIn","role":"aut"},{"roleDisplay":"VerfasserIn","display":"Klein, Joachim","role":"aut","family":"Klein","given":"Joachim"}],"origin":[{"dateIssuedKey":"2020","dateIssuedDisp":"2020"}],"title":[{"subtitle":"PCTL complexity and fraction-free Gaussian elimination","title":"Parametric Markov chains","title_sort":"Parametric Markov chains"}],"id":{"doi":["10.1016/j.ic.2019.104504"],"eki":["172668489X"]},"type":{"media":"Online-Ressource","bibl":"article-journal"},"note":["Available online 16 december 2019","Gesehen am 10.08.2020"],"relHost":[{"physDesc":[{"extent":"Online-Ressource"}],"id":{"issn":["1090-2651"],"eki":["26688170X"],"zdb":["1468010-5"]},"origin":[{"dateIssuedDisp":"1987-","publisher":"Elsevier ; Academic Press","dateIssuedKey":"1987","publisherPlace":"Amsterdam ; Orlando, Fla."}],"part":{"pages":"104504","year":"2020","volume":"272","text":"272(2020), Seite 104504"},"pubHistory":["72.1987 - 209.2011; Vol. 210.2012 -"],"language":["eng"],"recId":"26688170X","note":["Gesehen am 16.07.13"],"type":{"bibl":"periodical","media":"Online-Ressource"},"disp":"Parametric Markov chains PCTL complexity and fraction-free Gaussian eliminationInformation and computation","title":[{"title_sort":"Information and computation","title":"Information and computation"}]}],"language":["eng"],"recId":"172668489X"} | ||
| SRT | |a BAIERCHRISPARAMETRIC2020 | ||