Equivalence of probabilistic \(\mu\)-calculus and p-automata. (English) Zbl 1489.68122
Carayol, Arnaud (ed.) et al., Implementation and application of automata. 22nd international conference, CIAA 2017, Marne-la-Vallée, France, June 27–30, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10329, 64-75 (2017).
Summary: An important characteristic of Kozen’s \(\mu \)-calculus is its strong connection with parity alternating tree automata. Here, we show that the probabilistic \(\mu\)-calculus \(\mu^p\)-calculus and p-automata (parity alternating Markov chain automata) have an equally strong connection. Namely, for every \(\mu^p\)-calculus formula we can construct a p-automaton that accepts exactly those Markov chains that satisfy the formula. For every p-automaton we can construct a \(\mu^p\)-calculus formula satisfied in exactly those Markov chains that are accepted by the automaton. The translation in one direction relies on a normal form of the calculus and in the other direction on the usage of vectorial \(\mu^p\)-calculus. The proofs use the game semantics of \(\mu^p\)-calculus and automata to show that our translations are correct.
For the entire collection see [Zbl 1365.68007].
For the entire collection see [Zbl 1365.68007].
MSC:
| 68Q45 | Formal languages and automata |
| 03B70 | Logic in computer science |
| 03D05 | Automata and formal grammars in connection with logical questions |
| 60J20 | Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
References:
| [1] | Arnold, A., Niwiński, D.: Rudiments of \(\mu \)-calculus. Studies in Logic and the Foundations of Mathematics, vol. 146. Elsevier, New York (2001) · Zbl 0968.03002 |
| [2] | Baier, C.; Katoen, JP, Principles of Model Checking, 2008, Cambridge: The MIT Press, Cambridge · Zbl 1179.68076 |
| [3] | Blackburn, P.; Benthem, J.; Wolter, F., Handbook of Modal Logic, 2007, New York: Elsevier, New York · Zbl 1114.03001 |
| [4] | Bradfield, J., Stirling, C.: Modal \(\mu \)-calculi. In: Handbook of Modal Logic, pp. 721-756. Elsevier (2007) |
| [5] | Bradfield, J., Walukiewicz, I.: The \(\mu \)-calculus and model-checking. In: Handbook of Model Checking. Springer (2015) |
| [6] | Bruse, F.; Friedmann, O.; Lange, M., On guarded transformation in the modal \(\mu \)-calculus, Logic J. IGPL, 23, 2, 194-216, 2015 · Zbl 1405.03048 · doi:10.1093/jigpal/jzu030 |
| [7] | Cleaveland, R., Purushothaman Iyer, S., Narasimha, M.: Probabilistic temporal logics via the modal \(\mu \)-calculus. Theor. Comput. Sci. 342(2-3), 316-350 (2005) · Zbl 1077.68058 |
| [8] | Castro, P., Kilmurray, C., Piterman, N.: Tractable probabilistic \(\mu \)-calculus that expresses probabilistic temporal logics. In: 32nd Symposium on Theoretical Aspects of Computer Science. Schloss Dagstuhl (2015) · Zbl 1355.68173 |
| [9] | Chatterjee, K., Piterman, N.: Obligation Blackwell games and p-Automata. CoRR, abs/1206.5174 (2013) |
| [10] | Emerson, E.A., Jutla S.: Tree automata, \( \mu \)-calculus and determinacy. In: Proceedings of 32nd Annual Symposium on Foundations of Computer Science, pp. 368-377. IEEE (1991) |
| [11] | Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \(\mu \)-calculus. In: Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, LICS, pp. 267-278 (1986) |
| [12] | Grädel, E.; Thomas, W.; Wilke, T., Automata Logics, and Infinite Games: A Guide to Current Research, 2002, New York: Springer, New York · Zbl 1011.00037 · doi:10.1007/3-540-36387-4 |
| [13] | Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, 29 June- 2 July, pp. 111-122 (1997) |
| [14] | Janin, D., Walukiewicz, I.: Automata for the modal \(\mu \)-calculus and related results. Mathematical Foundations of Computer Science, pp. 552-562 (1995) · Zbl 1193.68163 |
| [15] | Kozen, D., Results on the propositional \(\mu \)-calculus, Theor. Comput. Sci., 27, 3, 333-354, 1983 · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6 |
| [16] | Kupferman, O.; Vardi, MY; Wolper, P., An automata-theoretic approach to branching-time model checking, J. ACM, 47, 2, 312-360, 2000 · Zbl 1133.68376 · doi:10.1145/333979.333987 |
| [17] | Mio, M.: Game semantics for probabilistic modal \(\mu \)-calculi. Ph.D. thesis, University of Edinburgh (2012) |
| [18] | Mio, M., Probabilistic modal \(\mu \)-calculus with independent product, Logical Methods Comput. Sci., 8, 4, 1-36, 2012 · Zbl 1261.03083 · doi:10.2168/LMCS-8(4:18)2012 |
| [19] | Mio, M., Simpson, A.K.: Łukasiewicz \(\mu \)-calculus. CoRR, abs/1510.00797 (2015) |
| [20] | Niwiński, D.: Fixed points vs. infinite generation. In: Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, LICS, pp. 402-409 (1988) |
| [21] | Niwiński, D., Fixed point characterization of infinite behavior of finite-state systems, Theor. Comput. Sci., 189, 1-2, 1-69, 1997 · Zbl 0893.68102 · doi:10.1016/S0304-3975(97)00039-X |
| [22] | Schneider, K., Verification of Reactive Systems: Formal Methods and Algorithms, 2004, Heidelberg: Springer, Heidelberg · Zbl 1067.68092 · doi:10.1007/978-3-662-10778-2 |
| [23] | Wilke, T., Alternating tree automata, parity games, and modal \(\mu \)-calculus, Bull. Soc. Math. Belg., 8, 2, 359-391, 2001 · Zbl 0994.68079 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
