Journal Home > Volume 27 , Issue 2
Tsinghua Science and Technology 2022, 27(2): 372-385 https://doi.org/10.26599/TST.2020.9010054
Open Access | Issue | Published: 29 September 2021

An Axiom System of Probabilistic Mu-Calculus

Show Author's Information Wanwei Liu( ),  Junnan Xu,  David N. Jansen,  Andrea Turrini,  Lijun Zhang
College of Computer Science, National University of Defense Technology, Changsha 410073, China
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
University of Chinese Academy of Sciences, Beijing 100039, China
Institute of Intelligent Software, Guangzhou 511458, China
Keywords:
PμTL, axiom system, aconjunctive formula, tableau approach
Cite this article:
Liu W, Xu J, Jansen DN, et al. An Axiom System of Probabilistic Mu-Calculus. Tsinghua Science and Technology, 2022, 27(2): 372-385. https://doi.org/10.26599/TST.2020.9010054
Download citation
EndNote(RIS)
BibTeX

542

Views

57

Downloads

Citations

0

Crossref

0

WoS

0

Scopus

0

CSCD

Abstract Full text About this article

Mu-calculus (a.k.a. μTL) is built up from modal/dynamic logic via adding the least fixpoint operator μ. This type of logic has attracted increasing attention since Kozen’s seminal work. P μTL is a succinct probabilistic extension of the standard μTL obtained by making the modal operators probabilistic. Properties of this logic, such as expressiveness and satisfiability decision, have been studied elsewhere. We consider another important problem: the axiomatization of that logic. By extending the approaches of Kozen and Walukiewicz, we present an axiom system for P μTL. In addition, we show that the axiom system is complete for aconjunctive formulas.


menu
Abstract
Full text
Outline
About this article

An Axiom System of Probabilistic Mu-Calculus

Show Author's information Wanwei Liu( ), Junnan Xu, David N. Jansen, Andrea Turrini, Lijun Zhang
College of Computer Science, National University of Defense Technology, Changsha 410073, China
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
University of Chinese Academy of Sciences, Beijing 100039, China
Institute of Intelligent Software, Guangzhou 511458, China

Abstract

Mu-calculus (a.k.a. μTL) is built up from modal/dynamic logic via adding the least fixpoint operator μ. This type of logic has attracted increasing attention since Kozen’s seminal work. P μTL is a succinct probabilistic extension of the standard μTL obtained by making the modal operators probabilistic. Properties of this logic, such as expressiveness and satisfiability decision, have been studied elsewhere. We consider another important problem: the axiomatization of that logic. By extending the approaches of Kozen and Walukiewicz, we present an axiom system for P μTL. In addition, we show that the axiom system is complete for aconjunctive formulas.

Keywords: PμTL, axiom system, aconjunctive formula, tableau approach

References(30)

[1]
D. Kozen, Results on the propositional μ-calculus, Theor. Comput. Sci., vol. 27, no. 3, pp. 333-354, 1983.
Google Scholar
[2]
I. Walukiewicz, Completeness of Kozen’s axiomatisation of the propositional μ-calculus, Inf. Comput., vol. 157, nos. 1-2, pp. 142-182, 2000.
Google Scholar
[3]
B. Banieqbal and H. Barringer, Temporal logic with fixed points, in Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, eds. Berlin, Germany: Springer, 1987, pp. 62-74.
[4]
C. Morgan and A. McIver, A probabilistic temporal calculus based on expectations, in Proc. Formal Methods Pacific, Singapore, 1997, pp. 4-22.
[5]
D. Niwiński and I. Walukiewicz, Games for the μ-calculus, Theor. Comput. Sci., vol. 163, nos. 1-2, pp. 99-116, 1996.
Google Scholar
[6]
K. Tamura, Completeness of Kozen’s axiomatization for the modal mu-calculus: A simple proof, arXiv preprint arXiv: 1408.3560, 2014.
Google Scholar
[7]
X. Song, W. Jiang, X. Liu, H. Lu, Z. Tian, and X. Du, A survey of game theory as applied to social networks, Tsinghua Science and Technology, vol. 25, no. 6, pp. 734-742, 2020.
Google Scholar
[8]
D. Kozen, Semantics of probabilistic programs, J. Comput. Syst. Sci., vol. 22, no. 3, pp. 328-350, 1981.
Google Scholar
[9]
H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Asp. Comput., vol. 6, no. 5, pp. 512-535, 1994.
Google Scholar
[10]
C. Baier, On algorithmic verification methods for probabilistic systems, Habilitationsschrift, Fakultät für Mathematik und Informatik, Universität Mannheim, Mannheim, Germany, 1998.
[11]
C. Baier and J. P. Katoen, Principles of Model Checking. Cambridge, MA, USA: The MIT Press, 2008.
[12]
A. Bianco and L. de Alfaro, Model checking of probabilistic and nondeterministic systems, in Foundations of Software Technology and Theoretical Computer Science, P. S. Thiagarajan, ed. Berlin, Germany: Springer, 1995, pp. 499-513.
[13]
T. Brázdil, V. Forejt, J. Kretínský, and A. Kucera, The satisfiability problem for probabilistic CTL, in Proc. 2008 23rd Annu. IEEE Symp. Logic in Computer Science, Pittsburgh, PA, USA, 2018, pp. 391-402.
[14]
L. de Alfaro, Formal verification of probabilistic systems, PhD dissertation, Stanford University, Stanford, CA, USA, 1997.
[15]
R. Dimitrova, L. M. F. Fioriti, H. Hermanns, and R. Majumdar, Probabilistic CTL*: The deductive way, in Tools and Algorithms for the Construction and Analysis of Systems, M. Chechik and J. F. Raskin, eds. Berlin, Germany: Springer, 2016, pp. 280-296.
[16]
W. W. Liu, L. Song, J. Wang, and L. J. Zhang, A simple probabilistic extension of modal μ-calculus, in Proc. 24th Int. Conf. Artificial Intelligence, Buenos Aires, Argentina, 2015, pp. 882-888.
[17]
Z. B. He and J. X. Zhou, Inference attacks on genomic data based on probabilistic graphical models, Big Data Mining and Anal ytics, vol. 3, no. 3, pp. 225-233, 2020.
Google Scholar
[18]
L. de Alfaro and R. Majumdar, Quantitative solution of omega-regular games, in Proc. 33rd Annu. ACM Symp. Theory of Computing, New York, NY, USA, 2001, pp. 675-683.
[19]
M. Huth and M. Kwiatkowska, Quantitative analysis and model checking, in Proc. 20th Annu. IEEE Symp. Logic in Computer Science, Warsaw, Poland, 1997, pp. 111-122.
[20]
A. K. McIver and C. C. Morgan, Games, probability and the quantitative μ-calculus qMμ, in Logic for Programming, Artificial Intelligence, and Reasoning, M. Baaz and A. Voronkov, eds. Berlin, Germany: Springer, 2002, pp. 292-310.
[21]
A. McIver and C. Morgan, Results on the quantitative μ-calculus qMμ, ACM Trans. Comput. Log., vol. 8, no. 1, p. 3, 2007.
Google Scholar
[22]
M. Mio, Probabilistic modal μ-calculus with independent product, in Foundations of Software Science and Computational Structures, M. Hofmann, ed. Berlin, Germany: Springer, 2011, pp. 290-304.
[23]
R. Cleaveland, S. P. Iyer, and M. Narasimha, Probabilistic temporal logics via the modal mu-calculus, Theor. Comput. Sci., vol. 342, nos. 2&3, pp. 316-350, 2005.
Google Scholar
[24]
P. F. Castro, C. Kilmurray, and N. Piterman, Tractable probabilistic μ-calculus that expresses probabilistic temporal logics, in Proc. 32nd Int. Symp. Theoretical Aspects of Computer Science: STACS’15, E. W. Mayr and N. Ollinger, eds. Dagstuhl, Germany, 2015, pp. 211-223.
[25]
S. Chakraborty and J. P. Katoen. On the satisfiability of some simple probabilistic logics, in Proc. 31st Annu. ACM/IEEE Symp. Logic in Computer Science, New York, NY, USA, 2016, pp. 56-65.
[26]
F. Song, Y. D. Zhang, T. L. Chen, Y. Tang, and Z. W. Xu, Probabilistic alternating-time μ-calculus, in Proc. 33rd AAAI Conf. Artificial Intelligence, AAAI 2019, The 31st Innovative Applications of Artificial Intelligence Conf., IAAI 2019, The 9th AAAI Symp. Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, HI, USA, 2019, pp. 6179-6186.
[27]
K. G. Larsen, R. Mardare, and B. T. Xue, Probabilistic mu-calculus: decidability and complete axiomatization, in Proc. 36th IARCS Annu. Conf. Foundations of Software Technology and Theoretical Computer Science: FSTTCS, A. Lal, S. Akshay, S. Saurabh, and S. Sen, eds. Dagstuhl, Germany, 2016, pp. 25:1-25:18.
[28]
R. S. Streett and E. A. Emerson, An automata theoretic decision procedure for the propositional mu-calculus, Inf. Comput., vol. 81, no. 3, pp. 249-264, 1989.
Google Scholar
[29]
J. Xu, W. Liu, D. N. Jansen, and L. Zhang, An axiomatisation of the probabilistic μ-calculus, in Formal Methods and Software Engineering, Y. A. Ameur and S. C. Qin, eds. Cham, Germany: Springer, 2019, pp. 420-437.
[30]
C. Löding, Methods for the transformation of ω-automata: complexity and connection to second order logic, Master dissertation, Christian-Albrechts-University of Kiel, Kiel, Germany, 1998.
Publication history
Copyright
Acknowledgements
Rights and permissions

Publication history

Received: 24 September 2020
Revised: 15 October 2020
Accepted: 19 October 2020
Published: 29 September 2021
Issue date: April 2022

Copyright

© The author(s) 2022

Acknowledgements

W. W. Liu is supported by the National Science Foundation of China (No. 61872371), the Open Fund from the State Key Laboratory of High Performance Computing of China (HPCL) (No. 2020001-07), and the National Key Research and Development Program of China (No. 2018YFB0204301). L. J. Zhang is supported by the Guangdong Science and Technology (No. 2018B010107004) and the National Science Foundation of China (Nos. 61761136011 and 61836005).

Rights and permissions

The articles published in this open access journal are distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/).

Return