Generating an ATL Model Checker using an Attribute Grammar

TL;DR

This paper presents a novel approach to developing an ATL model checker by using attribute grammars to generate the language of ATL formulas, integrating formal semantics with implementation techniques.

Contribution

It introduces an ATL attribute grammar formalism for specifying model checking semantics and demonstrates its implementation using ANTLR, relational databases, and web services.

Findings

Formal ATL attribute grammar defined for model checking

Implementation of ATL model checker using ANTLR and semantic actions

Performance evaluation on large ATL models with database and web services

Abstract

In this paper we use attribute grammars as a formal approach for model checkers development. Our aim is to design an ATL (Alternating-Time Temporal Logic) model checker from a context-free grammar which generates the language of the ATL formulas. An attribute grammar may be informally defined as a context-free grammar which is extended with a set of attributes and a collection of semantic rules. We use an ATL attribute grammar for specifying an operational semantics of the language of the ATL formulas by defining a translation into the language which describes the set of states from the ATL model where the corresponding ATL formulas are satisfied. We provide a formal definition for an attribute grammar used as input for Another Tool for Language Recognition (ANTLR) to generate an ATL model checker. Also, the technique of implementing the semantic actions in ANTLR is presented, which is the concept of connection between attribute evaluation in the grammar that generates the language of ATL formulas and algebraic compiler implementation that represents the ATL model checker. The original implementation of the model checking algorithm is based on Relational Databases and Web Services. Several database systems and Web Services technologies were used for evaluating the system performance in verification of large ATL models.