Experiments in Infinite States Verification in Game-Theoretic Logics

Many practical problems where the environment is not in the system’s control such as service orches-tration and contingent and multi-agent planning can be modelled in game-theoretic logics (e.g. ATL). But most work on verification methods for such logics is restricted to finite state cases. [De Gia-como et al., 2010] develops a situation calculus-based logical framework for representing such infi-nite state game-type problems together with a veri-fication method based on fixpoint approximates and regression. In this paper, we describe some case studies we have done to evaluate this method. We specify some example domains and show that the verification method does allow us to verify vari-ous properties. We also find some examples where the method must be extended to exploit informa-tion about the initial state and state constraints in order to work. Our example domains can be used to evaluate other infinite state verification methods.