Generation and Exploitation of Counterexamples in Stochastic Models

Reactive synthesis is a core problem in formal methods. Given a system to control trying to enforce some specification within an uncontrollable environment, it aims at the automated construction of provably-safe system controllers. Synthesis algorithms and tools permit to construct a suitable (formal) controller if one exists, i.e., if the specification can be enforced. If not the case, they simply tell us that no such controller exists. However, from a practical standpoint we need to help practitioners understand why their attempt failed. This can be done by generating counterexamples which carry information on why the synthesis process did not work. The generation of counterexamples has been studied in basic stochastic models such as Markov chains and also Markov decision processes (MDPs) which contain both non-deterministic choices and stochastic transitions. However, this has only been studied for verification: counterexamples can be used to prove the existence of a bad controller, but not the non-existence of a suitable one. In this talk, we tackle the generation of counterexamples for MDPs in the synthesis mindset.