Document Open Access Logo

Probabilistic Mu-Calculus: Decidability and Complete Axiomatization

Authors Kim G. Larsen, Radu Mardare, Bingtian Xue

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.25.pdf
  • Filesize: 0.61 MB
  • 18 pages

Document Identifiers

Author Details

Kim G. Larsen
Radu Mardare
Bingtian Xue

Cite AsGet BibTex

Kim G. Larsen, Radu Mardare, and Bingtian Xue. Probabilistic Mu-Calculus: Decidability and Complete Axiomatization. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.25

Abstract

We introduce a version of the probabilistic mu-calculus (PMC) built on top of a probabilistic modal logic that allows encoding n-ary inequational conditions on transition probabilities. PMC extends previously studied calculi and we prove that, despite its expressiveness, it enjoys a series of good meta-properties. Firstly, we prove the decidability of satisfiability checking by establishing the small model property. An algorithm for deciding the satisfiability problem is developed. As a second major result, we provide a complete axiomatization for the alternation-free fragment of PMC. The completeness proof is innovative in many aspects combining various techniques from topology and model theory.
Keywords
  • Markov process
  • probabilistic modal mu-calculus
  • n-ary (in-)equational modalities
  • satisfiability
  • axiomatization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Nathalie Bertrand, John Fearnley, and Sven Schewe. Bounded satisfiability for PCTL. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, pages 92-106. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2012.92.
  2. Girish Bhat and Rance Cleaveland. Efficient model checking via the equational μ-calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 304-312. IEEE Computer Society, 1996. URL: http://dx.doi.org/10.1109/LICS.1996.561358.
  3. Patrick Billingsley. Probability and Measure. Wiley-Interscience, 1995. Google Scholar
  4. Tomás Brázdil, Vojtech Forejt, Jan Kretínský, and Antonín Kucera. The satisfiability problem for probabilistic CTL. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 391-402. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.21.
  5. Pablo F. Castro, Cecilia Kilmurray, and Nir Piterman. Tractable probabilistic mu-calculus that expresses probabilistic temporal logics. In 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, pages 211-223. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2015.211.
  6. S. Chakraborty and J-P. Katoen. On the satisfiability of some simple probabilistic logics. In Proceedings of the Thirty-First Annual IEEE Symposium on Logic in Computer Science, LICS 2016, 5-8 July 2016, New York City, USA, 2016. Google Scholar
  7. Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus. In Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings, pages 179-193. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04027-6_15.
  8. Rance Cleaveland, S. Purushothaman Iyer, and Murali Narasimha. Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci., 342(2-3):316-350, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2005.03.048.
  9. Rance Cleaveland, Marion Klein, and Bernhard Steffen. Faster model checking for the modal mu-calculus. In Computer Aided Verification, Fourth International Workshop, CAV1992, Montreal, Canada, June 29 - July 1, 1992, Proceedings, pages 410-422. Springer, 1992. URL: http://dx.doi.org/10.1007/3-540-56496-9_32.
  10. Rance Cleaveland and Bernhard Steffen. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design, 2(2):121-147, 1993. URL: http://dx.doi.org/10.1007/BF01383878.
  11. Robert Goldblatt. On the role of the baire category theorem and dependent choice in the foundations of logic. J. Symb. Log., 50(2):412-422, 1985. URL: http://dx.doi.org/10.2307/2274230.
  12. Robert Goldblatt. Topological proofs of some rasiowa-sikorski lemmas. Studia Logica, 100(1-2):175-191, 2012. URL: http://dx.doi.org/10.1007/s11225-012-9374-2.
  13. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Asp. Comput., 6(5):512-535, 1994. URL: http://dx.doi.org/10.1007/BF01211866.
  14. Sergiu Hart and Micha Sharir. Probabilistic propositional temporal logics. Information and Control, 70(2/3):97-155, 1986. URL: http://dx.doi.org/10.1016/S0019-9958(86)80001-8.
  15. Dexter Kozen. Results on the propositional μ-calculus. In Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings, pages 348-359. Springer, 1982. URL: http://dx.doi.org/10.1007/BFb0012782.
  16. Dexter Kozen, Kim G. Larsen, Radu Mardare, and Prakash Panangaden. Stone duality for markov processes. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 321-330. IEEE Computer Society, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.38.
  17. Clemens Kupke and Dirk Pattinson. On modal logics of linear inequalities. In Advances in Modal Logic 8, papers from the eighth conference on "Advances in Modal Logic," held in Moscow, Russia, 24-27 August 2010, pages 235-255. College Publications, 2010. Google Scholar
  18. Kim G. Larsen, Radu Mardare, and Bingtian Xue. Alternation-free weighted mu-calculus: Decidability and completeness. Electr. Notes Theor. Comput. Sci., 319:289-313, 2015. URL: http://dx.doi.org/10.1016/j.entcs.2015.12.018.
  19. Kim Guldstrand Larsen. Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci., 72(2&3):265-288, 1990. URL: http://dx.doi.org/10.1016/0304-3975(90)90038-J.
  20. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90030-6.
  21. Kim Guldstrand Larsen and Arne Skou. Compositional verification of probabilistic processes. In CONCUR'92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, pages 456-471. Springer, 1992. URL: http://dx.doi.org/10.1007/BFb0084809.
  22. Daniel J. Lehmann and Saharon Shelah. Reasoning with time and chance. Information and Control, 53(3):165-198, 1982. URL: http://dx.doi.org/10.1016/S0019-9958(82)91022-1.
  23. Wanwei Liu, Lei Song, Ji Wang, and Lijun Zhang. A simple probabilistic extension of modal mu-calculus. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 882-888. AAAI Press, 2015. Google Scholar
  24. Henryk Michalewski and Matteo Mio. Baire category quantifier in monadic second order logic. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, pages 362-374. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_29.
  25. Matteo Mio. Probabilistic modal μ-calculus with independent product. Logical Methods in Computer Science, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(4:18)2012.
  26. Matteo Mio and Alex Simpson. Łukasiewicz mu-calculus. In Proceedings Workshop on Fixed Points in Computer Science, FICS 2013, Turino, Italy, September 1st, 2013., pages 87-104, 2013. URL: http://dx.doi.org/10.4204/EPTCS.126.7.
  27. Matteo Mio, Alex Simpson, and Colin Stirling. Game Semantics for Probabilistic Modal M-calculi. University of Edinburgh, 2012. Google Scholar
  28. Prakash Panangaden. Labelled Markov Processes. Imperial College Press, 2009. Google Scholar
  29. Vaughan R. Pratt. A decidable mu-calculus: Preliminary report. In 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981, pages 421-427. IEEE Computer Society, 1981. URL: http://dx.doi.org/10.1109/SFCS.1981.4.
  30. H. Rasiowa and R. Sikorski. A proof of the completeness theorem of Gödel. Fund. Math, 37:193-200, 1950. Google Scholar
  31. Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley &Sons, Chichester, 1986. Google Scholar
  32. D. Scott and J. de Bakker. A theory of programs. unpubilished notes, 1969. Google Scholar
  33. Robert S. Streett and E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput., 81(3):249-264, 1989. URL: http://dx.doi.org/10.1016/0890-5401(89)90031-X.
  34. Igor Walukiewicz. Completeness of kozen’s axiomatisation of the propositional μ-calculus. Inf. Comput., 157(1-2):142-182, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2836.
  35. Chunlai Zhou. A complete deductive system for probability logic. J. Log. Comput., 19(6):1427-1454, 2009. URL: http://dx.doi.org/10.1093/logcom/exp031.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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