State explosion in almost-sure probabilistic reachability

We show that the problem of reaching a state set with probability 1 in probabilisticnondeterministic systems operating in parallel is EXPTIME-complete. We then show that this probabilistic reachability problem is EXPTIME-complete also for probabilistic timed automata. Key words: probabilistic systems, model checking, computational complexity, formal methods, timed automata

• Type: Journal
• Year: 2007
• Where: IPL
• Authors: François Laroussinie, Jeremy Sproston
• Keywords: IPL 2007, Probabilistic Reachability Problem, Probabilistic Systems, Probabilistic Timed Automata