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

Serenella  Cerrito; Amelie  David; Valentin Goranko

doi:10.1007/978-3-319-08587-6_21

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

Serenella Cerrito, Amelie David, Valentin Goranko

Department of Applied Mathematics and Computer Science

Université d'Évry Val-d'Essonne

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Automated Reasoning. Proceedings
Volume	8562
Publisher	Springer
Publication date	2014
Pages	277–291
ISBN (Print)	978-3-319-08586-9
ISBN (Electronic)	978-3-319-08587-6
DOIs	https://doi.org/10.1007/978-3-319-08587-6_21
Publication status	Published - 2014
Event	7th International Joint Conference on Automated Reasoning - Vienna, Austria Duration: 19 Jul 2014 → 22 Jul 2014 Conference number: 7

Conference

Conference	7th International Joint Conference on Automated Reasoning
Number	7
Country/Territory	Austria
City	Vienna
Period	19/07/2014 → 22/07/2014

Series	Lecture Notes in Computer Science
Volume	8562
ISSN	0302-9743

Access to Document

10.1007/978-3-319-08587-6_21

OpenUrl availability

Full text

Cite this

@inproceedings{b137e9b7b3284db69812d250ea6730c1,

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

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.",

author = "Serenella Cerrito and Amelie David and Valentin Goranko",

year = "2014",

doi = "10.1007/978-3-319-08587-6_21",

language = "English",

isbn = "978-3-319-08586-9",

volume = "8562",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "277–291",

booktitle = "Automated Reasoning. Proceedings",

note = "7th International Joint Conference on Automated Reasoning, IJCAR ; Conference date: 19-07-2014 Through 22-07-2014",

}

Cerrito, S, David, A & Goranko, V 2014, Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+. in Automated Reasoning. Proceedings. vol. 8562, Springer, Lecture Notes in Computer Science, vol. 8562, pp. 277–291, 7th International Joint Conference on Automated Reasoning, Vienna, Austria, 19/07/2014. https://doi.org/10.1007/978-3-319-08587-6_21

Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+. / Cerrito, Serenella ; David, Amelie ; Goranko, Valentin.
Automated Reasoning. Proceedings. Vol. 8562 Springer, 2014. p. 277–291 (Lecture Notes in Computer Science, Vol. 8562).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

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

AU - Cerrito, Serenella

AU - David, Amelie

AU - Goranko, Valentin

N1 - Conference code: 7

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-08587-6_21

DO - 10.1007/978-3-319-08587-6_21

M3 - Article in proceedings

SN - 978-3-319-08586-9

VL - 8562

T3 - Lecture Notes in Computer Science

SP - 277

EP - 291

BT - Automated Reasoning. Proceedings

PB - Springer

T2 - 7th International Joint Conference on Automated Reasoning

Y2 - 19 July 2014 through 22 July 2014

ER -

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

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this