×

Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. (English) Zbl 1443.68101

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
60J10 Markov chains (discrete-time Markov processes on discrete state spaces)
68Q25 Analysis of algorithms and problem complexity
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Jonsson, B.; Larsen, K. G., Specification and refinement of probabilistic processes, (6th Annual Symposium on Logic in Computer Science (LICS) (1991), IEEE), 266-277
[2] Daws, C., Symbolic and parametric model checking of discrete-time Markov chains, (1st Int. Colloquium on Theoretical Aspects of Computing (ICTAC). 1st Int. Colloquium on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 3407 (2005), Springer), 280-294 · Zbl 1108.68497
[3] Lanotte, R.; Maggiolo-Schettini, A.; Troina, A., Parametric probabilistic transition systems for system design and analysis, Form. Asp. Comput., 19, 1, 93-109 (2007) · Zbl 1111.68084
[4] Hahn, E. M.; Hermanns, H.; Zhang, L., Probabilistic reachability for parametric Markov models, Int. J. Softw. Tools Technol. Transf., 13, 1, 3-19 (2011)
[5] Hahn, E. M.; Hermanns, H.; Wachter, B.; Zhang, L., PARAM: a model checker for parametric Markov models, (22nd Int. Conference on Computer Aided Verification (CAV). 22nd Int. Conference on Computer Aided Verification (CAV), LNCS, vol. 6174 (2010), Springer), 660-664
[6] Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (23rd Int. Conference on Computer Aided Verification (CAV). 23rd Int. Conference on Computer Aided Verification (CAV), LNCS, vol. 6806 (2011), Springer), 585-591
[7] Geddes, K. O.; Czapor, S. R.; Labahn, G., Algorithms for Computer Algebra (1993), Kluwer
[8] Dehnert, C.; Junges, S.; Katoen, J.-P.; Volk, M., A storm is coming: a modern probabilistic model checker, (29th Int. Conference on Computer Aided Verification (CAV). 29th Int. Conference on Computer Aided Verification (CAV), LNCS, vol. 10427 (2017), Springer), 592-600
[9] Jansen, N.; Corzilius, F.; Volk, M.; Wimmer, R.; Ábrahám, E.; Katoen, J.-P.; Becker, B., Accelerating parametric probabilistic verification, (11th Conference on Quantitative Evaluation of Systems (QEST). 11th Conference on Quantitative Evaluation of Systems (QEST), LNCS, vol. 8657 (2014), Springer), 404-420
[10] Bareiss, E. H., Computational solutions of matrix problems over an integral domain, IMA J. Appl. Math., 10, 1, 68-104 (1972) · Zbl 0241.65032
[11] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. Asp. Comput., 6, 5, 512-535 (1994) · Zbl 0820.68113
[12] Sen, K.; Viswanathan, M.; Agha, G., Model-checking Markov chains in the presence of uncertainties, (12th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 12th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3920 (2006), Springer), 394-410 · Zbl 1180.68179
[13] Chatterjee, K.; Sen, K.; Henzinger, T. A., Model-checking omega-regular properties of interval Markov chains, (11th Int. Conference on Foundations of Software Science and Computational Structures (FoSSaCS). 11th Int. Conference on Foundations of Software Science and Computational Structures (FoSSaCS), LNCS, vol. 4962 (2008), Springer), 302-317 · Zbl 1138.68441
[14] Hutschenreiter, L.; Baier, C.; Klein, J., Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, (8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF). 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), EPTCS, vol. 256 (2017)), 16-30 · Zbl 1483.68195
[15] McClellan, M. T., The exact solution of systems of linear equations with polynomial coefficients, J. Assoc. Comput. Mach., 20, 4, 563-588 (1973) · Zbl 0273.65030
[16] Kannan, R., Solving systems of linear equations over polynomials, Theor. Comput. Sci., 39, 69-88 (1985) · Zbl 0603.65024
[17] Sit, W. Y., An algorithm for solving parametric linear systems, J. Symb. Comput., 13, 4, 353-394 (1992) · Zbl 0752.34010
[18] Nakos, G.; Turner, P. R.; Williams, R. M., Fraction-free algorithms for linear and polynomial equations, ACM SIGSAM Bull., 31, 3, 11-19 (1997)
[19] Dehnert, C.; Junges, S.; Jansen, N.; Corzilius, F.; Volk, M.; Bruintjes, H.; Katoen, J.-P.; Ábrahám, E., PROPhESY: a probabilistic parameter synthesis tool, (27th Int. Conference on Computer Aided Verification (CAV). 27th Int. Conference on Computer Aided Verification (CAV), LNCS, vol. 9206 (2015), Springer), 214-231
[20] Filieri, A.; Ghezzi, C.; Tamburrelli, G., Run-time efficient probabilistic model checking, (33rd Int. Conference on Software Engineering (ICSE) (2011), ACM), 341-350
[21] Benedikt, M.; Lenhardt, R.; Worrell, J., LTL model checking of interval Markov chains, (19th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 19th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7795 (2013), Springer), 32-46 · Zbl 1381.68147
[22] Chonev, V., Reachability in augmented interval Markov chains, CoRR · Zbl 07121138
[23] Quatmann, T.; Dehnert, C.; Jansen, N.; Junges, S.; Katoen, J.-P., Parameter synthesis for Markov models: faster than ever, (14th Int. Symposium on Automated Technology for Verification and Analysis (ATVA). 14th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), LNCS, vol. 9938 (2016), Springer), 50-67 · Zbl 1398.68346
[24] Cubuktepe, M.; Jansen, N.; Junges, S.; Katoen, J.-P.; Papusha, I.; Poonawala, H. A.; Topcu, U., Sequential convex programming for the efficient verification of parametric MDPs, (TACAS (2). TACAS (2), LNCS, vol. 10206 (2017)), 133-150 · Zbl 1452.68117
[25] Kulkarni, V. G., Modeling and Analysis of Stochastic Systems (1995), Chapman & Hall · Zbl 0866.60004
[26] Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), The MIT Press · Zbl 1179.68076
[27] Ciesinski, F.; Baier, C.; Größer, M.; Klein, J., Reduction techniques for model checking Markov decision processes, (5th Int. Conference on Quantitative Evaluation of Systems (QEST) (2008), IEEE), 45-54
[28] Guennebaud, G.; Jacob, B., Eigen v3 (2010)
[29] Israeli, A.; Jalfon, M., Token management schemes and random walks yield self-stabilizing mutual exclusion, (9th ACM Symposium on Principles of Distributed Computing (PODC) (1990), ACM), 119-131
[30] Herman, T., Probabilistic self-stabilization, Inf. Process. Lett., 35, 2, 63-67 (1990) · Zbl 0697.68027
[31] Kwiatkowska, M. Z.; Norman, G.; Parker, D., Probabilistic verification of Herman’s self-stabilisation algorithm, Form. Asp. Comput., 24, 4-6, 661-670 (2012) · Zbl 1259.68130
[32] Aflaki, S.; Volk, M.; Bonakdarpour, B.; Katoen, J.-P.; Storjohann, A., Automated fine tuning of probabilistic self-stabilizing algorithms, (36th IEEE Symposium on Reliable Distributed Systems (SRDS) (2017), IEEE Computer Society), 94-103
[33] Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in Real Algebraic Geometry (2008), Springer
[34] Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, J. Comput. Syst. Sci., 32, 2, 251-264 (1986) · Zbl 0634.03031
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.