Probabilistic Modal μ-Calculus with Independent Product

DOI10.1007/978-3-642-19805-2_20MaRDI QIDQ3000616zbMATH OpenOpenAlexFDO

Authors Matteo Mio

Publication date 19 May 2011

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

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)

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.

Recommendations

• Probabilistic modal \(\mu\)-calculus with independent product
• Probabilistic \(\mu\)-calculus: decidability and complete axiomatization
• Probabilistic temporal logics via the modal mu-calculus
• scientific article; zbMATH DE number 1330140
• A modal aleatoric calculus for probabilistic reasoning
• Probabilistic logic with independence
• Probabilistic logics with independence and confirmation
• scientific article; zbMATH DE number 7204557
• On Probabilistic λ-Calculi
• Towards a structural proof theory of probabilistic \(\mu\)-calculi

Cited in

(7)

• Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
• Compositionality for quantitative specifications
• Equivalence of probabilistic \(\mu\)-calculus and p-automata
• Model checking probabilistic systems
• Probabilistic \(\mu\)-calculus: decidability and complete axiomatization
• Probabilistic modal \(\mu\)-calculus with independent product
• Proof theory of Riesz spaces and modal Riesz spaces

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)