State explosion in almost-sure probabilistic reachability

DOI10.1016/j.ipl.2007.01.003zbMath1184.68318OpenAlexW2028222307MaRDI 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 complexitytimed automatamodel checkingformal methodsprobabilistic systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (8)

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

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: State explosion in almost-sure probabilistic reachability