Document Open Access Logo

Compositional Reasoning for Parametric Probabilistic Automata

Authors Hannah Mertens , Tim Quatmann , Joost-Pieter Katoen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.31.pdf
  • Filesize: 1.18 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.31.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Verification
  • Probabilistic systems
  • Assume-guarantee reasoning
  • Parametric Probabilistic Automata
  • Parameter synthesis

Metrics

Abstract

We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.

Cite As Get BibTex

Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen. Compositional Reasoning for Parametric Probabilistic Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.31

Author Details

Hannah Mertens
  • RWTH Aachen University, Germany
Tim Quatmann
  • RWTH Aachen University, Germany
Joost-Pieter Katoen
  • RWTH Aachen University, Germany

Funding

  • Quatmann, Tim: This research was funded by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW.

References

  1. Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods Syst. Des., 15(1):7-48, 1999. URL: https://doi.org/10.1023/A:1008739929481.
  2. Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, and Harald Ruess. Compositional parameter synthesis. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 60-68, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_4.
  3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  4. Samik Basu and C. R. Ramakrishnan. Compositional analysis for verification of parameterized systems. Theor. Comput. Sci., 354(2):211-229, 2006. URL: https://doi.org/10.1016/J.TCS.2005.11.016.
  5. Redouane Bouchekir and Mohand Cherif Boukala. Toward implicit learning for the compositional verification of Markov decision processes. In Mohamed Faouzi Atig, Saddek Bensalem, Simon Bliudze, and Bruno Monsuez, editors, Verification and Evaluation of Computer and Communication Systems - 12th International Conference, VECoS 2018, Grenoble, France, September 26-28, 2018, Proceedings, volume 11181 of Lecture Notes in Computer Science, pages 200-217. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00359-3_13.
  6. Redouane Bouchekir, Saïda Boukhedouma, and Mohand Cherif Boukala. Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes. In Yuri Merkuryev, Tuncer I. Ören, and Mohammad S. Obaidat, editors, Proceedings of the 6th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2016), Lisbon, Portugal, July 29-31, 2016, pages 244-253. SciTePress, 2016. URL: https://doi.org/10.5220/0005978602440253.
  7. Radu Calinescu, Shinji Kikuchi, and Kenneth Johnson. Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In Radu Calinescu and David Garlan, editors, Large-Scale Complex IT Systems. Development, Operation and Management - 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012, Revised Selected Papers, volume 7539 of Lecture Notes in Computer Science, pages 303-329. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-34059-8_16.
  8. Luca Cardelli, Kim G. Larsen, and Radu Mardare. Modular Markovian logic. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 380-391. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_30.
  9. Souymodip Chakraborty and Joost-Pieter Katoen. Parametric LTL on Markov chains. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 207-221. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7_17.
  10. Krishnendu Chatterjee, Martin Chmelik, and Przemyslaw Daca. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods Syst. Des., 47(2):230-264, 2015. URL: https://doi.org/10.1007/S10703-015-0235-2.
  11. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154-169. Springer, 2000. URL: https://doi.org/10.1007/10722167_15.
  12. Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 353-362. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39190.
  13. Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. Learning assumptions for compositional verification. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 331-346. Springer, 2003. URL: https://doi.org/10.1007/3-540-36577-X_24.
  14. Conrado Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of Lecture Notes in Computer Science, pages 280-294. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-31862-0_21.
  15. Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science, pages 351-365. Springer, 2001. URL: https://doi.org/10.1007/3-540-44685-0_24.
  16. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. Automated circular assume-guarantee reasoning. Formal Aspects Comput., 30(5):571-595, 2018. URL: https://doi.org/10.1007/S00165-017-0436-0.
  17. Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci., 4(4), 2008. URL: https://doi.org/10.2168/LMCS-4(4:8)2008.
  18. Lu Feng, Marta Z. Kwiatkowska, and David Parker. Compositional verification of probabilistic systems using learning. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pages 133-142. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/QEST.2010.24.
  19. Lu Feng, Marta Z. Kwiatkowska, and David Parker. Automated learning of probabilistic assumptions for compositional reasoning. In Dimitra Giannakopoulou and Fernando Orejas, editors, Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6603 of Lecture Notes in Computer Science, pages 2-17. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19811-3_2.
  20. Lu Feng, Clemens Wiltsche, Laura R. Humphrey, and Ufuk Topcu. Controller synthesis for autonomous systems interacting with human operators. In ICCPS, pages 70-79. ACM, 2015. URL: https://doi.org/10.1145/2735960.2735973.
  21. Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Automated verification techniques for probabilistic systems. In Marco Bernardo and Valérie Issarny, editors, Formal Methods for Eternal Networked Software Systems - 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011. Advanced Lectures, volume 6659 of Lecture Notes in Computer Science, pages 53-113. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21455-4_3.
  22. Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, and Sarai Sheinvald. Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf., 24(5):667-689, 2022. URL: https://doi.org/10.1007/S10009-022-00669-9.
  23. Anubhav Gupta, Kenneth L. McMillan, and Zhaohui Fu. Automated assumption generation for compositional verification. Formal Methods Syst. Des., 32(3):285-301, 2008. URL: https://doi.org/10.1007/S10703-008-0050-0.
  24. Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and Lijun Zhang. Learning weighted assumptions for compositional verification of Markov decision processes. ACM Trans. Softw. Eng. Methodol., 25(3):21:1-21:39, 2016. URL: https://doi.org/10.1145/2907943.
  25. Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. You assume, we guarantee: Methodology and case studies. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 440-451. Springer, 1998. URL: https://doi.org/10.1007/BFB0028765.
  26. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596-619, 1983. URL: https://doi.org/10.1145/69575.69577.
  27. Sebastian Junges. Parameter synthesis in Markov models. PhD thesis, RWTH Aachen University, Germany, 2020. URL: https://publications.rwth-aachen.de/record/783179.
  28. Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des., 62(1):181-259, 2024. URL: https://doi.org/10.1007/S10703-023-00442-X.
  29. Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, and Tobias Winkler. The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci., 119:183-210, 2021. URL: https://doi.org/10.1016/J.JCSS.2021.02.006.
  30. Sebastian Junges and Matthijs T. J. Spaan. Abstraction-refinement for hierarchical probabilistic models. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 102-123. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_6.
  31. Joost-Pieter Katoen. The probabilistic model checking landscape. In LICS, pages 31-45. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934574.
  32. Anvesh Komuravelli, Corina S. Pasareanu, and Edmund M. Clarke. Assume-guarantee abstraction refinement for probabilistic systems. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 310-326. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_25.
  33. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Using probabilistic model checking in systems biology. SIGMETRICS Perform. Evaluation Rev., 35(4):14-21, 2008. URL: https://doi.org/10.1145/1364644.1364651.
  34. Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Assume-guarantee verification for probabilistic systems. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 23-37. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_3.
  35. Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38-65, 2013. URL: https://doi.org/10.1016/J.IC.2013.10.001.
  36. Rui Li and Yang Liu. Compositional stochastic model checking probabilistic automata via symmetric assume-guarantee rule. In 17th IEEE International Conference on Software Engineering Research, Management and Applications, SERA 2019, Honolulu, HI, USA, May 29-31, 2019, pages 110-115. IEEE, 2019. URL: https://doi.org/10.1109/SERA.2019.8886808.
  37. Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, and Tobias Winkler. Accurately computing expected visiting times and stationary distributions in Markov chains. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14571 of Lecture Notes in Computer Science, pages 237-257. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57249-4_12.
  38. Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen. Compositional reasoning for parametric probabilistic automata, 2025. URL: https://arxiv.org/abs/2506.08525.
  39. Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 589-606. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_39.
  40. Gethin Norman and Vitaly Shmatikov. Analysis of probabilistic contract signing. J. Comput. Secur., 14(6):561-589, 2006. URL: https://doi.org/10.3233/jcs-2006-14604.
  41. Corina S. Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M. Cobleigh, and Howard Barringer. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des., 32(3):175-205, 2008. URL: https://doi.org/10.1007/S10703-008-0049-6.
  42. Corina S. Pasareanu, Divya Gopinath, and Huafeng Yu. Compositional verification for autonomous systems with deep learning components. CoRR, abs/1810.08303, 2018. URL: https://arxiv.org/abs/1810.08303.
  43. Corina S. Pasareanu, Ravi Mangal, Divya Gopinath, and Huafeng Yu. Assumption generation for learning-enabled autonomous systems. In Panagiotis Katsaros and Laura Nenzi, editors, Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3-6, 2023, Proceedings, volume 14245 of Lecture Notes in Computer Science, pages 3-22. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-44267-4_1.
  44. Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8-19 October 1984, volume 13 of NATO ASI Series, pages 123-144. Springer, 1984. URL: https://doi.org/10.1007/978-3-642-82453-1_5.
  45. Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter synthesis for Markov models: Faster than ever. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 50-67, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_4.
  46. Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. URL: https://hdl.handle.net/1721.1/36560.
  47. Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. Nord. J. Comput., 2(2):250-273, 1995. Google Scholar
  48. Antti Siirtola and Keijo Heljanko. Parametrised compositional verification with multiple process and data types. In Josep Carmona, Mihai T. Lazarescu, and Marta Pietkiewicz-Koutny, editors, 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013, pages 60-69. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/ACSD.2013.9.
  49. Jip Spel. Monotonicity in Markov models. PhD thesis, RWTH Aachen University, Germany, 2023. URL: https://publications.rwth-aachen.de/record/974903.
  50. Jip Spel, Sebastian Junges, and Joost-Pieter Katoen. Are parametric Markov chains monotonic? In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 479-496. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_28.
  51. Jip Spel, Sebastian Junges, and Joost-Pieter Katoen. Finding provably optimal Markov chains. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 173-190. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_10.
  52. Mariëlle Stoelinga. An introduction to probabilistic automata. Bull. EATCS, 78:176-198, 2002. Google Scholar
  53. Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, and Matthias Volk, editors, Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, volume 15262 of Lecture Notes in Computer Science, pages 423-445. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-75778-5_20.
  54. Clemens Wiltsche. Assume-guarantee strategy synthesis for stochastic games. PhD thesis, University of Oxford, UK, 2015. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.719857.
  55. Xiaobin Zhang, Bo Wu, and Hai Lin. Assume-guarantee reasoning framework for MDP-POMDP. In 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016, pages 795-800. IEEE, 2016. URL: https://doi.org/10.1109/CDC.2016.7798365.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact