Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Alternating-time temporal logic ATL with finitely bounded semantics
Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
Number of Authors: 32019 (English)In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 797, p. 129-155Article in journal (Refereed) Published
Abstract [en]

We study a variant ATL(FB) of the alternating-time temporal logic ATL with a nonstandard, 'finitely bounded' semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL(FB) differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL(FB). The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL(FB) and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL(FB) and prove its soundness and completeness. 

Place, publisher, year, edition, pages
2019. Vol. 797, p. 129-155
Keywords [en]
Alternating-time temporal logic, Finitely bounded semantics, Tableaux, Decidability, Axiomatization, Completeness
National Category
Computer and Information Sciences Philosophy
Identifiers
URN: urn:nbn:se:su:diva-176664DOI: 10.1016/j.tcs.2019.05.029ISI: 000497889700006OAI: oai:DiVA.org:su-176664DiVA, id: diva2:1380244
Available from: 2019-12-18 Created: 2019-12-18 Last updated: 2019-12-18Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Goranko, Valentin
By organisation
Department of Philosophy
In the same journal
Theoretical Computer Science
Computer and Information SciencesPhilosophy

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 2 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf