Cited By
View all- Kupke CPattinson DSchröder L(2022)Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal LogicsACM Transactions on Computational Logic10.1145/350130023:2(1-34)Online publication date: 14-Jan-2022
Probabilistic modal µ-calculus with independent product
Author: 
Matteo MioAuthors Info & Claims
Abstract
The probabilistic modal µ-calculus pLµ (often called the quantitative µ-calculus) is a generalization of the standard modal µ-calculus designed for expressing properties of probabilistic labeled transition systems. The syntax of pLµ formulas coincides with that of the standard modal µ-calculus. Two equivalent semantics have been studied for pLµ, both assigning to each process-state p a value in [0, 1] representing the probability that the property expressed by the formula will hold in p: a denotational semantics and a game semantics given by means of two player stochastic games. In this paper we extend the logic pLµ with a second conjunction called product, whose semantics interprets the two conjuncts as probabilistically independent events. This extension allows one to encode useful operators, such as the modalities with probability one and with non-zero probability. We provide two semantics for this extended logic: one denotational and one based on a new class of games which we call tree games. The main result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin's Axiom at the first uncountable cardinal.
References
[1]
Bertrand, N., Genest, B., Gimbert, H.: Qualitative determinacy and decidability of stochastic games with signals. In: LICS 2009, IEEE Symposium on Logic in Computer Science, Los Angeles, USA (2009)
[2]
Blackwell, D.: Infinite Gd games with imperfect information. Matematyki Applicationes Mathematicae, Hugo Steinhaus Jubilee Volume (1969)
[3]
Brázdil, T., Brozek, V., ín Kucera, A., Obdrzálek, J.: Qualitative reachability in stochastic BPA games. In: STACS, pp. 207-218 (2009)
[4]
Brázdil, T., Brozek, V., Forejt, V., Kucera, A.: Stochastic games with branchingtime winning objectives. In: LICS, pp. 349-358 (2006)
[5]
de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. Journal of Computer and System Sciences 68, 374-397 (2004)
[6]
Deng, Y., van Glabbeek, R.: Characterising probabilistic processes logically. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 278-293. Springer, Heidelberg (2010)
[7]
Fischer, D., Gradel, E., Kaiser, L.: Model checking games for the quantitative µ-calculus. In: Theory of Computing Systems. Springer, New York (2009)
[8]
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6 (1994)
[9]
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: LICS 1997, Washington, DC, USA, p. 111. IEEE Computer Society, Los Alamitos (1997)
[10]
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science, 333-354 (1983)
[11]
Martin, D.A., Solovay, R.M.: Internal Cohen extensions. Ann. Math. Logic 2, 143- 178 (1970)
[12]
McIver, A., Morgan, C.: Results on the quantitative µ-calculus qMµ. ACM Trans. Comput. Logic 8(1), 3 (2007)
[13]
Mio, M.: The equivalence of denotational and game semantics for the probabilistic µ-calculus. In: 7th Workshop on Fixed Points in Computer Science (2010)
[14]
Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Groves, L., Reeves, S. (eds.) Proc. Formal Methods. Springer, Heidelberg (1997)
[15]
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, M.I.T. (1995)
[16]
Stirling, C.: Modal and temporal logics for processes. Springer, Heidelberg (2001)
Recommendations
On the Formalization of the Modal µ-Calculus in the Calculus of Inductive Constructions
We present a natural deduction proof system for the propositional modal -calculus and its formalization in the calculus of inductive constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets ...
A Characterization Theorem for the Alternation-Free Fragment of the Modal µ-Calculus
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer ScienceWe provide a characterization theorem, in the style of van Ben them and Janin-Walukiewicz, for the alternation-free fragment of the modal mu-calculus. For this purpose we introduce a variant of standard monadic second-order logic (MSO), which we call ...
Separation with Streams in the ?µ-calculus
LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer ScienceThe ??-calculus is an extension of the ?-calculus introduced in 1992 by Parigot [17] in order to generalize the Curry-Howard isomorphism to classical logic. Two versions of the calculus are usually considered in the literature: Parigot's original syntax ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 26 March 2011
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 22 Nov 2024
Other Metrics
Citations
Cited By
View all- Kupke CPattinson DSchröder L(2022)Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal LogicsACM Transactions on Computational Logic10.1145/350130023:2(1-34)Online publication date: 14-Jan-2022