Reachability in parametric interval Markov chains using constraints. (English) Zbl 1400.68118
Summary: Parametric Interval Markov Chains (pIMCs) are a specification formalism that extend Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labelled with parametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate three semantics for IMCs: once-and-for-all, interval-Markov-decision-process, and at-every-step. In particular, we prove that all three semantics agree on the maximal/minimal reachability probabilities of a given IMC. We then investigate solutions to several parameter synthesis problems in the context of pIMCs – consistency, qualitative reachability and quantitative reachability – that rely on constraint encodings. Finally, we propose a prototype implementation of our constraint encodings with promising results.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
References:
| [1] | Whittaker, J. A.; Thomason, M. G., A Markov chain model for statistical software testing, IEEE Trans. Softw. Eng., 20, 10, 812-824, (1994) |
| [2] | Husmeier, D.; Dybowski, R.; Roberts, S., Probabilistic modeling in bioinformatics and medical informatics, (2010), Springer Publishing Company, Incorporated |
| [3] | Alur, R.; Henzinger, T. A.; Vardi, M. Y., Parametric real-time reasoning, (Symposium on Theory of Computing, (1993), ACM), 592-601 · Zbl 1310.68139 |
| [4] | Jonsson, B.; Larsen, K. G., Specification and refinement of probabilistic processes, (Symposium on Logic in Computer Science, (1991), IEEE), 266-277 |
| [5] | Chatterjee, K.; Sen, K.; Henzinger, T. A., Model-checking omega-regular properties of interval Markov chains, (International Conference on Foundations of Software Science and Computational Structures, Lecture Notes in Comput. Sci., vol. 4962, (2008), Springer), 302-317 · Zbl 1138.68441 |
| [6] | Sen, K.; Viswanathan, M.; Agha, G., Model-checking Markov chains in the presence of uncertainties, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Comput. Sci., vol. 3920, (2006), Springer Berlin, Heidelberg), 394-410 · Zbl 1180.68179 |
| [7] | Dehnert, C.; Junges, S.; Jansen, N.; Corzilius, F.; Volk, M.; Bruintjes, H.; Katoen, J.-P.; Ábrahám, E., Prophesy: a probabilistic parameter synthesis tool, (International Conference on Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 9207, (2015), Springer Cham), 214-231 |
| [8] | Hahn, E. M.; Hermanns, H.; Wachter, B.; Zhang, L., PARAM: a model checker for parametric Markov models, (International Conference on Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 6174, (2010), Springer), 660-664 |
| [9] | Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (International Conference on Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 6806, (2011), Springer), 585-591 |
| [10] | Chakraborty, S.; Katoen, J.-P., Model checking of open interval Markov chains, (International Conference on Analytical and Stochastic Modelling Techniques and Applications, Lecture Notes in Comput. Sci., vol. 9081, (2015), Springer Cham), 30-42 · Zbl 1392.68240 |
| [11] | Benedikt, M.; Lenhardt, R.; Worrell, J., LTL model checking of interval Markov chains, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Comput. Sci., vol. 7795, (2013), Springer), 32-46 · Zbl 1381.68147 |
| [12] | Delahaye, B.; Lime, D.; Petrucci, L., Parameter synthesis for parametric interval Markov chains, (International Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Comput. Sci., vol. 9583, (2016), Springer), 372-390 · Zbl 1475.68181 |
| [13] | Rossi, F.; van Beek, P.; Walsh, T., Handbook of constraint programming (foundations of artificial intelligence), (2006), Elsevier Science Inc. · Zbl 1175.90011 |
| [14] | Bart, A.; Delahaye, B.; Lime, D.; Monfroy, E.; Truchet, C., Reachability in parametric interval Markov chains using constraints, (International Conference on Quantitative Evaluation of Systems, Lecture Notes in Comput. Sci., vol. 10503, (2017), Springer), 173-189 · Zbl 1420.68152 |
| [15] | Vielma, J. P., Mixed integer linear programming formulation techniques, SIAM Rev., 57, 1, 3-57, (2015) · Zbl 1338.90277 |
| [16] | Barrett, C. W.; Sebastiani, R.; Seshia, S. A.; Tinelli, C., Satisfiability modulo theories, (Handbook of Satisfiability, vol. 185, (2009)), 825-885 |
| [17] | Baier, C.; Katoen, J.-P., Principles of model checking (representation and mind series), (2008), The MIT Press · Zbl 1179.68076 |
| [18] | Cantor, G., Über unendliche, lineare punktmannig faltigkeiten V, Math. Ann., 21, 545-591, (1883) · JFM 15.0452.03 |
| [19] | Wongpiromsarn, T.; Topcu, U.; Ozay, N.; Xu, H.; Murray, R. M., Tulip: a software toolbox for receding horizon temporal logic planning, (ACM International Conference on Hybrid Systems: Computation and Control, (2011), ACM), 313-314 |
| [20] | Puggelli, A.; Li, W.; Sangiovanni-Vincentelli, A. L.; Seshia, S. A., Polynomial-time verification of PCTL properties of MDPs with convex uncertainties, (International Conference on Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 8044, (2013), Springer), 527-542 · Zbl 1435.68202 |
| [21] | Delahaye, B., Consistency for parametric interval Markov chains, (International Workshop on Synthesis of Complex Parameters, OpenAccess Ser. Inform. (OASIcs), vol. 44, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 17-32 · Zbl 1429.68141 |
| [22] | Kwiatkowska, M.; Norman, G.; Parker, D., Probabilistic verification of Herman’s self-stabilisation algorithm, Form. Asp. Comput., 24, 4, 661-670, (2012) · Zbl 1259.68130 |
| [23] | Norman, G.; Shmatikov, V., Analysis of probabilistic contract signing, J. Comput. Secur., 14, 6, 561-589, (2006) |
| [24] | D’Argenio, P.; Jeannet, B.; Jensen, H.; Larsen, K., Reachability analysis of probabilistic systems by successive refinements, (Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, Lecture Notes in Comput. Sci., vol. 2165, (2001), Springer), 39-56 · Zbl 1007.68131 |
| [25] | Shmatikov, V., Probabilistic model checking of an anonymity system, J. Comput. Secur., 12, 3/4, 355-377, (2004) |
| [26] | Norman, G.; Parker, D.; Kwiatkowska, M.; Shukla, S., Evaluating the reliability of NAND multiplexing with PRISM, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 24, 10, 1629-1637, (2005) |
| [27] | Belotti, P.; Bonami, P.; Fischetti, M.; Lodi, A.; Monaci, M.; Nogales-Gómez, A.; Salvagnin, D., On handling indicator constraints in mixed integer programming, Comput. Optim. Appl., 1-22, (2016) |
| [28] | De Moura, L.; Bjørner, N., Z3: an efficient SMT solver, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Comput. Sci., (2008), Springer), 337-340 |
| [29] | IBM ILOG CPLEX Optimizer (Last 2010).; IBM ILOG CPLEX Optimizer (Last 2010). |
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.
