MOVES Seminar 21. September 2006

Tingting Han

 

Counterexamples in fully probabilistic systems

 

Abstract:
 

The talk considers algorithms for counterexample generation of bounded
and unbounded probabilistic reachability properties in fully
probabilistic systems. We consider two problems that are aimed to
provide useful diagnostic feedback for the violation: generating
strongest evidences and smallest, most indicative counterexamples.
Finding a strongest evidence (i.e., the most probable path) violating
(bounded) until formula is shown to be reducible to a single-source
(hop-constrained) shortest path problem. Counterexamples of smallest
size that are mostly deviating from the requited probability bound can
be computed by adopting (partially new hop-constrained) k shortest paths
algorithms that dynamically determine k.