State explosion in almost-sure probabilistic reachability

DOI10.1016/j.ipl.2007.01.003zbMath1184.68318MaRDI QIDQ846015

Jeremy Sproston, François Laroussinie

Publication date: 29 January 2010

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2007.01.003

zbMATH Keywords

computational complexity; timed automata; model checking; formal methods; probabilistic systems

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

EXPTIME-complete Decision Problems for Modal and Mixed Specifications, Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties, Expected reachability-time games, Verification and control for probabilistic hybrid automata with finite bisimulations, Verification and Control of Probabilistic Rectangular Hybrid Automata, Concavely-Priced Probabilistic Timed Automata, Strict Divergence for Probabilistic Timed Automata, Modal and mixed specifications: key decision problems and their complexities

Uses Software

• PRISM

Cites Work

• Optimal control of diffusion processes with reflection
• A theory of timed automata
• Automatic verification of real-time systems with discrete probability distributions.
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Alternation
• The complexity of probabilistic verification
• Termination of Probabilistic Concurrent Program
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item