Rich Counter-Examples for Temporal-Epistemic Logic Model Checking

Simon Busard, Charles Pecheur

Model checking verifies that a model of a system satisfies a given property, and otherwise produces a counter-example explaining the violation. The verified properties are formally…