Implementing an ATL model checker tool using relational algebra concepts

Alternating-Time Temporal Logic (ATL) is a branching-time temporal logic that naturally describes computations of open systems. An open system interacts with its environment and its behavior depends on the state of the system as well as the behavior of the environment. ATL model-checking is a well-established technique for verifying that a formal model representing such a system satisfies a given property. In this paper we describe a new interactive model checker environment based on algebraic approach. Our tool is implemented in client-server paradigm. The client part allows an interactive construction of ATL models represented by concurrent game structures as directed multi-graphs. The server part embeds an ATL model checking algorithm implemented using ANTLR and Relational Algebra expressions translated into SQL queries. The server side of our tool was published as a Web service exposing its functionality to various clients through standard XML interfaces.