Probabilistic temporal logics via the modal mu-calculus

DOI10.1016/J.TCS.2005.03.048MaRDI QIDQ2566296zbMATH OpenOpenAlexFDO

Authors Rance Cleaveland, S. Purushothaman Iyer, Murali Narasimha

Publication date 22 September 2005

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL http://www.lib.ncsu.edu/resolver/1840.4/710

zbMATH Keywords

Model-checkingProbabilistic bisimulationProbabilistic temporal logicProbabilistic transition systemsReactive probabilistic labeled transition systemsReactive systems

Mathematics Subject Classification ID

Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1330140
• scientific article; zbMATH DE number 1497761
• Probabilistic modal \(\mu\)-calculus with independent product
• An expectation-transformer model for probabilistic temporal logic
• Tractable probabilistic -calculus that expresses probabilistic temporal logics

Cites work

• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• A Theory of Communicating Sequential Processes
• Algebraic laws for nondeterminism and concurrency
• An automata-theoretic approach to branching-time model checking
• An improved algorithm for the evaluation of fixpoint expressions
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Bisimulation through probabilistic testing
• Handbook of process algebra
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 1754605 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• scientific article; zbMATH DE number 3371972 (Why is no real title available?)
• Interpolants and Symbolic Model Checking
• Model checking and boolean graphs
• Model checking of probabilistic and nondeterministic systems
• Probabilistic verification
• Results on the propositional \(\mu\)-calculus
• Solving Polynomial Systems Using a Branch and Prune Approach
• Tableau-based model checking in the propositional mu-calculus
• Testing equivalences for processes
• “Sometimes” and “not never” revisited

Cited in

(21)

• Selective mu-calculus and formula-based equivalence of transition systems
• Probabilization of logics: completeness and decidability
• Equivalence of probabilistic \(\mu\)-calculus and p-automata
• A survey on temporal logics for specifying and verifying real-time systems
• On finite-state approximants for probabilistic computation tree logic
• Tractable probabilistic -calculus that expresses probabilistic temporal logics
• Probabilistic Modal μ-Calculus with Independent Product
• Qualitative Logics and Equivalences for Probabilistic Systems
• scientific article; zbMATH DE number 1324658 (Why is no real title available?)
• scientific article; zbMATH DE number 1330140 (Why is no real title available?)
• scientific article; zbMATH DE number 1497761 (Why is no real title available?)
• Łukasiewicz \(\mu\)-calculus
• Probabilistic modal \(\mu\)-calculus with independent product
• Model checking with probabilistic tabled logic programming
• An expectation-transformer model for probabilistic temporal logic
• scientific article; zbMATH DE number 7319046 (Why is no real title available?)
• Separable GPL: decidable model checking with more non-determinism
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• Probabilistic logics based on Riesz spaces
• Probabilistic logic over paths
• Coalgebraic satisfiability checking for arithmetic -calculi

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Probabilistic temporal logics via the modal mu-calculus

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