# alternatingtime_temporal_logic_on_finite_traces__97787c88.pdf

Alternating-time Temporal Logic on Finite Traces

Francesco Belardinelli1, Alessio Lomuscio2, Aniello Murano3 and Sasha Rubin3

1 Laboratoire IBISC, UEVE, France 2 Department of Computing, Imperial College London, UK 3 DIETI, Universit a degli Studi di Napoli, Italy francesco.belardinelli@univ-evry.fr, a.lomuscio@imperial.ac.uk, murano@na.infn.it, rubin@unina.it

We develop a logic-based technique to analyse ﬁnite interactions in multi-agent systems. We introduce a semantics for Alternating-time Temporal Logic (for both perfect and imperfect recall) and its branching-time fragments in which paths are ﬁnite instead of inﬁnite. We study validities of these logics and present optimal algorithms for their modelchecking problems in the perfect recall case.

1 Introduction There is a long tradition in logic-based approaches to Artiﬁcial Intelligence (AI) to model the evolution of a system on the basis of an inﬁnite sequence of states [Alur et al., 2002; Mogavero et al., 2014]. This approach is heavily inﬂuenced by works in reactive systems and related temporal logic approaches, where a computing system is conceived as an entity that interacts with the environment indeﬁnitely [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 ﬁnite, phases in negotiation and coordination protocols are ﬁnite [Jennings et al., 2001], business processes are naturally modelled using ﬁnite traces [Pesic et al., 2010], and in automated planning successful executions are often ﬁnite (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 veriﬁcation of multi-agent systems with ﬁnite 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 ﬁnal states F and strategic quantiﬁers only range on paths that end in a state of F. We automatically get ﬁnite-trace semantics for the natural syntactic fragments of ATL f, i.e., ATLf,

CTLf, and CTL f, the ﬁnite-trace variants of the branchingtime temporal logics CTL and CTL, that we also study. We use ordinary ﬁnite-automata, operating on ﬁnite words, instead of inﬁnite words or trees, to give optimal algorithms for the model-checking problems of these logics (with perfect recall).

In particular, our algorithms sidestep intrinsic difﬁculties of model-checking ATL that are due to automata operating over inﬁnite words or trees, e.g., determinisation of B uchi automata, which has been resistant to efﬁcient 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 inﬁnite traces. In contrast, just like the procedures in [De Giacomo and Vardi, 2015], our algorithms are extremely simple: they only involve automata operating on ﬁnite words, and simple standard constructions on these such as the classic subset construction for determinisation. We consider this a signiﬁcant technical improvement.

Related Work. In recent years, several contributions in AI have focused on variants of LTL to reason about ﬁnitecomputation systems. Along this line, well studied is LTLf, a variant of the Linear-time Temporal Logic LTL where formulas are interpreted over ﬁnite traces (see [De Giacomo and Vardi, 2015] for a survey). This logic has proved particularly useful in planning [Bacchus and Kabanza, 2000; Baier and Mc Ilraith, 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 ﬁniteand inﬁnite-trace semantics for LTL, showing surprising differences both at the modelling and veriﬁcation 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 ﬁnite traces have already been

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

considered in the context of branching-time temporal logics, but never for logics of strategies. In [Vardi and Stockmeyer, 1985] a ﬁnite-trace semantics for CTL is introduced. This formal account, which is a special case of our semantics, is analysed brieﬂy in Remark 2. The expressivity of CTL on parameterised sets of traces, which includes the set of ﬁnite 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 ﬁnite traces, [Gutierrez et al., 2017] introduced and studied iterated Boolean games with LDL goals over ﬁnite traces. Differently from us, they consider the problem of the existence of Nash equilibria. Lastly, [Kong and Lomuscio, 2018] developed a veriﬁcation approach for ﬁnite traces of multi-agent systems against LDLf K speciﬁcations. Their approach focuses on the veriﬁcation 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 ﬁnite executions.

2 Concurrent Game Systems with Final States

In this section we introduce concurrent game structures (CGS) endowed with ﬁnal states. Given a set X of elements, let u Xω X+ denote an inﬁnite or non-empty ﬁnite 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 ﬁrst element of u is denoted by first(u), and its last by last(u). We write u i for its sufﬁx uiui+1 . . . starting in ui, and u i for its preﬁx u0 . . . ui. The empty sequence is denoted by ϵ. For a vector v Q i Xi we denote its i-th element by v(i). We now introduce our class of relevant models.

Deﬁnition 1 (CGS with ﬁnal states). A concurrent game structure (CGS) with ﬁnal states is a tuple G = Ag, AP, {Acta}a Ag, S, s0, F, δ, λ where: Ag is the ﬁnite non-empty set of agent names; AP is the ﬁnite non-empty set of atomic propositions; Acta is the ﬁnite non-empty set of actions for a Ag; S is the ﬁnite non-empty set of states; with initial state s0 S, and the non-empty set F S of ﬁnal states; δ : S Jact S is the transition function, where Jact = Q 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 deﬁnition of CGS [Alur et al., 2002] by explicitly identifying a set F S of ﬁnal states. Final states can be thought of as end states in games (e.g., all conﬁgurations 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 inﬁnite (resp. ﬁnite) 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 ﬁnal state, i.e., last(π) F. In the next section, we will deﬁne strategic quantiﬁers to range on paths, i.e., ﬁnite sequences ending in ﬁnal 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 inﬁnite, resp. ﬁnite, 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 ﬁnite as well as inﬁnite traces.

Syntax Fix ﬁnite 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:

ϕ ::= p | ϕ | ϕ ϕ | A ψ ψ ::= ϕ | ψ | ψ ψ | X ψ | ψ U ψ

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 quantiﬁer 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 .. . ), e X ψ ::= X ψ (read weak next ), and ψ R ψ ::= ( ψ U ψ ) (read releases ), F ψ ::= true U ψ (read eventually ) and G ψ ::= false R ψ (read globally ). Hereafter we consider also the ATL fragment of ATL . State formulas are built in the same way, whereas path formulas ψ are deﬁned as follows:

ψ ::= X ϕ | e X ϕ | ϕ U ϕ | ϕ R ϕ

Notice that operators e 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. Speciﬁcally, in

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

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 ﬁnite traces.

Semantics Fix a CGS G with ﬁnal states. For x { , f} and y {R, r}, we simultaneously deﬁne, 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:

(G, s) |=xy p iff p λ(s) (G, s) |=xy ϕ iff (G, s) |=xy ϕ (G, s) |=xy ϕ ϕ iff (G, s) |=xy ϕ and (G, s) |=xy ϕ

(G, s) |=xy A ψ iff for some joint strategy σA Σy(G), for all π outx(s, σA), (G, π) |=xy ψ. (G, π) |=xy ϕ iff (G, π0) |=xy ϕ (G, π) |=xy ψ iff (G, π) |=xy ψ (G, π) |=xy ψ ψ iff (G, π) |=xy ψ and (G, π) |=xy ψ

(G, π) |=xy X ψ iff π 1 = ϵ and (G, π 1) |=xy ψ (G, π) |=xy ψ U ψ iff for some j < |π|, (G, π j) |=xy ψ , and for all k with 0 k < j, (G, π k) |=xy ψ 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 ﬁnal states. We consider the following sets of validities: For x { , f} and y {R, r}, let

ATL xy = {ϕ ATL ||=xy ϕ}

ATLxy = {ϕ ATL ||=xy ϕ}.

Notice that for x = we obtain the standard semantics for ATL and ATL on inﬁnite traces [Alur et al., 2002]; while y {R, r} discriminates between the perfectand 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 ﬁnite 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 inﬁnite path π starting in s such that every preﬁx of π ending in a ﬁnal state in F satisﬁes ψ. 2. [[Ag]]ψ is true at state s iff for all inﬁnite paths π starting in s, there is some preﬁx of π ending in a ﬁnal state in F, that satisﬁes ψ. 3. A ψ deﬁned as ψ is true at state s iff all ﬁnite paths starting in s and ending in F satisfy ψ. 4. E ψ deﬁned as [[ ]]ψ is true at state s iff that there exists a ﬁnite path starting in s, ending in F, that satisﬁes ψ. 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 deﬁnite 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 ﬁnal states correspond to the end states or the important states.1 Then, e.g., if the ﬁnal states in the CGS corresponds to check , a formula of the form {Black} G F Queen 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 ﬁnite traces, i.e., for x = f. We begin by discussing the relationship between our CTL f R and a previous deﬁnition of CTL on ﬁnite traces.

Remark 2. In [Vardi and Stockmeyer, 1985] a semantics for CTL on ﬁnite traces is put forward. Speciﬁcally, path quantiﬁers range on all ﬁnite paths starting from a given state s, including the trivial path π = s . Observe that we can mimic such an interpretation in CGS with ﬁnal states by assuming that F = S. However, such a semantic choice validates peculiar CTL formulas including A F ϕ ϕ and E G ϕ ϕ. As a result, whenever path quantiﬁers range unrestrictedly over all ﬁnite paths, modalities A F and E G collapse to truth in the current state. We stress that nothing similar is the case in the semantics we propose, in particular A F and E G 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 inﬁnite 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:

ATLfr = ATLf R

ATL fr ATL f R Thus, ATL and ATL have the same distinguishing power as regards perfect/imperfect recall both on inﬁnite and on ﬁnite traces. Now we discuss the reason we chose the syntax of ATL to include e X, the dual of X. Remark 4. It is known that, differently from the case of inﬁnite traces, on ﬁnite 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

|=f X ψ X ψ but |=f X ψ X ψ

This remark justiﬁes the introduction of weak next e X ψ as X ψ (thus, e.g., differently from the case of inﬁnite traces, A e X ϕ is no longer equivalent to A X ϕ).

1Of 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.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

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

[[A]] X ϕ ::= A e X ϕ

[[A]] e X ϕ ::= A X ϕ [[A]](ϕ U ϕ ) ::= A ( ϕ R ϕ ) [[A]](ϕ R ϕ ) ::= A ( ϕ U ϕ )

Finally, we present ﬁxed 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 ﬁxed points. Remark 5. The following formulas are validities in ATLf (for each type of recall r, R):

A ψ1 U ψ2 A (ψ2 (ψ1 A X A ψ1 U ψ2)) (1)

A ψ1 R ψ2 A (ψ1 (ψ2 A X A ψ1 R ψ2)) (2)

We conclude by remarking that on inﬁnite traces A is equivalent to , which is not the case on ﬁnite traces. In fact, on ﬁnite 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. Deﬁnition 2 (Model Checking). Given a CGS G with ﬁnal states and a formula ϕ, model checking G against ϕ on inﬁnite (resp. ﬁnite) 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.

Logic Complexity Reference CTL PTIME-c [Clarke et al., 1986] CTL PSPACE-c [Emerson and Lei, 1985] ATL PTIME-c [Alur et al., 2002] ATL 2EXPTIME-c [Alur et al., 2002]

Table 1: Complexity of model checking for x = , y = R.

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

Logic Complexity Theorems CTLf,R PTIME-c 2, 4 CTL f,R PSPACE-c 3, 5 ATLf,R PTIME-c 2, 4 ATL f,R 2EXPTIME-c 1, 6

Table 2: Complexity of model checking for x = f, y = R.

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 ﬁnite, 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 simpliﬁes 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 ﬁx-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: Game Solving(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 coalition A can 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 Vardi Wolper construction to ﬁnite 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

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Algorithm: Model Checking(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: (a) If ϕ = p AP then label s by pϕ iff p λ(s). (b) If ϕ = ϕ1 then label s by pϕ iff s is not in the set output by Model Checking(G, ϕ1). (c) If ϕ = ϕ1 ϕ2 then label s by pϕ iff s is in the sets output by Model Checking(G, ϕi) for i = 1, 2. (d) If ϕ = A ψ (so ψ is a path formula) then i. Let Max(ψ) be the set of maximal statesubformulas of ψ. ii. For every ξ Max(ψ) label s by pξ if s is in the set output by Model Checking(G, ξ). iii. Replace every occurrence in ψ of ξ Max(ψ) by pξ. iv. Label s by pϕ iff s is in the set output by Game Solving(G, A, ψ). 2. 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 Game Solving algorithm (Figure 1).

2AP D, and ﬁnal 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 a Acta (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 G Safe). This can be solved in linear time using the greatest ﬁx-point of the operation Y 7 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 Game Solving 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 X p , e X p , p U p or p R p where p , p are atoms. So, the complexity of Game Solving(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 Game Solving(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: LTLf Model Checking(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 ﬁnite words, e.g., [Vardi and Wolper, 1994]. Denote its states N, initial states I N, transition relation N 2AP N, and ﬁnal 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 from modelchecking CTL, known to be PTIME-hard [Clarke et al., 1986]; for CTL f we reduce from model-checking ﬁnite 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

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

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 ﬁnal 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 ﬁnite 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 ﬁnal 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 ﬁnal), δ(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 ﬁnite 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 ﬁnite 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 ﬁnite sequence X0X1 . . . Xn with Xi X, the sequence (X0 c(X0))(X1 c(X0X1)) . . . (Xn c(X0X1 Xn)) satisﬁes ϕ. 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 ﬁnite and end in ﬁnal states. Let ϕ be an LTLf formula over atoms X Y . We deﬁne a CGS GX,Y with ﬁnal states and an LTLf formula ϕd such that ϕ is realisable iff GX,Y |= {2} X X ϕd. Deﬁne GX,Y with ﬁnal 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 ﬁrst. 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 ﬁnal states) is in the language ( {{z} : z F}) . For example, the ﬁnite 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})}. Deﬁne the formula ϕd as follows: pd = p, (ϕ ϕ )d = ϕd ϕ d, ( ϕ)d = ϕd, (X ϕ)d = X X ϕ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} X X ϕ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 ﬁxed X and Y , and thus GX,Y has constant size.

5 Conclusions

Motivated by problems in AI rather than program veriﬁcation, we deﬁned a logic with the same syntax as ATL but in which paths are ﬁnite instead of inﬁnite. Precisely, a model is equipped with a special set F of ﬁnal states and strategic quantiﬁers only account for paths that end in a state of F. This deﬁnition is general enough to capture previous proposals for CTL and LTL on ﬁnite traces, as well as synthesis of LTL on ﬁnite traces. Indeed, in Section 4 we showed how to reduce model-checking ﬁnite traces against LTLf formulas to model-checking CGS with ﬁnal 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 ﬁnite traces in structures [Vardi and Stockmeyer, 1985], it was assumed (in the language of this paper) that all states are ﬁnal, which leads to validities such as A F ϕ ϕ and E G ϕ ϕ that are not intuitive or natural (see Remark 2). Our more reﬁned 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 f R does not use complex constructions on automata operating on inﬁnite strings or inﬁnite trees. In fact, we do not translate ATL f R (or its fragments) into

ATL R. Instead, our algorithms only involve automata operating on ﬁnite words, and simple standard constructions on these, e.g., the classic subset construction for determinisation and a ﬁx-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 SVe Da S (ANR-16-CE40-0021); the Royal Academy of Engineering; the Royal Society; and INDAM GNCS 2018 Project Metodi Formali per la Veriﬁca e la Sintesi di Sistemi Discreti e Ibridi .

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

References [Alur et al., 2002] R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672 713, 2002. [Bacchus and Kabanza, 2000] F. Bacchus and F. Kabanza. Using temporal logics to express search control knowledge for planning. Artiﬁcial Intelligence, 116(1-2):123 191, 2000. [Baier and Katoen, 2008] C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press, 2008. [Baier and Mc Ilraith, 2006] J. A. Baier and S. A. Mc Ilraith. Planning with ﬁrst-order temporally extended goals using heuristic search. In AAAI, pages 788 795, 2006. [Camacho et al., 2017] A. Camacho, E. Triantaﬁllou, C. J. Muise, J. A. Baier, and S. A. Mc Ilraith. Non-deterministic planning with temporally extended goals: LTL over ﬁnite and inﬁnite traces. In AAAI, pages 3716 3724, 2017. [Clarke et al., 1986] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic veriﬁcation of ﬁnite-state concurrent systems using temporal logic speciﬁcations: A practical approach. ACM TOPLAS, 8(2):244 263, 1986. [De Giacomo and Vardi, 2013] G. De Giacomo and M. Y. Vardi. Linear temporal logic and linear dynamic logic on ﬁnite traces. In IJCAI, pages 854 860, 2013. [De Giacomo and Vardi, 2015] G. De Giacomo and M. Y. Vardi. Synthesis for LTL and LDL on ﬁnite traces. In IJCAI, pages 1558 1564, 2015. [De Giacomo et al., 2014a] G. De Giacomo, R. De Masellis, M. Grasso, F. M. Maggi, and M. Montali. Monitoring business metaconstraints based on LTL and LDL for ﬁnite traces. In BPM, LNCS 8659, pages 1 17, 2014. [De Giacomo et al., 2014b] G. De Giacomo, R. De Masellis, and M. Montali. Reasoning on LTL on ﬁnite traces: Insensitivity to inﬁniteness. In AAAI, pages 1027 1033, 2014. [Emerson and Halpern, 1986] E. A. Emerson and J. Y. Halpern. sometimes and not never revisited: on branching versus linear time temporal logic. Journal of the ACM, 33(1):151 178, 1986. [Emerson and Lei, 1985] E. A. Emerson and C. L. Lei. Modalities for model checking: Branching time logic strikes back. In POPL, pages 84 96, 1985. [Emerson et al., 2001] E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model checking for the µ-calculus and its fragments. Theor. Comp. Sci., 258(1 2):491 522, 2001. [Filiot et al., 2011] E. Filiot, N. Jin, and J.-F. Raskin. Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design, 39(3):261 296, 2011. [Geffner and Bonet, 2013] H. Geffner and B. Bonet. A Concise Introduction to Models and Methods for Automated Planning. Morgan & Claypool Publishers, 2013. [Gerevini et al., 2009] A. Gerevini, P. Haslum, D. Long, A. Saetti, and Y. Dimopoulos. Deterministic planning in the ﬁfth international planning competition: PDDL3 and

experimental evaluation of the planners. Artiﬁcial Intelligence, 173(5-6):619 668, 2009. [Gr adel et al., 2002] E. Gr adel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Inﬁnite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. [Gutierrez et al., 2017] J. Gutierrez, G. Perelli, and M. Wooldridge. Iterated games with LDL goals over ﬁnite traces. In AAMAS, pages 696 704, 2017. [Harel and Pnueli, 1985] D. Harel and A. Pnueli. On the development of reactive systems. In Logics and models of concurrent systems, pages 477 498. Springer, 1985. [Hopcroft and Ullman, 1979] J. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Adison-Wesley Publishing Company, 1979. [Jennings et al., 2001] N. R. Jennings, P. Faratin, A. Lomuscio, S. Parsons, M. Wooldridge, and C. Sierra. Automated negotiation: prospects, methods and challenges. Group Decision and Negotiation, 10(2):199 215, 2001. [Kong and Lomuscio, 2018] J. Kong and A. Lomuscio. Model checking multi-agent systems against ldlk speciﬁcations on ﬁnite traces. In AAMAS, 2018. To Appear. [Kupferman et al., 2006] O. Kupferman, N. Piterman, and M. Y. Vardi. Safraless compositional synthesis. In CAV, LNCS 4144, pages 31 44, 2006. [Mogavero et al., 2014] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):34:1 34:47, 2014. [Montali et al., 2010] M. Montali, M. Pesic, W. M. P. van der Aalst, F. Chesani, P. Mello, and S. Storari. Declarative speciﬁcation and veriﬁcation of service choreographiess. ACM Transactions on the Web (TWEB), 4(1):3, 2010. [Pauly and Parikh, 2003] M. Pauly and R. Parikh. Game logic - an overview. Studia Logica, 75(2):165 182, 2003. [Pesic et al., 2010] M. Pesic, D. Bosnacki, and W. M. P. ravan der Aalst. Enacting declarative languages using LTL: avoiding errors and improving performance. In SPIN, LNCS 6349, pages 146 161, 2010. [Rabin and Scott, 1959] M. O. Rabin and D. S. Scott. Finite Automata and their Decision Problems. IBM Journal of Research & Development, 3:115 125, 1959. [Schnoebelen, 2003] Ph. Schnoebelen. The complexity of temporal logic model checking. In Ai ML02, volume 4 of Advances in Modal Logic, pages 437 459. 2003. [Tsai et al., 2014] M.-H. Tsai, S. Fogarty, M. Y. Vardi, and Y.-K. Tsay. State of B uchi complementation. Logical Methods in Computer Science, 10(4), 2014. [Vardi and Stockmeyer, 1985] M. Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In STOC, pages 240 251, 1985. [Vardi and Wolper, 1994] M. Y. Vardi and P. Wolper. Reasoning about inﬁnite computations. Information and Computation, 115(1):1 37, 1994.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)