×

Fair termination for parameterized probabilistic concurrent systems. (English) Zbl 1452.68127

Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 499-517 (2017).
Summary: We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with \(n\) finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework for the parameterized verification of non-probabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework – often crucial for verifying termination – has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur and Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Herman’s protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fully-automatic method that can prove termination for these examples.
For the entire collection see [Zbl 1360.68015].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

PRISM; FAST
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

References:

[1] PRISM website (referred in July 2015). http://www.prismmodelchecker.org/
[2] Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158-174. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_14 · Zbl 1284.68337 · doi:10.1007/978-3-642-12002-2_14
[3] Abdulla, P.A.: Regular model checking. STTT 14(2), 109-118 (2012) · doi:10.1007/s10009-011-0216-8
[4] Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J., Saksena, M.: Regular model checking for LTL (MSO). STTT 14(2), 223-241 (2012) · doi:10.1007/s10009-011-0212-z
[5] Alur, R., Henzinger, T.A.: Finitary fairness. ACM Trans. Program. Lang. Syst. 20(6), 1171-1194 (1998) · doi:10.1145/295656.295659
[6] Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307-309 (1986) · doi:10.1016/0020-0190(86)90071-2
[7] Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076
[8] Baier, C., Kwiatkowska, M.Z.: On the verification of qualitative properties of probabilistic processes under fairness constraints. Inf. Process. Lett. 66(2), 71-79 (1998) · Zbl 1078.68664 · doi:10.1016/S0020-0190(98)00038-6
[9] Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. STTT 10(5), 401-424 (2008) · doi:10.1007/s10009-008-0064-3
[10] Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474-488. Springer, Heidelberg (2005). doi:10.1007/11562948_35 · Zbl 1170.68507 · doi:10.1007/11562948_35
[11] Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: FSTTCS 2013, LIPIcs, vol. 24, pp. 501-513. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013) · Zbl 1359.68185
[12] Boigelot, B., Herbreteau, F.: The power of hybrid acceleration. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 438-451. Springer, Heidelberg (2006). doi:10.1007/11817963_40 · Zbl 1188.68169 · doi:10.1007/11817963_40
[13] Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223-235. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_24 · Zbl 1278.68157 · doi:10.1007/978-3-540-45069-6_24
[14] Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: POPL 2013, pp. 457-468. ACM (2013) · Zbl 1301.68169
[15] Bonnet, R., Kiefer, S., Lin, A.W.: Analysis of probabilistic basic parallel processes. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 43-57. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54830-7_3 · Zbl 1405.68208 · doi:10.1007/978-3-642-54830-7_3
[16] Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular (tree) model checking. STTT 14(2), 167-191 (2012) · Zbl 1273.68221 · doi:10.1007/s10009-011-0205-y
[17] Cardelli, L., Csikász-Nagy, A.: The cell cycle switch computes approximate majority. Sci. Rep. 2(656) (2012)
[18] Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511-526. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_34 · doi:10.1007/978-3-642-39799-8_34
[19] Chakarov, A., Voronin, Y.-L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 260-279. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_15 · Zbl 1420.68153 · doi:10.1007/978-3-662-49674-9_15
[20] Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Form. Methods Syst. Des. 1(4), 385-415 (1992) · Zbl 0777.68045 · doi:10.1007/BF00709157
[21] Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 165-176. Springer, Heidelberg (1997). doi:10.1007/BFb0023457 · Zbl 1498.68155 · doi:10.1007/BFb0023457
[22] Esparza, J.: Parameterized verification of crowds of anonymous processes. Dependable Softw. Syst. Eng. 45, 59-71 (2016)
[23] Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123-138. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_14 · doi:10.1007/978-3-642-31424-7_14
[24] Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL 2015, pp. 489-501. ACM (2015) · Zbl 1345.68104
[25] Fokkink, W.: Distributed Algorithms. MIT Press, Cambridge (2013) · Zbl 1278.68003
[26] Francez, N.: Fairness. Springer, New York (1986) · Zbl 0602.68007 · doi:10.1007/978-1-4612-4886-6
[27] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2500. Springer, Heidelberg (2002). [Outcome of a Dagstuhl seminar, February 2001] · Zbl 1011.00037
[28] Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst. 5(3), 356-380 (1983) · Zbl 0511.68009 · doi:10.1145/2166.357214
[29] Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63-67 (1990) · Zbl 0697.68027 · doi:10.1016/0020-0190(90)90107-9
[30] Hoenicke, J., Olderog, E.-R., Podelski, A.: Fairness for dynamic control. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 251-265. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_20 · Zbl 1284.68400 · doi:10.1007/978-3-642-12002-2_20
[31] Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: PODC, pp. 119-131 (1990)
[32] Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 364-389. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1_15 · Zbl 1335.68058 · doi:10.1007/978-3-662-49498-1_15
[33] Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: LICS, p. 351 (2003)
[34] Lehmann, D., Rabin, M.: On the advantage of free choice: a symmetric and fully distributed solution to the dining philosophers problem (extended abstract). In: POPL, pp. 133-138 (1981)
[35] Lieberman, E., Hauert, C., Nowak, M.A.: Evolutionary dynamics on graphs. Nature 433(7023), 312-316 (2005) · doi:10.1038/nature03204
[36] Lin, A.W., Rümmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 112-133. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41540-6_7 · Zbl 1411.68075 · doi:10.1007/978-3-319-41540-6_7
[37] Lin, A.W.: Accelerating tree-automatic relations. In: FSTTCS, pp. 313-324 (2012) · Zbl 1354.68176
[38] Lynch, N.A., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: PODC, pp. 314-323 (1994) · Zbl 1373.68448
[39] Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 111-126. Springer, Heidelberg (2001). doi:10.1007/3-540-47764-0_7 · Zbl 0997.68515 · doi:10.1007/3-540-47764-0_7
[40] Moran, P.A.P.: Random processes in genetics. Math. Proc. Camb. Philos. Soc. 54(1), 60-71 (1958) · Zbl 0091.15701 · doi:10.1017/S0305004100033193
[41] Neider, D., Jansen, N.: Regular model checking using solver technologies and automata learning. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 16-31. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_2 · doi:10.1007/978-3-642-38088-4_2
[42] Nilsson, M.: Regular model checking. Ph.D. thesis, Uppsala Universitet (2005)
[43] Olderog, E.-R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM Trans. Program. Lang. Syst. 10(3), 420-455 (1988) · doi:10.1145/44501.44504
[44] Olderog, E.-R., Podelski, A.: Explicit fair scheduling for dynamic control. In: Dams, D., Hannemann, U., Steffen, M. (eds.) Concurrency, Compositionality, and Correctness. LNCS, vol. 5930, pp. 96-117. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11512-7_7 · Zbl 1274.68035 · doi:10.1007/978-3-642-11512-7_7
[45] Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53-72 (1986) · Zbl 0598.68019 · doi:10.1007/BF01843570
[46] To, A.W.: Model checking infinite-state systems: generic and specific approaches. Ph.D. thesis, LFCS, School of Informatics, University of Edinburgh (2010)
[47] To, A.W., Libkin, L.: Algorithmic metatheorems for decidable LTL model checking over infinite systems. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 221-236. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12032-9_16 · Zbl 1284.68416 · doi:10.1007/978-3-642-12032-9_16
[48] Vardi, M.
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.