×

Compositional probabilistic verification through multi-objective model checking. (English) Zbl 1277.68138

Summary: Compositional approaches to verification offer a powerful means to address the challenge of scalability. In this paper, we develop techniques for compositional verification of probabilistic systems based on the assume-guarantee paradigm. We target systems that exhibit both nondeterministic and stochastic behaviour, modelled as probabilistic automata, and augment these models with costs or rewards to reason about, for example, energy usage or performance metrics. Despite significant theoretical advances in compositional reasoning for probabilistic automata, there has been a distinct lack of practical progress regarding automated verification.
We propose a new assume-guarantee framework based on multi-objective probabilistic model checking which supports compositional verification for a range of quantitative properties, including probabilistic \(\omega\)-regular specifications and expected total cost or reward measures. We present a wide selection of assume-guarantee proof rules, including asymmetric, circular and asynchronous variants, and also show how to obtain numerical results in a compositional fashion. Given appropriate assumptions to be used in the proof rules, our compositional verification methods are, in contrast to previously proposed approaches, efficient and fully automated. Experimental results demonstrate their practical applicability on several large case studies, including instances where conventional probabilistic verification is infeasible.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68Q45 Formal languages and automata

Software:

LiQuor; ECDAR; PRISM
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bianco, A.; de Alfaro, L., Model checking of probabilistic and nondeterministic systems, (Thiagarajan, P., Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science. Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’95. Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science. Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’95, Lect. Notes Comput. Sci., vol. 1026 (1995), Springer), 499-513 · Zbl 1354.68167
[2] Courcoubetis, C.; Yannakakis, M., Markov decision processes and regular events, (Paterson, M., Proc. 17th International Colloquium on Automata, Languages and Programming. Proc. 17th International Colloquium on Automata, Languages and Programming, ICALP’90. Proc. 17th International Colloquium on Automata, Languages and Programming. Proc. 17th International Colloquium on Automata, Languages and Programming, ICALP’90, Lect. Notes Comput. Sci., vol. 443 (1990), Springer), 336-349 · Zbl 0765.68152
[3] de Alfaro, L., Formal verification of probabilistic systems (1997), Stanford University, PhD thesis
[4] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: Verification of probabilistic real-time systems, (Gopalakrishnan, G.; Qadeer, S., Proc. 23rd International Conference on Computer Aided Verification. Proc. 23rd International Conference on Computer Aided Verification, CAV’11. Proc. 23rd International Conference on Computer Aided Verification. Proc. 23rd International Conference on Computer Aided Verification, CAV’11, Lect. Notes Comput. Sci., vol. 6806 (2011), Springer), 585-591
[5] Ciesinski, F.; Baier, C., Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems, (Proc. 3rd International Conference on Quantitative Evaluation of Systems. Proc. 3rd International Conference on Quantitative Evaluation of Systems, QEST’06 (2006), IEEE CS Press), 131-132
[6] Jones, C., Tentative steps towards a development method for interfering programs, ACM Trans. Program. Lang. Syst., 5, 596-619 (1983) · Zbl 0517.68032
[7] Pasareanu, C.; Giannakopoulou, D.; Bobaru, M.; Cobleigh, J.; Barringer, H., Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning, Form. Methods Syst. Des., 32, 175-205 (2008) · Zbl 1147.68053
[8] Segala, R., Modelling and verification of randomized distributed real time systems (1995), Massachusetts Institute of Technology, PhD thesis
[9] Segala, R.; Lynch, N., Probabilistic simulations for probabilistic processes, Nord. J. Comput., 2, 250-273 (1995) · Zbl 0839.68067
[10] Pogosyants, A.; Segala, R.; Lynch, N., Verification of the randomized consensus algorithm of Aspnes and Herlihy: A case study, Distrib. Comput., 13, 155-186 (2000) · Zbl 1448.68156
[11] Segala, R., A compositional trace-based semantics for probabilistic automata, (Lee, I.; Smolka, S., Proc. 6th International Conference on Concurrency Theory. Proc. 6th International Conference on Concurrency Theory, CONCUR’95. Proc. 6th International Conference on Concurrency Theory. Proc. 6th International Conference on Concurrency Theory, CONCUR’95, Lect. Notes Comput. Sci., vol. 962 (1995), Springer), 234-248
[12] de Alfaro, L.; Henzinger, T.; Jhala, R., Compositional methods for probabilistic systems, (Larsen, K.; Nielsen, M., Proc. 12th International Conference on Concurrency Theory. Proc. 12th International Conference on Concurrency Theory, CONCUR’01. Proc. 12th International Conference on Concurrency Theory. Proc. 12th International Conference on Concurrency Theory, CONCUR’01, Lect. Notes Comput. Sci., vol. 2154 (2001), Springer), 351-365 · Zbl 1006.68083
[13] Cheung, L.; Lynch, N.; Segala, R.; Vaandrager, F., Switched probabilistic I/O automata, (Proc. 1st International Colloquium on Theoretical Aspects of Computing. Proc. 1st International Colloquium on Theoretical Aspects of Computing, ICTAC’04. Proc. 1st International Colloquium on Theoretical Aspects of Computing. Proc. 1st International Colloquium on Theoretical Aspects of Computing, ICTAC’04, Lect. Notes Comput. Sci., vol. 3407 (2004), Springer), 494-510 · Zbl 1109.68053
[14] Etessami, K.; Kwiatkowska, M.; Vardi, M.; Yannakakis, M., Multi-objective model checking of Markov decision processes, Log. Methods Comput. Sci., 4, 1-21 (2008) · Zbl 1161.68565
[15] Forejt, V.; Kwiatkowska, M.; Norman, G.; Parker, D.; Qu, H., Quantitative multi-objective verification for probabilistic systems, (Abdulla, P.; Leino, K., Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’11. Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’11, Lect. Notes Comput. Sci., vol. 6605 (2011), Springer), 112-127 · Zbl 1315.68177
[16] Alur, R.; Henzinger, T., Reactive modules, (Proc. 11th Annual IEEE Symposium on Logic in Computer Science. Proc. 11th Annual IEEE Symposium on Logic in Computer Science, LICS’96 (1996), IEEE CS Press), 207-218
[17] Kwiatkowska, M.; Norman, G.; Parker, D.; Qu, H., Assume-guarantee verification for probabilistic systems, (Esparza, J.; Majumdar, R., Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’10. Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’10, Lect. Notes Comput. Sci., vol. 6105 (2010), Springer), 23-37 · Zbl 1284.68406
[18] Etessami, K.; Kwiatkowska, M.; Vardi, M.; Yannakakis, M., Multi-objective model checking of Markov decision processes, (Grumberg, O.; Huth, M., Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’07. Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’07, Lect. Notes Comput. Sci., vol. 4424 (2007), Springer), 50-65 · Zbl 1186.68286
[19] Feng, L.; Kwiatkowska, M.; Parker, D., Compositional verification of probabilistic systems using learning, (Proc. 7th International Conference on Quantitative Evaluation of SysTems. Proc. 7th International Conference on Quantitative Evaluation of SysTems, QEST’10 (2010), IEEE CS Press), 133-142
[20] Feng, L.; Kwiatkowska, M.; Parker, D., Automated learning of probabilistic assumptions for compositional reasoning, (Giannakopoulou, D.; Orejas, F., Proc. 14th International Conference on Fundamental Approaches to Software Engineering. Proc. 14th International Conference on Fundamental Approaches to Software Engineering, FASE’11. Proc. 14th International Conference on Fundamental Approaches to Software Engineering. Proc. 14th International Conference on Fundamental Approaches to Software Engineering, FASE’11, Lect. Notes Comput. Sci., vol. 6603 (2011), Springer), 2-17
[21] Komuravelli, A.; Pasareanu, C.; Clarke, E., Assume-guarantee abstraction refinement for probabilistic systems, (Madhusudan, P.; Seshia, S., Proc. 24th International Conference on Computer Aided Verification. Proc. 24th International Conference on Computer Aided Verification, CAV’12. Proc. 24th International Conference on Computer Aided Verification. Proc. 24th International Conference on Computer Aided Verification, CAV’12, Lect. Notes Comput. Sci., vol. 7358 (2012), Springer), 310-326
[22] Kumar, J. A.; Vasudevan, S., Automatic compositional reasoning for probabilistic model checking of hardware designs, (Proc. 7th International Conference on Quantitative Evaluation of SysTems. Proc. 7th International Conference on Quantitative Evaluation of SysTems, QEST’10 (2010), IEEE CS Press), 143-152
[23] Delahaye, B.; Caillaud, B.; Legay, A., Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems, (Proc. 10th International Conference on Application of Concurrency to System Design. Proc. 10th International Conference on Application of Concurrency to System Design, ACSD’10 (2010), IEEE CS Press), 223-232
[24] Chatterjee, K.; de Alfaro, L.; Faella, M.; Henzinger, T.; Majumdar, R.; Stoelinga, M., Compositional quantitative reasoning, (Proc. 3rd International Conference on Quantitative Evaluation of Systems. Proc. 3rd International Conference on Quantitative Evaluation of Systems, QEST’06 (2006), IEEE CS Press), 179-188
[25] David, A.; Larsen, K. G.; Legay, A.; Nyman, U.; Wasowski, A., ECDAR: An environment for compositional design and analysis of real time systems, (Bouajjani, A.; Chin, W.-N., Proc. 8th International Symposium on Automated Technology for Verification and Analysis. Proc. 8th International Symposium on Automated Technology for Verification and Analysis, ATVA’10. Proc. 8th International Symposium on Automated Technology for Verification and Analysis. Proc. 8th International Symposium on Automated Technology for Verification and Analysis, ATVA’10, Lect. Notes Comput. Sci., vol. 6252 (2010), Springer), 365-370
[26] Kemeny, J.; Snell, J.; Knapp, A., Denumerable Markov Chains (1976), Springer · Zbl 0348.60090
[27] Thomas, W., Automata on infinite objects, (van Leeuwen, J., Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics (1990), Elsevier), 133-192 · Zbl 0900.68316
[28] Forejt, V.; Kwiatkowska, M.; Norman, G.; Parker, D., Automated verification techniques for probabilistic systems, (Bernardo, M.; Issarny, V., Formal Methods for Eternal Networked Software Systems. Formal Methods for Eternal Networked Software Systems, SFM’11. Formal Methods for Eternal Networked Software Systems. Formal Methods for Eternal Networked Software Systems, SFM’11, Lect. Notes Comput. Sci., vol. 6659 (2011), Springer), 53-113
[29] Kwiatkowska, M.; Norman, G.; Parker, D.; Sproston, J., Performance analysis of probabilistic timed automata using digital clocks, Form. Methods Syst. Des., 29, 33-78 (2006) · Zbl 1105.68063
[30] Courcoubetis, C.; Yannakakis, M., Markov decision processes and regular events, IEEE Trans. Autom. Control, 43, 1399-1418 (1998) · Zbl 0954.90061
[31] Puterman, M., Markov Decision Processes: Discrete Stochastic Dynamic Programming (1994), John Wiley and Sons · Zbl 0829.90134
[32] Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), MIT Press
[33] Forejt, V.; Kwiatkowska, M.; Parker, D., Pareto curves for probabilistic model checking, (Chakraborty, S.; Mukund, M., Proc. 10th International Symposium on Automated Technology for Verification and Analysis. Proc. 10th International Symposium on Automated Technology for Verification and Analysis, ATVA’12. Proc. 10th International Symposium on Automated Technology for Verification and Analysis. Proc. 10th International Symposium on Automated Technology for Verification and Analysis, ATVA’12, Lect. Notes Comput. Sci., vol. 7561 (2012), Springer), 317-332 · Zbl 1374.68285
[34] Baier, C.; Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness, Distrib. Comput., 11, 125-155 (1998) · Zbl 1448.68285
[35] Baier, C.; Größer, M.; Ciesinski, F., Quantitative analysis under fairness constraints, (Proc. 7th International Symposium on Automated Technology for Verification and Analysis. Proc. 7th International Symposium on Automated Technology for Verification and Analysis, ATVA’09. Proc. 7th International Symposium on Automated Technology for Verification and Analysis. Proc. 7th International Symposium on Automated Technology for Verification and Analysis, ATVA’09, Lect. Notes Comput. Sci., vol. 5799 (2009), Springer), 135-150 · Zbl 1262.68102
[36] Hansen, H.; Kwiatkowska, M.; Qu, H., Partial order reduction for model checking Markov decision processes under unconditional fairness, (Proc. 8th International Conference on Quantitative Evaluation of SysTems. Proc. 8th International Conference on Quantitative Evaluation of SysTems, QEST’11 (2011), IEEE CS Press), 203-212
[37] Hahn, E. M.; Hermanns, H.; Zhang, L., Probabilistic reachability for parametric Markov models, Int. J. Softw. Tools Technol. Transf., 13, 3-19 (2011)
[38] Chen, T.; Hahn, E. M.; Han, T.; Kwiatkowska, M.; Qu, H.; Zhang, L., Model repair for Markov decision processes, (Proc. 7th International Symposium on Theoretical Aspects of Software Engineering. Proc. 7th International Symposium on Theoretical Aspects of Software Engineering, TASE’13 (2013), IEEE CS Press), 85-92
[39] Aspnes, J.; Herlihy, M., Fast randomized consensus using shared memory, J. Algorithms, 15, 441-460 (1990) · Zbl 0705.68016
[40] (2013)
[41] Kwiatkowska, M.; Norman, G.; Segala, R., Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM, (Berry, G.; Comon, H.; Finkel, A., Proc. 13th International Conference on Computer Aided Verification. Proc. 13th International Conference on Computer Aided Verification, CAV’01. Proc. 13th International Conference on Computer Aided Verification. Proc. 13th International Conference on Computer Aided Verification, CAV’01, Lect. Notes Comput. Sci., vol. 2102 (2001), Springer), 194-206 · Zbl 0991.68503
[42] Cheshire, S.; Adoba, B.; Gutterman, E., Dynamic configuration of IPv4 link local addresses (2005), available from
[43] Farzan, A.; Chen, Y.-F.; Clarke, E.; Tsay, Y.-K.; Wang, B.-Y., Extending automated compositional verification to the full class of omega-regular languages, (Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08. Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08, Lect. Notes Comput. Sci., vol. 4963 (2008), Springer), 2-17 · Zbl 1134.68406
[45] Hermanns, H., Interactive Markov Chains and the Quest for Quantified Quality, Lect. Notes Comput. Sci., vol. 2428 (2002), Springer · Zbl 1012.68142
[46] Eisentraut, C.; Hermanns, H.; Zhang, L., On probabilistic automata in continuous time, (Proc. 25th Annual IEEE Symposium on Logic in Computer Science. Proc. 25th Annual IEEE Symposium on Logic in Computer Science, LICS’10 (2010), IEEE CS Press), 342-351
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.