The STUDIA UNIVERSITATIS BABEŞ-BOLYAI issue article summary

The summary of the selected article appears at the bottom of the page. In order to get back to the contents of the issue this article belongs to you have to access the link from the title. In order to see all the articles of the archive which have as author/co-author one of the authors mentioned below, you have to access the link from the author's name.

The Alternating-Time Temporal Logic (ATL) is interpreted over the game structures. 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. In this paper we will use an algebraic approach to implement an ATL model checker. Our tool is implemented in client-server paradigm: ATL Designer, the client tool, allows an interactive construction of concurrent game structures as a directed multi-graph and the ATL Checker, the core of our tool, represents the server part and is published as Web service. The ATL Checker includes an algebraic compiler implemented with ANTLR (Another Tool for Language Recognition) support. The main function of the Web service is to parse a given formula, find the set of nodes in which the formula is satisfied and return the result to the user.

Key words and phrases, algebraic compiler, ATL model checking, ANTLR, Web services.