A Cutoff Technique for the Verification of Parameterised Interpreted Systems with Parameterised Environments / 2013
Panagiotis Kouvaros, Alessio Lomuscio

We put forward a cutoff technique for determining the number of agents that is sufficient to consider when checking temporal-epistemic specifications on a system of any size. We identify a special class of interleaved interpreted systems for which we give a parameterised semantics and an abstraction methodology. This enables us to overcome the significant limitations in expressivity present in the state-of-the-art. We present an implementation and discuss experimental results.