Minimal counterexamples for linear-time probabilistic verification. (English) Zbl 1360.68604
Summary: Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time Markov chains and Markov decision processes as counterexamples for violated \(\omega\)-regular properties. Minimality can thereby be defined in terms of the number of states or transitions. This problem is known to be NP-complete for Markov decision processes. We show how to compute such subsystems using mixed integer linear programming and evaluate the practical applicability in a number of experiments. They show that our method yields substantially smaller counterexample than using existing techniques.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 60J20 | Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 90C11 | Mixed integer programming |
| 90C40 | Markov and semi-Markov decision processes |
Keywords:
Markov chain; Markov decision process; counterexample; \(\omega\)-regular property; mixed integer linear programming; SAT-modulo-theoriesReferences:
| [1] | Clarke, E. M., The birth of model checking, (25 Years of Model Checking—History, Achievements, Perspectives. 25 Years of Model Checking—History, Achievements, Perspectives, LNCS, vol. 5000 (2008), Springer), 1-26 · Zbl 1142.68046 |
| [2] | Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (Proc. of CAV. Proc. of CAV, LNCS, vol. 1855 (2000), Springer), 154-169 · Zbl 0974.68517 |
| [3] | Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 5, 752-794 (2003) · Zbl 1325.68145 |
| [4] | Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic CEGAR, (Proc. of CAV. Proc. of CAV, LNCS, vol. 5123 (2008), Springer), 162-175 · Zbl 1155.68438 |
| [5] | Chadha, R.; Viswanathan, M., A counterexample-guided abstraction-refinement framework for Markov decision processes, ACM Trans. Comput. Log., 12, 1, 1-45 (2010) · Zbl 1351.68154 |
| [6] | Clarke, E. M.; Veith, H., Counterexamples revisited: principles, algorithms, applications, (Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, LNCS, vol. 2772 (2003), Springer), 208-224 · Zbl 1274.68179 |
| [7] | Gastin, P.; Moro, P.; Zeitoun, M., Minimization of counterexamples in SPIN, (Proc. of SPIN. Proc. of SPIN, LNCS, vol. 2989 (2004), Springer), 92-108 · Zbl 1125.68369 |
| [8] | Clarke, E. M.; Grumberg, O.; McMillan, K. L.; Zhao, X., Efficient generation of counterexamples and witnesses in symbolic model checking, (Proc. of DAC (1995), IEEE Computer Society), 427-432 |
| [9] | Clarke, E. M.; Jha, S.; Lu, Y.; Veith, H., Tree-like counterexamples in model checking, (Proc. of LICS (2002), IEEE Computer Society), 19-29 |
| [10] | Busard, S.; Pecheur, C., Rich counter-examples for temporal-epistemic logic model checking, (Proc. of IWIGP. Proc. of IWIGP, EPTCS, vol. 78 (2012)), 39-53 |
| [11] | Schuppan, V.; Biere, A., Shortest counterexamples for symbolic model checking of LTL with past, (Proc. of TACAS. Proc. of TACAS, LNCS, vol. 3440 (2005), Springer), 493-509 · Zbl 1087.68060 |
| [12] | Fischer, M. J.; Lynch, N. A.; Paterson, M., Impossibility of distributed consensus with one faulty process, J. ACM, 32, 2, 374-382 (1985) · Zbl 0629.68027 |
| [13] | Bustan, D.; Rubin, S.; Vardi, M. Y., Verifying \(ω\)-regular properties of Markov chains, (Proc. of CAV. Proc. of CAV, LNCS, vol. 3114 (2004), Springer), 189-201 · Zbl 1103.68072 |
| [14] | Kretínský, J.; Esparza, J., Deterministic automata for the \((F, G)\)-fragment of LTL, (Proc. of CAV. Proc. of CAV, LNCS, vol. 7358 (2012), Springer: Springer Berkeley, CA, USA), 7-22 |
| [15] | Kwiatkowska, M. Z.; Norman, G.; Parker, D., Prism 4.0: verification of probabilistic real-time systems, (Proc. of CAV. Proc. of CAV, LNCS, vol. 6806 (2011), Springer), 585-591 |
| [16] | Ciesinski, F.; Baier, C., LIQuor: a tool for qualitative and quantitative linear time analysis of reactive systems, (Proc. of QEST (2006)), 131-132 |
| [17] | Katoen, J.-P.; Zapreev, I. S.; Hahn, E. M.; Hermanns, H.; Jansen, D. N., The ins and outs of the probabilistic model checker MRMC, Perform. Eval., 68, 2, 90-104 (2011) |
| [18] | Penna, G. D.; Intrigila, B.; Melatti, I.; Tronci, E.; Zilli, M. V., Finite horizon analysis of Markov chains with the Murphi verifier, Softw. Tools Technol. Transf., 8, 4-5, 397-409 (2006) |
| [19] | Kwiatkowska, M.; Norman, G.; Parker, D., The PRISM benchmark suite, (Proc. of QEST (2012), IEEE Computer Society), 203-204 |
| [20] | Han, T.; Katoen, J.-P.; Damman, B., Counterexample generation in probabilistic model checking, IEEE Trans. Softw. Eng., 35, 2, 241-257 (2009) |
| [21] | Wimmer, R.; Braitling, B.; Becker, B., Counterexample generation for discrete-time Markov chains using bounded model checking, (Proc. of VMCAI. Proc. of VMCAI, LNCS, vol. 5403 (2009), Springer), 366-380 · Zbl 1206.68195 |
| [22] | Andrés, M. E.; D’Argenio, P.; van Rossum, P., Significant diagnostic counterexamples in probabilistic model checking, (Proc. of HVC. Proc. of HVC, LNCS, vol. 5394 (2008), Springer), 129-148 |
| [23] | Günther, M.; Schuster, J.; Siegle, M., Symbolic calculation of \(k\)-shortest paths and related measures with the stochastic process algebra tool Caspa, (Proc. of DYADEM-FTS (2010), ACM Press), 13-18 |
| [24] | Komuravelli, A.; Pasareanu, C. S.; Clarke, E. M., Assume-guarantee abstraction refinement for probabilistic systems, (Proc. of CAV. Proc. of CAV, LNCS, vol. 7358 (2012), Springer), 310-326 |
| [25] | Komuravelli, A.; Pasareanu, C. S.; Clarke, E. M., Learning probabilistic systems from tree samples, (Proc. of LICS (2012), IEEE Computer Society), 441-450 · Zbl 1362.68122 |
| [26] | Kattenbelt, M.; Huth, M., Verification and refutation of probabilistic specifications via games, (Proc. of FSTTCS. Proc. of FSTTCS, LIPIcs, vol. 4 (2009), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 251-262 · Zbl 1248.68333 |
| [27] | Fecher, H.; Huth, M.; Piterman, N.; Wagner, D., PCTL model checking of Markov chains: truth and falsity as winning strategies in games, Perform. Eval., 67, 9, 858-872 (2010) |
| [28] | Aljazzar, H.; Leue, S., Directed explicit state-space search in the generation of counterexamples for stochastic model checking, IEEE Trans. Softw. Eng., 36, 1, 37-60 (2010) |
| [29] | Jansen, N.; Ábrahám, E.; Katelaan, J.; Wimmer, R.; Katoen, J.-P.; Becker, B., Hierarchical counterexamples for discrete-time Markov chains, (Proc. of ATVA. Proc. of ATVA, LNCS, vol. 6996 (2011), Springer), 443-452 · Zbl 1348.68139 |
| [30] | Aljazzar, H.; Leitner-Fischer, F.; Leue, S.; Simeonov, D., DiPro—a tool for probabilistic counterexample generation, (Proc. of SPIN. Proc. of SPIN, LNCS, vol. 6823 (2011), Springer), 183-187 |
| [31] | Jansen, N.; Ábrahám, E.; Volk, M.; Wimmer, R.; Katoen, J.-P.; Becker, B., The COMICS tool—computing minimal counterexamples for DTMCs, (Proc. of ATVA. Proc. of ATVA, LNCS, vol. 7561 (2012), Springer), 349-353 |
| [32] | Schmalz, M.; Varacca, D.; Völzer, H., Counterexamples in probabilistic LTL model checking for Markov chains, (Proc. of CONCUR. Proc. of CONCUR, LNCS, vol. 5710 (2009), Springer), 587-602 · Zbl 1254.68155 |
| [33] | de Moura, L. M.; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77 (2011) |
| [34] | Schrijver, A., Theory of Linear and Integer Programming (1986), Wiley · Zbl 0665.90063 |
| [35] | Wimmer, R.; Becker, B.; Jansen, N.; Ábrahám, E.; Katoen, J.-P., Minimal critical subsystems for discrete-time Markov models, (Proc. of TACAS. Proc. of TACAS, LNCS, vol. 7214 (2012), Springer), 299-314 · Zbl 1352.68167 |
| [36] | Wimmer, R.; Becker, B.; Jansen, N.; Ábrahám, E.; Katoen, J.-P., Minimal critical subsystems as counterexamples for \(ω\)-regular DTMC properties, (Proc. of MBMV (2012), Verlag Dr. Kovač), 169-180 |
| [37] | Norris, J. R., Markov Chains, Cambridge Series in Statistical Probabilistic Mathematics (1997), Cambridge University Press · Zbl 0873.60043 |
| [38] | Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), The MIT Press · Zbl 1179.68076 |
| [39] | Vardi, M. Y., Automatic verification of probabilistic concurrent finite-state programs, (Proc. of FOCS (1985), IEEE Computer Society), 327-338 |
| [40] | de Alfaro, L., Formal verification of probabilistic systems (1997), Stanford University, Ph.D. thesis |
| [41] | Vardi, M. Y., Probabilistic linear-time model checking: an overview of the automata-theoretic approach, (Proc. of ARTS. Proc. of ARTS, LNCS, vol. 1601 (1999), Springer), 265-276 |
| [42] | Couvreur, J.-M.; Saheb, N.; Sutre, G., An optimal automata approach to LTL model checking of probabilistic systems, (Proc. of LPAR. Proc. of LPAR, LNCS, vol. 2850 (2003), Springer), 361-375 · Zbl 1273.68224 |
| [43] | Safra, S., Complexity of automata on infinite objects (1989), The Weizmann Institute of Science: The Weizmann Institute of Science Rehovot, Israel, Ph.D. thesis |
| [44] | Tarjan, R. E., Depth-first search and linear graph algorithms, SIAM J. Comput., 1, 2, 146-160 (1972) · Zbl 0251.05107 |
| [45] | Dutertre, B.; de Moura, L. M., A fast linear-arithmetic solver for DPLL(T), (Proc. of CAV. Proc. of CAV, LNCS, vol. 4144 (2006), Springer), 81-94 |
| [46] | de Moura, L. M.; Bjørner, N., Z3: an efficient SMT solver, (Proc. of TACAS. Proc. of TACAS, LNCS, vol. 4963 (2008), Springer), 337-340 |
| [47] | Barrett, C.; Tinelli, C., CVC3, (Proc. of CAV. Proc. of CAV, LNCS, vol. 4590 (2007), Springer: Springer Berlin), 298-302 |
| [48] | Griggio, A., A practical approach to satisfiability modulo linear integer arithmetic, J. Satisf. Boolean Model. Comput., 8, 1-27 (2012) · Zbl 1331.68207 |
| [49] | Garey, M. R.; Johnson, D. S., Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), W.H. Freeman & Co Ltd. · Zbl 0411.68039 |
| [50] | Gurobi Optimization, Inc., Gurobi optimizer reference manual (2013) |
| [51] | Achterberg, T., SCIP: solving constraint integer programs, Math. Program. Comput., 1, 1, 1-41 (2009) · Zbl 1171.90476 |
| [52] | IBM CPLEX optimization studio, version 12.4 (2012) |
| [53] | Chatterjee, K.; Henzinger, M., Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification, (Proc. of SODA (2011), ACM Press), 1318-1336 · Zbl 1374.68272 |
| [54] | Pnueli, A., The temporal logic of programs, (Proc. of FOCS (1977), IEEE Computer Society), 46-57 |
| [55] | Klein, J.; Baier, C., Experiments with deterministic \(ω\)-automata for formulas of linear temporal logic, Theoret. Comput. Sci., 363, 2, 182-195 (2006) · Zbl 1153.03016 |
| [56] | Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (Proc. of CAV. Proc. of CAV, LNCS, vol. 2102 (2001), Springer), 53-65 · Zbl 0991.68044 |
| [57] | Aljazzar, H.; Leue, S., Extended directed search for probabilistic timed reachability, (Proc. of FORMATS. Proc. of FORMATS, LNCS, vol. 4202 (2006), Springer), 33-51 · Zbl 1141.68449 |
| [58] | Eppstein, D., Finding the \(k\) shortest paths, SIAM J. Comput., 28, 2, 652-673 (1998) · Zbl 0912.05057 |
| [59] | Aljazzar, H.; Leue, S., \(K^\ast \): a heuristic search algorithm for finding the \(k\) shortest paths, Artificial Intelligence, 175, 18, 2129-2154 (2011) · Zbl 1238.68148 |
| [60] | Aljazzar, H.; Kuntz, M.; Leitner-Fischer, F.; Leue, S., Directed and heuristic counterexample generation for probabilistic model checking—a comparative evaluation, (Proc. of QUOVADIS (2010), ACM Press), 25-32 |
| [61] | Itai, A.; Rodeh, M., Symmetry breaking in distributed networks, Inform. and Comput., 88, 1, 60-87 (1990) · Zbl 0705.68020 |
| [62] | Reiter, M. K.; Rubin, A. D., Crowds: anonymity for web transactions, ACM Trans. Inf. Syst. Sec., 1, 1, 66-92 (1998) |
| [63] | von Neumann, J., Probabilistic logics and synthesis of reliable organisms from unreliable components, (Automata Studies (1956), Princeton University Press), 43-98 |
| [64] | 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) |
| [65] | D’Argenio, P.; Jeannet, B.; Jensen, H.; Larsen, K., Reachability analysis of probabilistic systems by successive refinements, (Proc. of PAPM/PROBMIV. Proc. of PAPM/PROBMIV, LNCS, vol. 2165 (2001), Springer), 39-56 · Zbl 1007.68131 |
| [66] | D’Argenio, P. R.; Katoen, J.-P.; Ruys, T. C.; Tretmans, J., The bounded retransmission protocol must be on time!, (Proc. of TACAS. Proc. of TACAS, LNCS, vol. 1217 (1997), Springer), 416-431 |
| [67] | Aspnes, J.; Herlihy, M., Fast randomized consensus using shared memory, J. Algorithms, 15, 1, 441-460 (1990) · Zbl 0705.68016 |
| [68] | Kwiatkowska, M.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, Inform. and Comput., 205, 7, 1027-1077 (2007) · Zbl 1122.68075 |
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.
