Rezumat articol ediţie STUDIA UNIVERSITATIS BABEŞ-BOLYAI

În partea de jos este prezentat rezumatul articolului selectat. Pentru revenire la cuprinsul ediţiei din care face parte acest articol, se accesează linkul din titlu. Pentru vizualizarea tuturor articolelor din arhivă la care este autor/coautor unul din autorii de mai jos, se accesează linkul din numele autorului.

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.