State explosion in almost-sure probabilistic reachability

DOI10.1016/J.IPL.2007.01.003zbMATH Open1184.68318OpenAlexW2028222307MaRDI QIDQ846015FDOQ846015

Authors: François Laroussinie, Jeremy Sproston 

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

Recommendations

• scientific article; zbMATH DE number 1864589
• On Almost-Sure Properties of Probabilistic Discrete Event Systems
• Model checking of probabilistic and nondeterministic systems
• On probabilistic timed automata.
• The complexity of probabilistic verification

zbMATH Keywords

computational complexitymodel checkingformal methodstimed automataprobabilistic systems

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (12)

• Modal and mixed specifications: key decision problems and their complexities
• Title not available (Why is that?)
• Verification and control for probabilistic hybrid automata with finite bisimulations
• Verification and control of probabilistic rectangular hybrid automata
• Expected reachability-time games
• Reachability in networks of register protocols under stochastic schedulers
• Zero-reachability in probabilistic multi-counter automata
• Strict Divergence for Probabilistic Timed Automata
• EXPTIME-complete decision problems for modal and mixed specifications
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Concavely-Priced Probabilistic Timed Automata
• Tackling continuous state-space explosion in a Markovian process algebra

Uses Software

• PRISM

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

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