Search

• < Previous
• 1
• Next >

High-level Counterexamples for Probabilistic Automata

Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited&nbsp;[&hellip;]