Probabilistic Modal μ-Calculus with Independent Product

DOI10.1007/978-3-642-19805-2_20zbMATH Open1326.68202arXiv1211.1511OpenAlexW1932846340MaRDI QIDQ3000616FDOQ3000616

Matteo Mio

Publication date: 19 May 2011

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Abstract: The probabilistic modal {mu}-calculus is a fixed-point logic designed for expressing properties of probabilistic labeled transition systems (PLTS's). Two equivalent semantics have been studied for this logic, both assigning to each state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other is a game semantics, specified in terms of two-player stochastic parity games. A shortcoming of the probabilistic modal {mu}-calculus is the lack of expressiveness required to encode other important temporal logics for PLTS's such as Probabilistic Computation Tree Logic (PCTL). To address this limitation we extend the logic with a new pair of operators: independent product and coproduct. The resulting logic, called probabilistic modal {mu}-calculus with independent product, can encode many properties of interest and subsumes the qualitative fragment of PCTL. The main contribution of this paper is the definition of an appropriate game semantics for this extended probabilistic {mu}-calculus. This relies on the definition of a new class of games which generalize standard two-player stochastic (parity) games by allowing a play to be split into concurrent subplays, each continuing their evolution independently. Our main technical result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin's Axiom at an uncountable cardinal.

Full work available at URL: https://arxiv.org/abs/1211.1511

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (4)

• Title not available (Why is that?)
• Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
• Model Checking Probabilistic Systems
• Compositionality for quantitative specifications

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Probabilistic logics with independence and confirmation 👍 👎
• Probabilistic logic with independence 👍 👎
• Probabilistic modal {\mu}-calculus with independent product 👍 👎
• Probabilistic temporal logics via the modal mu-calculus 👍 👎
• A modal aleatoric calculus for probabilistic reasoning 👍 👎
• Towards a structural proof theory of probabilistic \(\mu\)-calculi 👍 👎
• On Probabilistic λ-Calculi 👍 👎

This page was built for publication: Probabilistic Modal μ-Calculus with Independent Product

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000616)