Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+

Serenella Cerrito, Amelie David, Valentin Goranko

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL+ of the full Alternating time temporal logic ATL∗. The method extends in an essential way a previously developed tableaux-based decision method for ATL and works in 2EXPTIME, which is the optimal worst case complexity of the satisfiability problem for ATL+. We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL+ formulae can reduce the complexity of the satisfiability problem.
Original languageEnglish
Title of host publicationAutomated Reasoning. Proceedings
Volume8562
PublisherSpringer
Publication date2014
Pages277–291
ISBN (Print)978-3-319-08586-9
ISBN (Electronic) 978-3-319-08587-6
DOIs
Publication statusPublished - 2014
Event7th International Joint Conference on Automated Reasoning - Vienna, Austria
Duration: 19 Jul 201422 Jul 2014
Conference number: 7

Conference

Conference7th International Joint Conference on Automated Reasoning
Number7
CountryAustria
CityVienna
Period19/07/201422/07/2014
SeriesLecture Notes in Computer Science
Volume8562
ISSN0302-9743

Fingerprint Dive into the research topics of 'Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+'. Together they form a unique fingerprint.

Cite this