test
Search publications, data, projects and authors

Thesis

English

ID: <

10670/1.5f5ih8

>

Where these data come from
Towards Synthesizing Open Systems : Tableaux For Multi-Agent Temporal Logics
Keywords

Abstract

In this thesis, we try to provide automated tools to design safe open systems. Open systems, which can be viewed as multi-agent systems, may be specified in ATL. The logic ATL has been especially introduced for that purpose. There exist two relevant extensions of ATL, namely ATL+ and ATL* (ATL+ being a restriction of ATL*).ATL+ allows Boolean combination of temporal operators, and ATL* also allows nesting of temporal operators. The tableau-based decision procedure for ATL is a constructive method to test the satisfiability of a given specification. It is constructive in the sense that it is possible to extract a model from the obtained tableau, whenever the root formula is indeed satisfiable. In this thesis, we propose two tableau-based decision procedures for ATL+ and ATL*, as well as an implementation of these procedures. Our procedures are sound, complete and optimal. Indeed, our two procedures run in 2Exptime. Up to our knowledge our implementation is the first running tool to decide satisfiability of both ATL and ATL* formulae. In the perspectives of this thesis, we discuss how it is possible to improve the extraction of models from tableaux for ATL, ATL+ and ATL*. We would like to obtain relatively small models at the end.

Your Feedback

Please give us your feedback and help us make GoTriple better.
Fill in our satisfaction questionnaire and tell us what you like about GoTriple!