infinite states verification in game-theoretic logics

Many practical problems where the environment is not in the system's control such as service orchestration and contingent and multi-agent planning can be modelled in game-theoretic logics. This thesis demonstrates that the verification techniques based on regression and fixpoint approximation introduced in De Giacomo, Lesperance and Pearce [DLP10] do work on several game-theoretic problems. De Giacomo, Lesperance and Pearce [DLP10] emphasize that their study is essentially theoretical and call for complementing their work with experimental studies to understand whether these techniques are effective in practical cases. Several example problems with varying properties have been developed and, although not exhaustive nor complete,, our results nevertheless demonstrate that the techniques work on some problems. Our results show that the methods introduced in [DLP10] work for infinite domains where very few verification methods are available and allow reasoning about a wide range of game problems. Our examples also demonstrate the use of a rich language for specifying temporal properties proposed in [DLP10]. While classical model checking is well known and utilized, it is mostly restricted to finite-state models. A important aspect of the work is the demonstration of the use and effectiveness of characteristic graphs (ClaBen and Lakemeyer [CL08]) in verifying properties of games in infinite domains. A special-purpose programming language GameGolog proposed in De Giacomo, Lesperance and Pearce [DLP10] allows such game-theoretic systems to be specified procedurally at a high-level of abstraction. We show its practicality to model game structures in a convenient way that combines declarative and procedural elements. We provided examples to show the verification of GameGolog specifications using characteristic graphs. This thesis also proposes a refinement to the formalism in [DLP10] to incorporate action constraints as a mechanism to incorporate user strategies and for the modeller to supply heuristic guidance in temporal property verification. It also presents an implementation of evaluation-based fixpoint verifier that handles Situation Calculus game structures, as well as GameGolog specifications, for temporal property verification in the initial or a given situation. The verifier supports player action constraints