Alternating-time Temporal Logic on Finite Traces

1 Introduction

There is a long tradition in logic-based approaches to Artificial Intelligence (AI) to model the evolution of a system on the basis of an infinite sequence of states [Alur et al., 2002; Mogavero et al., 2014]. This approach is heavily influenced by works in reactive systems and related temporal logic approaches, where a computing system is conceived as an entity that interacts with the environment indefinitely [Harel and Pnueli, 1985].

While this modelling choice has long proven to be valuable in regards to AI as well, many areas of AI are typically characterised by executions that terminate. For example, plays in classic ludic games are finite, phases in negotiation and coordination protocols are finite [Jennings et al., 2001], business processes are naturally modelled using finite traces [Pesic et al., 2010], and in automated planning successful executions are often finite (e.g., in classical planning and in strong solutions to fully observable non-deterministic planning) [Geffner and Bonet, 2013].

In this paper we introduce ATL∗f , Alternating-time Temporal Logic for the modelling and verification of multi-agent systems with finite computations. The syntax is the same as ATL∗ [Alur et al., 2002], while the semantics is novel. Precisely, a model comes equipped with a special set of final states F and strategic quantifiers only range on paths that end in a state of F. We automatically get finite-trace semantics for the natural syntactic fragments of ATL∗f , i.e., ATLf , CTLf , and CTL∗f , the finite-trace variants of the branchingtime temporal logics CTL∗ and CTL, that we also study. We use ordinary finite-automata, operating on finite words, instead of infinite words or trees, to give optimal algorithms for the model-checking problems of these logics (with perfect recall).

In particular, our algorithms sidestep intrinsic difficulties of model-checking ATL∗ that are due to automata operating over infinite words or trees, e.g., determinisation of B¨uchi automata, which has been resistant to efficient implementation [Tsai et al., 2014], or emptiness of alternating parity tree automata, which is conjectured to be in PTIME and known to be in NP and co-NP [Emerson et al., 2001]. There are algorithms that avoid determinisation or solving emptiness of alternating tree automata, notably Safraless decision procedures [Kupferman et al., 2006; Filiot et al., 2011]. These algorithms, while undeniably elegant, are still complex and tailored to reasoning about infinite traces. In contrast, just like the procedures in [De Giacomo and Vardi, 2015], our algorithms are extremely simple: they only involve automata operating on finite words, and simple standard constructions on these such as the classic subset construction for determinisation. We consider this a significant technical improvement.

Related Work. In recent years, several contributions in AI have focused on variants of LTL to reason about finitecomputation systems. Along this line, well studied is LTLf , a variant of the Linear-time Temporal Logic LTL where formulas are interpreted over finite traces (see [De Giacomo and Vardi, 2015] for a survey). This logic has proved particularly useful in planning [Bacchus and Kabanza, 2000; Baier and McIlraith, 2006; Gerevini et al., 2009; De Giacomo and Vardi, 2013; Camacho et al., 2017], and in business process modelling [Pesic et al., 2010; Montali et al., 2010; De Giacomo et al., 2014a]. Moreover, recent work [De Giacomo et al., 2014b] has compared the finite- and infinite-trace semantics for LTL, showing surprising differences both at the modelling and verification levels.

There are two standard semantics for LTL, i.e., over traces and over transition systems [Baier and Katoen, 2008]. In [De Giacomo and Vardi, 2013] model-checking LTLf is considered for semantics over traces, i.e., models are of the form π0π1 · · · πn where πi is a set of atomic proposition. In contrast, our models of ATL∗f are transition systems. This opens up the possibility of modelling complex strategic and branching-time properties of transition systems rather than just properties of traces. Furthermore, thanks to the strategic operators in ATL∗f , we reduce LTLf synthesis [De Giacomo and Vardi, 2015] to ATL∗f model checking (see Section 4).

To the best of our knowledge finite traces have already been considered in the context of branching-time temporal logics, but never for logics of strategies. In [Vardi and Stockmeyer, 1985] a finite-trace semantics for CTL∗ is introduced. This formal account, which is a special case of our semantics, is analysed briefly in Remark 2. The expressivity of CTL∗ on parameterised sets of traces, which includes the set of finite traces, has been investigated in [Emerson and Halpern, 1986], but the related model-checking problem has not been tackled as far as we know. Our framework is also related to Game Logic [Pauly and Parikh, 2003], which was designed to reason about games, and has applications to protocol analysis, e.g., cake cutting and secret exchange. However, Game Logic is a generalisation of PDL from programs to games, whereas our framework is in the tradition of branching and alternatingtime temporal logics. Moreover, its model checking problem was studied for the two-player case only. Motivated by multiagent strategic reasoning over finite traces, [Gutierrez et al., 2017] introduced and studied iterated Boolean games with LDL goals over finite traces. Differently from us, they consider the problem of the existence of Nash equilibria.

Lastly, [Kong and Lomuscio, 2018] developed a verification approach for finite traces of multi-agent systems against LDLfK specifications. Their approach focuses on the verification algorithms and the resulting implementation. In contrast, we are here concerned with the theoretical underpinning of an approach supporting the strategic interplay of the agents on finite executions.

2 Concurrent Game Systems with Final States

In this section we introduce concurrent game structures (CGS) endowed with final states. Given a set X of elements, let u ∈ Xω ∪ X+ denote an infinite or non-empty finite sequence on X. Then, we write ui for its (i + 1)-th element, i.e., u = u0u1 . . ., and |u| for its length, with |u| = ∞ for u ∈ Xω . The first element of u is denoted by first(u), and its last by last(u). We write u≥i for its suffix uiui+1 . . . starting in ui, and u≤i for its prefix u0 . . . ui. The empty sequence is denoted by ϵ. For a vector v ∈ ∏i Xi we denote its i-th element by v(i).

We now introduce our class of relevant models.

Definition 1 (CGS with final states). A concurrent game structure (CGS) with final states is a tuple G = 〈Ag , AP, {Acta}a∈Ag , S, s0, F, δ, λ〉 where:

• Ag is the finite non-empty set of agent names;
• AP is the finite non-empty set of atomic propositions;
• Acta is the finite non-empty set of actions for a ∈ Ag;
• S is the finite non-empty set of states; with initial state s0 ∈ S, and the non-empty set F ⊆ S of final states;
• δ : S × Jact → S is the transition function, where Jact = ∏a∈Ag Acta is the set of joint actions;
• λ : S → 2AP is the labelling function that assigns a set of atoms to each state s.

Def. 1 extends the standard definition of CGS [Alur et al., 2002] by explicitly identifying a set F ⊆ S of final states. Final states can be thought of as end states in games (e.g., all configurations in which a king is in check-mate in chess), or goal states in plans, or remarkable states along a system's execution. Final states allow us to talk about plays that have both a start and an end.

A run (resp. history) is an infinite (resp. finite) sequence π ∈ S+ ∪Sω of states complying with the transition function, i.e., for every i < |π| there exists a joint action J ∈ Jact such that δ(πi, J) = πi+1. We denote with Run (resp. Hist) the set of all runs (resp. histories).

A path is a history π that ends in a final state, i.e., last(π) ∈ F. In the next section, we will define strategic quantifiers to range on paths, i.e., finite sequences ending in final states. We denote the set of all paths by Path.

A (perfect recall or memoryful) strategy for agent a is a function σa : Hist → Acta. A strategy σ is positional or memoryless if for all h, h′ ∈ Hist, last(h) = last(h′ ) implies σ(h) = σ(h′ ). The set of all memoryful (resp. memoryless) strategies is denoted as ΣR(G) (resp. Σr(G)). For A ⊆ Ag and y ∈ {R, r}, let σA : A → Σy(G) denote a joint strategy associating a (memoryful or memoryless) strategy σa with each agent a ∈ A.

For s ∈ S, a joint strategy σA, and x ∈ {∞, f}, we write outx(s, σA), called the infinite, resp. finite, outcomes of σA from s, for the set of runs, resp. paths, π ∈ Run∪Path such that π is consistent with s and σA. That is, π ∈ outx(s, σA) iff (i) π0 = s; (ii) for every i ≥ 0, there exists a joint action Ji ∈ Jact such that πi+1 ∈ δ(πi, Ji) and for every a ∈ A, Ji(a) = σA(a)(π≤i).

3 ATL∗ on Finite Traces

In this section we introduce the language ATL∗ and its fragment ATL [Alur et al., 2002]. Then, we interpret them on finite as well as infinite traces.

Syntax Fix finite sets AP of atomic propositions (atoms) and Ag of agents. The state (ϕ) and path (ψ) formulas over AP and Ag are built using the following grammar:

where p ∈ AP and A ⊆ Ag .

The class of ATL∗ formulas is the set of state formulas generated by the grammar. The temporal operators are X (read "next") and U (read "until"). The strategy quantifier is 〈〈A〉〉 (read "the agents in A can enforce . . . "). We introduce the following abbreviations: [[A]]ψ ::= ¬〈〈A〉〉¬ψ (read "no matter what the agents in A do . . . "), ˜Xψ ::= ¬X¬ψ (read "weak next"), and ψRψ′ ::= ¬(¬ψU¬ψ′ ) (read "releases"), Fψ ::= trueUψ (read "eventually") and Gψ ::= falseRψ (read "globally").

Hereafter we consider also the ATL fragment of ATL∗ . State formulas are built in the same way, whereas path formulas ψ are defined as follows:

Notice that operators ˜X and R have to be assumed as primitive now. We discuss the reason why in Remark 4.

In the following we also consider the CTL and CTL∗ fragments of ATL and ATL∗ respectively. Specifically, in CTL/CTL∗ we only allow the empty coalition ∅ in strategic operators. Further, we use the usual abbreviations Aψ ::= 〈〈∅〉〉ψ and Eψ ::= ¬A¬ψ ≡ [[∅]]ψ.

Finally, we introduce the LTL fragment of CTL∗ as the set of path formulas generated by the grammar: ψ ::= p | ¬ψ | ψ ∧ ψ | Xψ | ψUψ, where p ∈ AP.

We provide all these different languages with a semantics based on finite traces.

Semantics Fix a CGS G with final states. For x ∈ {∞, f} and y ∈ {R, r}, we simultaneously define, by induction on the structure of formulas, the relations (G, s) |=xy ϕ, where s ∈ S and ϕ is a state formula, and (G, π) |=xy ψ where π ∈ Run if x = ∞ and π ∈ Path if x = f , and ψ is a path formula:

For a state formula ϕ, we write G |=xy ϕ to mean that (G, s0) |=xy ϕ; whereas ϕ is a validity, or |=xy ϕ, iff G |=xy ϕ for every CGS G with final states.

We consider the following sets of validities: For x ∈ {∞, f} and y ∈ {R, r}, let

Notice that for x = ∞we obtain the standard semantics for ATL∗ and ATL on infinite traces [Alur et al., 2002]; while y ∈ {R, r} discriminates between the perfect- and imperfectrecall variant. We will drop the subscripts when they are clear from the context.

We now unpack the meaning of the strategic operators.

Remark 1. In standard ATL∗ (x = ∞, y = R) we have validities 〈〈Ag〉〉ψ ↔ [[∅]]ψ and [[Ag]]ψ ↔ 〈〈∅〉〉ψ. However, on finite traces we only have 〈〈Ag〉〉ψ → [[∅]]ψ and 〈〈∅〉〉ψ → [[Ag]]ψ, as the converses fail. Indeed, for x = f, y = R:

1. 〈〈Ag〉〉ψ is true at state s iff there is some infinite path π starting in s such that every prefix of π ending in a final state in F satisfies ψ.
2. [[Ag]]ψ is true at state s iff for all infinite paths π starting in s, there is some prefix of π ending in a final state in F, that satisfies ψ.
3. Aψ defined as 〈〈∅〉〉ψ is true at state s iff all finite paths starting in s and ending in F satisfy ψ.
4. Eψ defined as [[∅]]ψ is true at state s iff that there exists a finite path starting in s, ending in F, that satisfies ψ.

Further, for x = f, y = r only the ⇒-implications of (1) and (2) hold, as memoryless strategies may restrict the set of paths produced (whereas (3) and (4) still hold).

We now illustrate our framework with a simple scenario.

Example 1. Consider any ludic game that has a definite end and/or states in which something "important" happens. E.g., in chess, a "checkmate" is one way to signal the end of the game, and a "check" signals that the opponent's King is under threat. We can model such games as CGS whose final states correspond to the end states or the "important" states. 1 Then, e.g., if the final states in the CGS corresponds to "check", a formula of the form 〈〈{Black}〉〉GFQueen says that the Black player has a strategy ensuring that whenever "check" occurs, the black queen is still on the board.

Discussion We now make some remarks that motivate and discuss the syntax and semantics of ATL∗ on finite traces, i.e., for x = f .

We begin by discussing the relationship between our CTL∗fR and a previous definition of CTL∗ on finite traces.

Remark 2. In [Vardi and Stockmeyer, 1985] a semantics for CTL∗ on finite traces is put forward. Specifically, path quantifiers range on all finite paths starting from a given state s, including the trivial path π = 〈s〉. Observe that we can mimic such an interpretation in CGS with final states by assuming that F = S. However, such a semantic choice validates peculiar CTL∗ formulas includingAFϕ↔ϕandEGϕ↔ϕ. As a result, whenever path quantifiers range unrestrictedly over all finite paths, modalities AF and EG collapse to truth in the current state. We stress that nothing similar is the case in the semantics we propose, in particular AF and EG remain distinct.

We now discuss, at the level of validities, the difference between perfect and imperfect recall.

Remark 3. It is well-known that, for infinite traces, recall does not impact validities of ATL, i.e., ATL∞R = ATL∞r, whereas it does make a difference for ATL∗ , i.e., ATL∗∞r ⊂ ATL∗∞R [Alur et al., 2002]. Here we state without proof that similar results hold also for our semantics:

Thus, ATL and ATL∗ have the same distinguishing power as regards perfect/imperfect recall both on infinite and on finite traces.

Now we discuss the reason we chose the syntax of ATL to include ˜X, the dual of X.

Remark 4. It is known that, differently from the case of infinite traces, on finite traces the next operator X is not selfdual. In particular, according to the semantics for |=f given in [De Giacomo and Vardi, 2015] in LTLf we have that

This remark justifies the introduction of weak next ˜Xψ as ¬X¬ψ (thus, e.g., differently from the case of infinite traces, 〈〈A〉〉 ˜Xϕ is no longer equivalent to 〈〈A〉〉Xϕ).

1 Of course such games may have huge state spaces that require additional techniques to analyse. This important dimension, however, is out of the scope of this paper.

Finally, in ATLf (for each type of recall r,R) we can introduce operators involving [[A]] as follows:

Finally, we present fixed points for formulas 〈〈A〉〉ψ1 Uψ2 and 〈〈A〉〉ψ1 Rψ2 in ATL. Such validities are relevant as symbolic model checking algorithms for ATL are based on similar fixed points.

Remark 5. The following formulas are validities in ATLf (for each type of recall r,R):

We conclude by remarking that on infinite traces 〈〈A〉〉⊥ is equivalent to ⊥, which is not the case on finite traces. In fact, on finite traces 〈〈A〉〉⊥ means that there exists a strategy for coalition A with an empty set of outcomes.

Model Checking We now state the main decision problem tackled in this work.

Definition 2 (Model Checking). Given a CGS G with final states and a formula ϕ, model checking G against ϕ on infinite (resp. finite) traces, with perfect (resp. imperfect) recall is the following decision problem: decide whether G |=xy ϕ for x = ∞ (resp. x = f ) and y = R (resp. y = r).

Table 1 recalls the complexity of the model-checking problem for the logic ATL∗∞R and some of its fragments. Citations to the original papers are given.

4 Complexity of Model Checking

In this section we explore the computational complexity of model checking ATL∗ (and its fragments) over finite traces and under the perfect-recall assumption. See Table 2 for a summary of the results and their corresponding references.

For the rest of this section we assume y = R and do not write this subscript.

4.1 Upper Bounds

We solve the model-checking problem for ATL∗f by using an automata-theoretic approach. Since our paths are finite, we only need to use ordinary automata, i.e., deterministic word automata (DFW), non-deterministic word automata (NFW) [Hopcroft and Ullman, 1979], instead of ω-regular automata. This considerably simplifies the constructions. Overall, we reduce the problem (G, s) |= ϕ to model checking a game with an LTLf objective ψ; in turn, this can be solved by converting ψ into a DFW accepting the models of ψ (the DFW might be doubly-exponentially larger than the formula), then taking the product of the resulting DFW with the structure G to obtain a safety game that, in turn, can be solved by using the standard fix-point algorithm linearly in the size of the game. The rest of the section explores all the relevant cases in detail.

We begin with a special case that serves as a building block, i.e., (G, s) |=f 〈〈A〉〉ψ where ψ is an LTLf formula. The algorithm is presented in Figure 1. Intuitively, this corresponds to solving a game with the LTLf objective ψ: the coalition A plays a game on a graph that simulates G and a DFW for ψ; it is trying to enforce that every play from s stays "safe", i.e., in states such that if the corresponding state of G is in F then the corresponding state of the DFW is accepting (this captures the semantics of 〈〈A〉〉 which relativises paths to be those ending in F ).

Algorithm: GameSolving(G, A, ψ) Input: CGS G (states S), agents A ⊆ Ag, LTLf formula ψ. Output: The set X ⊆ S such that s ∈ X iff (G, s) |=f 〈〈A〉〉ψ.

1. Convert ψ into an equivalent NFW.
2. Convert the NFW into an equivalent DFW (D, d0, ∆, F ′ ).
3. Form the product edge-labelled graph on states S ×D.
4. Form the set Safe ⊆ S ×D as consisting of (s, d) such that s ∈ F implies d ∈ F ′ .
5. Put s ∈ X iff coalitionAcan ensure the play in the product, starting in (s,∆(d0, λ(s))), always stays in Safe.

Figure 1: Algorithm for solving games with LTLf objectives in double-exponential time.

Proposition 1. Model-checking ATL∗f formulas of the form 〈〈A〉〉ψ where ψ is an LTLf -formula is in 2EXPTIME. In particular, it is doubly-exponential in ψ and polynomial in G.

Proof. The overall structure of the proposed algorithm is presented in Figure 2. We give some more details.

For step 1, we use the adaptation of the classic VardiWolper construction to finite words, e.g. [De Giacomo and Vardi, 2015], to get an NFW that accepts all the traces (over atoms AP, i.e., alphabet 2AP ) that satisfy ψ. The number of states of the NFW is at most exponential in the size of the formula.

For step 2, we apply the standard subset construction for determinising NFW [Rabin and Scott, 1959] to get a DFW with state set D, initial state d0 ∈ D, transition function ∆ : D×

Algorithm: ModelChecking(G, ϕ)

Input: CGS G, ATL∗f formula ϕ

Output: The set X ⊆ S such that s ∈ X iff (G, s) |= ϕ.

1. Introduce a new atom pϕ and, for each state s, label s by pϕ (i.e., add pϕ to λ(s)) as follows:
2. (a) If ϕ = p ∈ AP then label s by pϕ iff p ∈ λ(s).
3. (b) If ϕ = ¬ϕ1 then label s by pϕ iff s is not in the set output by ModelChecking(G, ϕ1).
4. (c) If ϕ = ϕ1 ∧ϕ2 then label s by pϕ iff s is in the sets output by ModelChecking(G, ϕi) for i = 1, 2.
5. (d) If ϕ = 〈〈A〉〉ψ (so ψ is a path formula) then
6. Let Max(ψ) be the set of maximal statesubformulas of ψ.
7. For every ξ ∈ Max(ψ) label s by pξ if s is in the set output by ModelChecking(G, ξ).
8. Replace every occurrence in ψ of ξ ∈ Max(ψ) by pξ.
9. Label s by pϕ iff s is in the set output by GameSolving(G, A, ψ).
10. Output the set X of s ∈ S such that s is labelled by pϕ.

Figure 2: Recursive algorithm for model-checking ATLf that calls the GameSolving algorithm (Figure 1).

2AP → D, and final states F ′ ⊆ D. The number of states of the DFW is at most exponential in the number of states of the NFW.

For step 3, we form an edge-labelled graph: the vertices are S ×D, edge labels are of the form α : A → ∪aActa (i.e., a tuple of actions of the agents in A), and edges (s, d) α-→ (s′ , d′ ) if there is some joint action J such that (i) J(a) = α(a) for all a ∈ A, (ii) δ(s, J) = s′ , and (iii) ∆(d, λ(s′ )) = d′ .

For step 4 we build the set Safe of states of the product graph that the coalition A is trying to stay in.

For step 5 we introduce some notation regarding graphgames [Gr¨adel et al., 2002]. A safety game is a tuple (V,Σ,E, T) with: vertices V , actions Σ, labelled edges E ⊆ V ×Σ× V , and safety set T ⊆ V . Note that the graph from step 3 combined with the set from step 4 forms a safety game. Solving a safety game concerns deciding from which vertices v there is a strategy for the agent that ensures every path stays in T (similarly to model-checking the formula 〈〈A〉〉GSafe). This can be solved in linear time using the greatest fix-point of the operation Y ↦→ T ∩ Pre(Y ) where Pre(Y ) = {v ∈ V : ∃σ.∀w.E(v, σ,w) →w ∈ Y }.

We now provide an algorithm for model-checking ATL∗f , see Figure 2. It follows the standard approach for modelchecking ATL∗ [Alur et al., 2002], i.e., we inductively mark the states of the G by those state subformula that hold. The atomic case is immediate, and the Boolean operations are done inductively. For the strategic operator 〈〈A〉〉ψ we may assume, by induction, that ψ is an LTLf formula, and so we call the GameSolving algorithm in Figure 1. This gives:

Theorem 1. Model checking ATL∗f is in 2EXPTIME.

Now, suppose the algorithm is applied to formulas of ATLf . Then, in step 1(d) of the algorithm in Figure 2, the path formula ψ is of the form Xp′ , ˜Xp′ , p′ Up′′ or p′ Rp′′ where p′ , p′′ are atoms. So, the complexity of GameSolving(G, A, ψ) is polynomial (Proposition 1).

Theorem 2. Model checking ATLf , and thus also CTLf , is in polynomial time.

Finally, to solve model-checking of CTL∗f we make a slight change to the above algorithm. In step 1(d) of Figure 2, instead of calling GameSolving(G, ∅, ψ) (which costs doubleexponential time), we call the LTLf model-checking procedure described in Figure 3. The complexity analysis is described in the accompanying proof.

Algorithm: LTLfModelChecking(G, ψ)

Input: CGS G, LTLf formula ψ.

Output: The set X ⊆ S such that s ∈ X iff (G, s) |= 〈〈∅〉〉ψ.

1. Convert ψ into an equivalent NFW (N, I, ∆, F ′ ).
2. Form the product graph on states S ×N.
3. Form the set Safe of states (s, t) such that s ∈ F implies t ∈ F ′ .
4. Put s ∈ X iff every path starting from states of the form (s, n) for n ∈ I stays in Safe.

Figure 3: Algorithm for model-checking G against LTLf formulas.

Theorem 3. Model checking CTL∗f is in polynomial space.

Proof. We discuss the steps of the algorithm in Figure 3. In step 1, the NFW can be formed by using an adaptation of the classic Vardi-Wolper construction for finite words, e.g., [Vardi and Wolper, 1994]. Denote its states N, initial states I ⊆ N, transition relation ∆ ⊆ N ×2AP ×N, and final states F ′ ⊆ N. This can be built in polynomial space.

In step 2, the graph has states S ×N, and edges (s, n) → (s′ , n′ ) if there is some joint action J with s′ ∈ δ(s, J) and (n, λ(s′ ), n′ ) ∈ ∆.

In step 3, form the set Safe as described. In step 4, for s ∈ S and n ∈ I, we need to check that every path from (s, n) stays in Safe. This check can be done in logspace in the size of the graph. Since the graph is exponential, the whole algorithm runs in polynomial space.

4.2 Lower Bounds

We now supply the lower-bounds for model checking ATL∗f and its fragments. For CTLf and ATLf we reduce frommodelchecking CTL, known to be PTIME-hard [Clarke et al., 1986]; for CTL∗f we reduce frommodel-checking finite traces against LTLf formulas, known to be PSPACE-hard [De Giacomo and Vardi, 2013]; and for ATL∗f we reduce from LTLf synthesis, known to be 2EXPTIME-hard [De Giacomo and Vardi, 2015].

Theorem 4. Model checking CTLf (and thus ATLf ) is PTIME-hard.

Proof. The proof is almost identical to the one that shows that CTL model checking is PTIME-hard by reducing from CIRCUIT-VALUE, a problem that is PTIME-complete when restricted to circuits that are monotone (no negation), synchronized (connections between gates respect layers), and with proper alternation, see Section 3.2.1 of [Schnoebelen, 2003]. Adapt that proof by letting the final states be the sink nodes 0 and 1.

We now turn to the fragment CTL∗f . In [De Giacomo and Vardi, 2013], a trace-based semantics is given for LTLf . There, the model checking problem asks, given an LTLf formula ϕ and a finite trace π, to decide whether ϕ holds on π. We reduce this trace-based LTLf model-checking to our structure-based CTL∗f model-checking.

Theorem 5. Model-checking CTL∗f is PSPACE-hard.

Proof. Given π = π0π1π2 · · · πn-1, construct a CGS Gπ with final states as follows: Ag = {1}, AP are the atoms appearing in π, Act1 = {a} (i.e., there is only one action), S = {i : 0 ≤ i ≤ n} (the last state is used to make the transition function total), F = {n-1} (i.e., the second last state is final), δ(i, a) = i+1 if i < n, δ(n, a) = n, and λ(i) = πi for i < n, and λ(n) = ∅. Note that the complexity of this translation is linear, and for every LTLf formula and finite trace π, we have that ϕ holds on π iff Gπ |=f Aϕ.

Finally, we turn to the logic ATL∗f . We reduce from LTLf synthesis, known to be 2EXPTIME-complete [De Giacomo and Vardi, 2015]. Let X, Y be disjoint finite non-empty sets of Boolean variables. The LTLf realisability problem (for turn-based players) asks, given an LTLf formula ϕ over atoms X∪Y , to decide if there is a function c : (2X )+ → 2Y such that for every finite sequence X0X1 . . .Xn with Xi ⊆ X, the sequence (X0 ∪ c(X0))(X1 ∪ c(X0X1)) . . . (Xn ∪ c(X0X1 · · ·Xn)) satisfies ϕ. In this case we say ϕ is realisable. We now show how to reduce the LTLf realisability problem to ATL∗f model-checking.

Theorem 6. Model-checking ATL∗f is 2EXPTIME-hard.

Proof. The proof is similar to the proof that ATL∗ is 2EXPTIME-hard which reduces from LTL synthesis [Alur et al., 2002]. The main difference is to deal with the fact that in our semantics paths are finite and end in final states.

Let ϕ be an LTLf formula over atoms X ∪ Y . We define a CGS GX,Y with final states and an LTLf formula ϕd such that ϕ is realisable iff GX,Y |= 〈〈{2}〉〉XXϕd.

Define GX,Y with final states F = {2} × 2X∪Y as follows: Ag = {1, 2}, AP = F , S = ({1} × 2X ) ∪ F ∪ sinit, Act1 = 2X , Act2 = 2Y , s0 = sinit; labelling λ(s) = {s} for s ∈ F, and λ(s) = ∅ otherwise; and transitions: δ(sinit, (X′ , ·)) = (1,X′ ), δ((1,X′ ), (·, Y ′ )) = (2,X′ ∪ Y ′ ), and δ((2, ·), (X′ , ·)) = (1,X′ ) (where X′ ⊆ X, Y ′ ⊆ Y , and · stands for any set).

In words, the CGS models two players that take turns, with player 1 going first. On his turn player 1 chooses a subset of X, on her turn player 2 chooses a subset of Y , and the resulting sequence of sets of atoms (for traces ending in final states) is in the language ∅·(∅·{{z} : z ∈ F})∗ . For example, the finite word {x} · {x, y} over alphabet 2{x,y} with X =

{x}, Y = {y} corresponds to the sequence of states of GX,Y : sinit, (1, {x}), (2, {x}), (1, {x}), (2, {x, y}) whose labelling is ∅ · ∅ · {(2, {x})} · ∅ · {(2, {x, y})}.

Define the formula ϕd as follows: pd = p, (ϕ∧ϕ′ )d = ϕd∧ ϕ′d , (¬ϕ)d = ¬ϕd, (Xϕ)d = XXϕd, (ϕUϕ′ )d = (F → ϕd) U(F ∧ϕd). In words, ϕd simulates ϕ on the subsequence of the trace consisting of odd numbered positions.

Then, an LTLf formula ϕ over X ∪ Y is realisable iff GX,Y |= 〈〈{2}〉〉XXϕd. Regarding complexity, the formula ϕd is polynomial in the size of ϕ. On the other hand, just as in [Alur et al., 2002], LTLf synthesis is already 2EXPTIMEhard for fixed X and Y , and thus GX,Y has constant size.

5 Conclusions

Motivated by problems in AI rather than program verification, we defined a logic with the same syntax as ATL∗ but in which paths are finite instead of infinite. Precisely, a model is equipped with a special set F of final states and strategic quantifiers only account for paths that end in a state of F.

This definition is general enough to capture previous proposals for CTL∗ and LTL on finite traces, as well as synthesis of LTL on finite traces. Indeed, in Section 4 we showed how to reduce model-checking finite traces against LTLf formulas to model-checking CGS with final states against CTL∗f formulas (Theorem 5), and how to reduce LTLf synthesis to ATL∗f (with perfect recall) model-checking (Theorem 6). It follows that the formalism ATL∗f that we introduced is rich enough to express two fundamental decision problems about LTLf , and at no extra cost in terms of computational complexity.

Moreover, in previous proposals to reasoning about finite traces in structures [Vardi and Stockmeyer, 1985], it was assumed (in the language of this paper) that all states are final, which leads to validities such as AFϕ ↔ ϕ and EGϕ ↔ ϕ that are not intuitive or natural (see Remark 2). Our more refined semantics removes these undesirable validities.

Finally, we emphasise that, unlike algorithms for model checking ATL∗∞R (e.g., [Alur et al., 2002]), our algorithm for model-checking ATL∗fR does not use complex constructions on automata operating on infinite strings or infinite trees. In fact, we do not translate ATL∗fR (or its fragments) into ATL∗∞R. Instead, our algorithms only involve automata operating on finite words, and simple standard constructions on these, e.g., the classic subset construction for determinisation and a fix-point algorithm synthesising strategies.

In future work we plan to account also for the imperfect information agents might have about the environment as well as the state of other agents.

Acknowledgements

The authors acknowledge support of ANR JCJC Project SVeDaS (ANR-16-CE40-0021); the Royal Academy of Engineering; the Royal Society; and INDAM GNCS 2018 Project "Metodi Formali per la Verifica e la Sintesi di Sistemi Discreti e Ibridi".