Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL

DOI10.1016/S0304-3975(02)00612-6zbMath1019.03022MaRDI QIDQ1395428

Carroll Morgan, Annabelle McIver

Publication date: 1 July 2003

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

zbMATH Keywords

livenessprobabilistic transition systemsmodal mu-calculusalmost-certain correctnessprobabilistic temporal logic

Mathematics Subject Classification ID

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

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• Results on the propositional \(\mu\)-calculus
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Probabilistic verification
• Model checking of probabilistic and nondeterministic systems
• Verification of Probabilistic Programs
• The complexity of probabilistic verification
• Termination of Probabilistic Concurrent Program
• An expectation-transformer model for probabilistic temporal logic
• Demonic, angelic and unbounded probabilistic choices in sequential programs