Alternating-time temporal logic ATL with finitely bounded semantics

We study a variant ATL_FB 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 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.