An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties

  • Yong Li
  • Wanwei Liu
  • Andrea TurriniEmail author
  • Ernst Moritz Hahn
  • Lijun Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


In this paper, we propose an efficient algorithm for the parameter synthesis of PLTL formulas with respect to parametric Markov chains. The PLTL formula is translated to an almost fully partitioned Büchi automaton which is then composed with the parametric Markov chain. We then reduce the problem to solving an optimisation problem, allowing to decide the satisfaction of the formula using an SMT solver. The algorithm works also for interval Markov chains. The complexity is linear in the size of the Markov chain, and exponential in the size of the formula. We provide a prototype and show the efficiency of our approach on a number of benchmarks.


Markov Chain Model Check Markov Chain Model Product Graph Strongly Connect Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



This work is supported by the CDZ project CAP (GZ 1023), by the Chinese Academy of Sciences Fellowship for International Young Scientists, by the National Natural Science Foundation of China (Grants No. 61532019, 61472473, 61550110249, 61550110506, 61103012, 61379054, and 61272335), and by the CAS/SAFEA International Partnership Program for Creative Research Teams.


  1. 1.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  2. 2.
    Baier, C., Kiefer, S., Klein, J., Klüppelholz, S., Müller, D., Worrell, J.: Markov chains and unambiguous Büchi automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 23–42. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-41528-4_2 Google Scholar
  3. 3.
    Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-36742-7_3 CrossRefGoogle Scholar
  4. 4.
    Bianco, A., Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995). doi: 10.1007/3-540-60692-0_70 CrossRefGoogle Scholar
  5. 5.
    Bustan, D., Rubin, S., Vardi, M.Y.: Verifying \(\omega \)-regular properties of Markov chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 189–201. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27813-9_15 CrossRefGoogle Scholar
  6. 6.
    Carton, O., Michel, M.: Unambiguous Büchi automata. TCS 297(1–3), 37–81 (2003)CrossRefzbMATHGoogle Scholar
  7. 7.
    Chatterjee, K., Gaiser, A., Křetínský, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559–575. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_37 CrossRefGoogle Scholar
  8. 8.
    Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking \(\omega \)-regular properties of interval Markov chains. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78499-9_22 CrossRefGoogle Scholar
  9. 9.
    Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131–132 (2006)Google Scholar
  10. 10.
    Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1–26. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-69850-0_1 CrossRefGoogle Scholar
  11. 11.
    Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994). doi: 10.1007/3-540-58179-0_72 CrossRefGoogle Scholar
  12. 12.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)CrossRefGoogle Scholar
  13. 13.
    Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Couvreur, J.-M., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 361–375. Springer, Heidelberg (2003). doi: 10.1007/978-3-540-39813-4_26 CrossRefGoogle Scholar
  15. 15.
    D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001). doi: 10.1007/3-540-44804-7_3 CrossRefGoogle Scholar
  16. 16.
    Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  17. 17.
    Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., Ábrahám, E.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214–231. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-21690-4_13 CrossRefGoogle Scholar
  18. 18.
    Esparza, J., Křetínský, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192–208. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-08867-9_13 Google Scholar
  19. 19.
    Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6), 637–647 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2011)CrossRefGoogle Scholar
  21. 21.
    Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: IscasMC: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-06410-9_22 CrossRefGoogle Scholar
  22. 22.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6(5), 512–535 (1994)zbMATHGoogle Scholar
  23. 23.
    Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127–165. Springer, Heidelberg (1994). doi: 10.1007/3-540-58085-9_75 CrossRefGoogle Scholar
  24. 24.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277 (1991)Google Scholar
  25. 25.
    Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81(4), 356–389 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    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)CrossRefGoogle Scholar
  27. 27.
    Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. D. Van Nostrand Company, New York (1966)zbMATHGoogle Scholar
  28. 28.
    Kini, D., Viswanathan, M.: Limit deterministic and probabilistic automata for LTL\(\setminus \)GU. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 628–642. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46681-0_57 Google Scholar
  29. 29.
    Klein, J., Baier, C.: On-the-Fly Stuttering in the Construction of Deterministic \(\omega \)-Automata. In: Holub, J., Žd’árek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51–61. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-76336-9_7 CrossRefGoogle Scholar
  30. 30.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_47 CrossRefGoogle Scholar
  31. 31.
    Li, Y., Liu, W., Turrini, A., Hahn, E.M., Zhang, L.: An efficient synthesis algorithm for parametric Markov chains against linear time properties (2016). CoRR. Google Scholar
  32. 32.
    Liu, W., Wang, J.: A tighter analysis of Piterman’s Büchi determinization. Inf. Process. Lett. 109(16), 941–945 (2009)CrossRefzbMATHGoogle Scholar
  33. 33.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. LMCS 3(3:5), 1–21 (2007)zbMATHGoogle Scholar
  34. 34.
    Reiter, M., Rubin, A.: Crowds: anonymity for web transactions. ACM TISSEC 1(1), 66–92 (1998)CrossRefGoogle Scholar
  35. 35.
    Safra, S.: On the complexity of \(\omega \)-automata. In: FOCS, pp. 319–327 (1988)Google Scholar
  36. 36.
    Schewe, S.: Tighter bounds for the determinisation of Büchi automata. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 167–181. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-00596-1_13 CrossRefGoogle Scholar
  37. 37.
    Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006). doi: 10.1007/11691372_26 CrossRefGoogle Scholar
  38. 38.
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338 (1985)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Yong Li
    • 1
    • 2
  • Wanwei Liu
    • 3
  • Andrea Turrini
    • 1
    Email author
  • Ernst Moritz Hahn
    • 1
  • Lijun Zhang
    • 1
    • 2
  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareCASBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.College of Computer ScienceNational University of Defense TechnologyChangshaChina

Personalised recommendations