Parameter Synthesis Algorithms for Parametric Interval Markov Chains

  • Laure PetrucciEmail author
  • Jaco van de PolEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10854)


This paper considers the consistency problem for Parametric Interval Markov Chains. In particular, we introduce a co-inductive definition of consistency, which improves and simplifies previous inductive definitions considerably. The equivalence of the inductive and co-inductive definitions has been formally proved in the interactive theorem prover PVS.

These definitions lead to forward and backward algorithms, respectively, for synthesizing an expression for all parameters for which a given PIMC is consistent. We give new complexity results when tackling the consistency problem for IMCs (i.e. without parameters). We provide a sharper upper bound, based on the longest simple path in the IMC. The algorithms are also optimized, using different techniques (dynamic programming cache, polyhedra representation, etc.). They are evaluated on a prototype implementation. For parameter synthesis, we use Constraint Logic Programming and the PARMA library for convex polyhedra.



The authors would like to thank the reviewers for their extensive comments, which helped them to improve the paper. They acknowledge the support of University Paris 13 and of the Van Gogh project PAMPAS, that covered their mutual research visits.


  1. 1.
    Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Bart, A., Delahaye, B., Lime, D., Monfroy, É., Truchet, C.: Reachability in parametric interval Markov chains using constraints. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 173–189. Springer, Cham (2017). Scholar
  3. 3.
    Bergstra, J.A., Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes. In: ICALP 1984, pp. 82–94 (1984)Google Scholar
  4. 4.
    Češka, M., Pilař, P., Paoletti, N., Brim, L., Kwiatkowska, M.: PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 367–384. Springer, Heidelberg (2016). Scholar
  5. 5.
    Chakraborty, S., Katoen, J.-P.: Model checking of open interval Markov chains. In: Gribaudo, M., Manini, D., Remke, A. (eds.) ASMTA 2015. LNCS, vol. 9081, pp. 30–42. Springer, Cham (2015). Scholar
  6. 6.
    Chen, T., Han, T., Kwiatkowska, M.Z.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210–216 (2013)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005). Scholar
  8. 8.
    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, Cham (2015). Scholar
  9. 9.
    Delahaye, B.: Consistency for parametric interval Markov chains. In: SynCoP 2015, pp. 17–32 (2015)Google Scholar
  10. 10.
    Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: Abstract probabilistic automata. Inf. Comput. 232, 66–116 (2013)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: New results for constraint Markov chains. Perform. Eval. 69(7–8), 379–401 (2012)CrossRefGoogle Scholar
  12. 12.
    Delahaye, B., Lime, D., Petrucci, L.: Parameter synthesis for parametric interval Markov chains. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 372–390. Springer, Heidelberg (2016). Scholar
  13. 13.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2011)CrossRefGoogle Scholar
  14. 14.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS 1991, pp. 266–277 (1991)Google Scholar
  15. 15.
    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). Scholar
  16. 16.
    Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Asp. Comput. 19(1), 93–109 (2007)CrossRefGoogle Scholar
  17. 17.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). Scholar
  18. 18.
    Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50–67. Springer, Cham (2016). Scholar
  19. 19.
    Wielemakers, J.: SWI-prolog version 7 extensions. In: WLPE-2014, July 2014Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2018

Authors and Affiliations

  1. 1.LIPN, CNRS UMR 7030, Université Paris 13, Sorbonne Paris CitéVilletaneuseFrance
  2. 2.Formal Methods and ToolsUniversity of TwenteEnschedeThe Netherlands

Personalised recommendations