## Alternating-time temporal logic ATL with finitely bounded semantics

Research output: Contribution to journal › Article › Scientific › peer-review

### Standard

**Alternating-time temporal logic ATL with finitely bounded semantics.** / Goranko, Valentin; Kuusisto, A.; Rönnholm, R.

Research output: Contribution to journal › Article › Scientific › peer-review

### Harvard

*Theoretical Computer Science*. https://doi.org/10.1016/j.tcs.2019.05.029

### APA

*Theoretical Computer Science*. https://doi.org/10.1016/j.tcs.2019.05.029

### Vancouver

### Author

### Bibtex - Download

}

### RIS (suitable for import to EndNote) - Download

TY - JOUR

T1 - Alternating-time temporal logic ATL with finitely bounded semantics

AU - Goranko, Valentin

AU - Kuusisto, A.

AU - Rönnholm, R.

N1 - dupl=49136187

PY - 2019

Y1 - 2019

N2 - We study a variant ATLFB of the alternating-time temporal logic ATL with a non-standard, ‘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 ATLFB 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 ATLFB. 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 ATLFB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATLFB and prove its soundness and completeness.

AB - We study a variant ATLFB of the alternating-time temporal logic ATL with a non-standard, ‘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 ATLFB 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 ATLFB. 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 ATLFB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATLFB and prove its soundness and completeness.

KW - Alternating-time temporal logic

KW - Axiomatization

KW - Completeness

KW - Decidability

KW - Finitely bounded semantics

KW - Tableaux

U2 - 10.1016/j.tcs.2019.05.029

DO - 10.1016/j.tcs.2019.05.029

M3 - Article

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -