On-the-fly model checking for extended action-based probabilistic operators

  • Radu MateescuEmail author
  • José Ignacio Requeno
SPIN 2016


The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data handling, and quantitative aspects. In this paper, we aim at facilitating the quantitative analysis of systems modeled as PTSs (Probabilistic Transition Systems) labeled by actions containing data values and probabilities. We propose a new regular probabilistic operator that specifies the probability measure of a path described by a generalized regular formula involving arbitrary computations on data values. This operator, which subsumes the Until operators of PCTL and their action-based counterparts, can provide useful quantitative information about paths having certain (e.g., peak) cost values. We integrated the regular probabilistic operator into MCL (Model Checking Language) and we devised an associated on-the-fly model checking method, based on a combined local resolution of linear and Boolean equation systems. We implemented the method in the EVALUATOR model checker of the CADP toolbox and experimented it on realistic PTSs modeling concurrent systems.


Probabilistic transition system Action-based probabilistic logic On-the-fly model checking 



This work was partially supported by the European project SENSATION (Self Energy-Supporting Autonomous Computation) FP7-318490. We are grateful to the anonymous referees for their constructive criticism and their valuable suggestions for improving the manuscript. We also thank Wendelin Serwe for providing the LNT descriptions of the mutual exclusion protocols.


  1. 1.
    Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)CrossRefGoogle Scholar
  2. 2.
    Amestoy, P., Duff, I.S., L’Excellent, J.-Y., Koster, J.: MUMPS: a general purpose distributed memory sparse solver. In: PARA’2000, LNCS, vol. 1947, pp. 121–130. Springer, Berlin (2000)Google Scholar
  3. 3.
    Andersen, H.R.: Model checking and Boolean graphs. TCS 126(1), 3–30 (1994)CrossRefzbMATHGoogle Scholar
  4. 4.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: CAV’96, LNCS, vol. 1102, pp. 269–276. Springer, Berlin (1996)Google Scholar
  5. 5.
    Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Softw. Eng. 33(4), 209–224 (2007)CrossRefGoogle Scholar
  6. 6.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(7), 1–18 (2003)zbMATHGoogle Scholar
  7. 7.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  8. 8.
    Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: VMCAI’04, LNCS, vol. 2937,pp. 44–57. Springer, Berlin (2004)Google Scholar
  9. 9.
    Bolze, R., Cappello, F., Caron, E., Daydé, M.J., Desprez, F., Jeannot, E., Jégou, Y., Lanteri, S., Leduc, J., Melab, N., Mornet, G., Namyst, R., Primet, P., Quétier, B., Richard, O., Talbi, E.-G., Touche, I.: Grid’5000: a large scale and highly reconfigurable experimental grid testbed. IJHPCA 20(4), 481–494 (2006)Google Scholar
  10. 10.
    Brzozowski, J.A.: Derivatives of regular expressions. JACM 11(4), 481–494 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference manual of the LNT to LOTOS translator (Version 6.2). Inria/Vasy and Inria/Convecs (2015)Google Scholar
  12. 12.
    Chua, L.O., Lin, P.M.: Computer Aided Analysis of Electronic Circuits. Prentice Hall, Englewood Cliffs (1975)zbMATHGoogle Scholar
  13. 13.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)CrossRefzbMATHGoogle Scholar
  14. 14.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  15. 15.
    Cleaveland, R., Iyer, S.P., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. TCS 342(2–3), 316–350 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. FMSD 2(2), 121–147 (1993)zbMATHGoogle Scholar
  17. 17.
    Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial gals designs. In: CAV’2009, LNCS, vol. 5643, pp. 204–218. Springer, Berlin (2009)Google Scholar
  18. 18.
    D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: PAPM/PROBMIV’01, LNCS, vol. 2165, pp. 39–56. Springer, Berlin (2001)Google Scholar
  19. 19.
    Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1), 69–115 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Concurrency, LNCS, vol. 469, pp. 407–419. Springer, Berlin (1990)CrossRefGoogle Scholar
  21. 21.
    Dijkstra, E.W.: Solution of a problem in concurrent programming control. CACM 8(9), 569 (1965)CrossRefGoogle Scholar
  22. 22.
    Duflot, M., Fribourg, L., Picaronny, C.: Randomized dining philosophers without fairness assumption. Distrib. Comput. 17(1), 65–76 (2004)CrossRefGoogle Scholar
  23. 23.
    Emerson, E.A., Lei, C-L.: Efficient model checking in fragments of the propositional mu-calculus. In: LICS’86, pp. 267–278. IEEE Press, New York (1986)Google Scholar
  24. 24.
    Feller, W.: An Introduction to Probability Theory and Its Applications. Wiley, New York (2001)zbMATHGoogle Scholar
  25. 25.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. JCSS 18(2), 194–211 (1979)MathSciNetzbMATHGoogle Scholar
  26. 26.
    Garavel, H.: OPEN/CAESAR: an open software architecture for verification, simulation, and testing. In: TACAS’98, LNCS, vol. 1384, pp. 68–84. Springer, Berlin. Full version available as INRIA Research Report RR-3352 (1998)Google Scholar
  27. 27.
    Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: FORTE’01, pp. 377–392. Kluwer, Dordrecht (2001)Google Scholar
  28. 28.
    Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)CrossRefzbMATHGoogle Scholar
  29. 29.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  30. 30.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137–161 (1985)CrossRefzbMATHGoogle Scholar
  31. 31.
    Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: IFM’00, LNCS, vol. 1945, pp. 420–439. Springer, Berlin (2000)Google Scholar
  32. 32.
    Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizating mutual exclusion. In: PODC’90, pp. 119–131. ACM Press, New York (1990)Google Scholar
  33. 33.
    Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 357–428. Academic Press, New York (1976)Google Scholar
  34. 34.
    Kozen, D.: Results on the propositional \(\mu \)-calculus. TCS 27, 333–354 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Kozen, D.: A probabilistic PDL. JCSS 30(2), 162–178 (1985)MathSciNetzbMATHGoogle Scholar
  36. 36.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV’2011, LNCS, vol. 6806, pp. 585–591. Springer, Berlin (2011)Google Scholar
  37. 37.
    Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987)CrossRefGoogle Scholar
  38. 38.
    Larsen, K.G.: Proof systems for Hennessy–Milner logic with recursion. In: CAAP’88, LNCS, vol. 299, pp. 215–230. Springer, Berlin (1988)Google Scholar
  39. 39.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Latella, D., Loreti, M., Massink, M.: On-the-fly fast mean-field model-checking. In: Trustworthy Global Computing, pp. 297–314. Springer, Berlin (2014)Google Scholar
  41. 41.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification, vol. I. Springer, New York (1992)CrossRefzbMATHGoogle Scholar
  42. 42.
    Mateescu, R.: Formal description and analysis of a bounded retransmission protocol. In: COST’96, University of Maribor, Slovenia (1996). Also available as INRIA Research Report RR-2965Google Scholar
  43. 43.
    Mateescu, R.: Caesar_solve: a generic library for on-the-fly resolution of alternation-free Boolean equation systems. STTT 8(1), 37–56 (2006)CrossRefGoogle Scholar
  44. 44.
    Mateescu, R., Monteiro, P.T., Dumas, E., de Jong, H.: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. TCS 412(26), 2854–2883 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  45. 45.
    Mateescu, R., Requeno, J.I.: On-the-fly model checking for extended action-based probabilistic operators. In: SPIN’2016, LNCS, vol. 9641, pp. 189–207. Springer, Berlin (2016)Google Scholar
  46. 46.
    Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. SCP 78(7), 843–861 (2013)Google Scholar
  47. 47.
    Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. SCP 46(3), 255–281 (2003)MathSciNetzbMATHGoogle Scholar
  48. 48.
    Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: FM’08, LNCS, vol. 5014, pp. 148–164. Springer, Berlin (2008)Google Scholar
  49. 49.
    Wolper, P.: Temporal logic can be more expressive. In: FOCS’81, pp. 340–348. IEEE Press, New York (1981)Google Scholar
  50. 50.
    van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIGGrenobleFrance
  2. 2.University of ZaragozaZaragozaSpain

Personalised recommendations