AI Chat Paper
Note: Please note that the following content is generated by AMiner AI. SciOpen does not take any responsibility related to this content.
{{lang === 'zh_CN' ? '文章概述' : 'Summary'}}
{{lang === 'en_US' ? '中' : 'Eng'}}
Chat more with AI
Powered by AMiner. Clicking this button will take you away from SciOpen.
Home Tsinghua Science and Technology Article
PDF (708.6 KB)
Cite
EndNote(RIS) BibTeX
Collect
Submit Manuscript AI Chat Paper
Show Outline
Outline
Show full outline
Hide outline
Outline
Show full outline
Hide outline
Open Access

An Axiom System of Probabilistic Mu-Calculus

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
Show Author Information

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μTLaxiom systemaconjunctive formulatableau approach

References

[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.
Tsinghua Science and Technology
Volume 27 Issue 2,
April 2022
Pages 372-385
DOI: 10.26599/TST.2020.9010054
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

817

Views

95

Downloads

0

Crossref

0

Web of Science

0

Scopus

0

CSCD

Altmetrics
Received: 24 September 2020
Revised: 15 October 2020
Accepted: 19 October 2020
Published: 29 September 2021
© The author(s) 2022

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