<figure><img src="image_1.png" /></figure>

HAL
open science

# Imperfect Information in Alternating-Time Temporal Logic on Finite Traces

Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, Sasha Rubin

► To cite this version:

Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, Sasha Rubin. Imperfect Information in Alternating-Time Temporal Logic on Finite Traces. 22nd International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2019), Oct 2019, Turin, Italy. pp.469-477, 10.1007/978-3-030-33792-6_31. hal-02424595

HAL Id: hal-02424595

https://hal.science/hal-02424595v1

Submitted on 19 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Imperfect Information
in Alternating-time Temporal Logic on Finite Traces

Francesco Belardinelli<fnref n="1" />,<fnref n="2" />, Alessio Lomuscio<fnref n="2" />, Aniello Murano<fnref n="3" />, and Sasha Rubin<fnref n="4" />

**Abstract.** We introduce a logic to reason about strategic abilities in finite games under imperfect information. We interpret Alternating-time Temporal Logic on interpreted systems with final states, where agents only have partial observability of the system's global state. We consider the model checking problem in this setting. We prove that the complexity results available for the case of infinite traces carry over to the finite traces case. We show that when only public actions are allowed, the verification problem under perfect recall becomes decidable.

## 1 Introduction

In this paper we further the line of work initiated in [5] and introduce a novel semantics for Alternating-time Temporal Logic (ATL) interpreted on finite traces, under both the *objective* and *subjective* interpretation of imperfect information [19]. Indeed, in negotiation, coordination, planning, business processes, as well as other AI-inspired applications, agents typically have imperfect information regarding the current state of the system. More precisely, we extend interpreted systems — a well-studied framework to reason about imperfect information [15] — with final states. Then, strategy operators in ATL only range on paths that end in a final state. We consider the model checking problem in this setting. In Sec. 3 we show that the complexity of model checking ATL on finite traces (under imperfect information, for both perfect and imperfect recall) is the same as for infinite traces, a result that echoes [5]. Yet, our decision procedures only use ordinary automata, operating on finite words, instead of infinite words or trees, thus sidestepping intrinsic difficulties of model checking ATL on infinite traces, due to automata operating over infinite words or trees, e.g., the determinisation of Büchi automata, which has proved to be resistant to efficient implementation [26], and emptiness of alternating parity tree automata [14]. Finally, in Sec. 4 we prove that, when agents can only perform public actions, then verification becomes decidable even under imperfect information and perfect recall. This result, which builds on [4, 6], is relevant, e.g., to the theoretical foundations of planning with public actions [20].

**Related Work.** Recently, a wealth of contributions in formal methods for AI have focused on LTL<sub>f</sub>, a variant of the linear-time temporal logic LTL interpreted on finite traces (see, e.g., [10]). This logic has been applied to planning [2, 3, 17, 11, 7], and in business process modelling [24, 23, 8, 25]. For a thorough comparison of the finite- and infinite-trace semantics for LTL, see [9].

<footnote n="1">¹ Laboratoire IBISC, UEVE, France</footnote>

<footnote n="2">² Department of Computing, Imperial College London, UK</footnote>

<footnote n="3">³ DIETI, Università degli Studi di Napoli, Italy</footnote>

<footnote n="4">⁴ School of Computer Science, University of Sydney, Australia</footnote>
Differently from [11], where model checking LTL<sub>f</sub> is considered w.r.t. finite traces, here our models for ATL are interpreted systems. This modelling choice allows for the representation of complex strategic behaviours in multi-agent systems. Actually, interpretations on finite traces were originally considered in the context of the branching-time temporal logic CTL* [27]. These investigations were further pursued in [13], but — to the best of our knowledge — there is no work that tackles their model checking problems. Motivated by strategic reasoning over finite traces, [18] introduced iterated Boolean games with LDL goals over finite traces. Differently from us, the authors focus on the existence of Nash equilibria, rather than the verification of general ATL specifications. Further, [21] developed a verification approach for finite traces of multi-agent systems in the LDL<sub>f</sub> K specifications language, which is more limited in that it does not have strategic operators, and more general in that it allows LDL operators (while we only allow LTL operators).

Closely related to the present contribution is [5], where a semantics for ATL on finite traces is presented for the case of concurrent game structures of *perfect information*. Here, we analyse the arguably more complex case of interpreted systems with imperfect information. Moreover, the restriction to public actions to retain decidability of ATL in contexts of imperfect information and perfect recall has been put forward in [4, 6], even though only in relation with infinite traces. We here apply the same intuition to a semantics on finite traces. In general, automata-theoretic decision procedures working on finite traces present several advantages. More precisely, the procedures in Sec. 3 and 4 avoid determinisation and solving emptiness of alternating tree automata, such as Safraless decision procedures [22, 16]. These procedures, while undeniably elegant, are still complex and tailored to reasoning about infinite traces. In contrast, just like [10], our algorithms are simpler: they only involve automata operating on *finite words*, and use the standard constructions on these, such as the classic subset construction for determinisation. We consider this a significant technical improvement.

## 2 ATL on Interpreted Systems with Final States

Given a set $X$ of elements, let $u \in X^+$ denote a non-empty finite sequence on $X$. Then, we write $u_i$ for its $i$th element, i.e., $u = u_1 u_2 \dots$, and $|u| \in \mathbb{N}$ for its length. The first element of $u$ is denoted by $first(u)$, and its last by $last(u)$. We write $u_{\ge i}$ for its suffix $u_i u_{i+1} \dots$ starting in $u_i$, and $u_{\le i}$ for its prefix $u_1 \dots u_i$. The empty sequence is denoted by $\epsilon$. For a vector $v \in \prod_i X_i$ we denote its $i$th element by $v(i)$. The powerset of $X$ is denoted by $\mathbb{P}(X)$.

We extend the formalisms of interpreted systems [15] with final states, similarly to the definition of finite automata. In what follows we fix a set *AP* of atomic propositions (or *atoms*).

**Definition 1 (IS<sub>f</sub>).*** An interpreted system (IS) with final states is a tuple $M = \langle Ag, \{L_a, act_a, P_a, \tau_a\}_{a \in Ag}, S_0, F, \lambda \rangle$, where $Ag = \{1, \dots, n\}$ is a finite set of agents and for every $a \in Ag$:

- $L_a$ is the finite set of local states $l, l', \dots$ of agent $a$.
- $act_a$ is the finite non-empty set of actions of agent a. Then, let Jact denote the set $act_1 \times \dots \times act_n$ of joint actions, and Act the set $\cup_{a \in Ag} act_a$ of all actions.

- $P_a : L_a \to \mathbb{P}(act_a) \setminus \{\emptyset\}$ is the local protocol for agent a, specifying which actions a can execute from each local state.

If $j \in P_a(l)$ we say that action j is available to agent a in local state $l \in L_a$.

- $\tau_a : L_a \times Jact \to L_a$ is the (partial) local transition function such that $\tau_a(l, J)$ is defined iff action $J(a)$ is available to a in local state $l$. That is, $\tau_a$ returns the next local state for agent a from local state $l$ following a joint action $J$ by all agents.

Further, let $S = L_1 \times \dots \times L_n$ be the set of global states, $S_0 \subseteq S$ is the set of initial (global) states and $F \subseteq S$ is the set of final (global) states. Finally, $\lambda : AP \to \mathbb{P}(S)$ is the valuation function.

We now recall some standard terminology about interpreted systems, that will be used hereafter. The induced global transition function is the partial function $\tau : S \times Jact \to S$ such that $\tau(s, J)$ is defined iff for every agent $a \in Ag$, action $J(a)$ is available to agent $a$ in local state $s(a)$. If defined, $\tau(s, J)$ is the global state $s'$ such that $s'(a) = \tau_a(s(a), J)$ for every agent $a \in Ag$. A history is a finite sequence $h \in S^+$ of global states starting in an initial state, and respecting the global transition function, i.e., $h(1) \in S_0$ and for every $n < |h|$ there exists a joint action $J \in Jact$ such that (i) all agent actions are allowed by the respective individual protocols (i.e., $J(a) \in P_a(h_a(n)))$, and (ii) $h(n+1) = \tau(h(n), J)$. For agent $a \in Ag$ and $n < |h|$, let $h_a(n)$ be the local state of agent $a$ in the $n$th global state of $h$. We denote with Hist the set of all histories. A trace is a history $\pi$ that ends in a final state, i.e., $last(\pi) \in F$. Hereafter, we define strategic quantifiers to range over traces, i.e., finite sequences ending in final states. We denote the set of all traces by Traces.

Finally, we introduce an indistinguishability relation $\sim_a$ on $S$, for every agent $a \in Ag$, such that $s \sim_a s'$ iff $s(a) = s'(a)$, that is, two states are indistinguishable for agent $a$ iff $a$'s local state is the same in both states [15]. We extend $\sim_a$ to histories in a synchronous, point-wise manner: for $h, h' \in Hist$ define $h \sim_a h'$ if $|h| = |h'|$ and $h(i) \sim_a h'(i)$ for all $i \le |h|$. Finally, for a history $h$, let $last([h]_{\sim_A}) \subseteq S$ denote the set of states $last(h')$ for which there exists $a \in A$ with $h' \sim_a h$.

We now introduce the language ATL\* and its fragment ATL [1]. We then provide them with an interpretation on the finite traces generated by the interpreted systems with final states introduced in Sec. 2.

**Definition 2 (ATL\***). The history $(\varphi)$ and trace $(\psi)$ formulas over AP and Ag are built using the following BNF, where $p \in AP$ and $A \subseteq Ag$:

$$ \varphi ::= p \mid \neg \varphi \mid \varphi \wedge \varphi \mid \langle\!\langle A \rangle\!\rangle \psi $$

$$ \psi ::= \varphi \mid \neg \psi \mid \psi \wedge \psi \mid X \psi \mid \psi \cup \psi $$

The class of ATL\* formulas is the set of all and only history formulas.

Traces formulas are built by using the temporal operators "next" X and "until" U. The strategy quantifier $\langle\!\langle A \rangle\!\rangle$ is read as "the agents in coalition A can enforce ...". We introduce the following abbreviations: $[A]\psi ::= \neg\langle\!\langle A \rangle\!\rangle\neg\psi$ (read "no matter what the
agents in A do..."), "weak next" $\tilde{X} \psi ::= \neg X \neg \psi$, "releases" $\psi R \psi' ::= \neg(\neg \psi U \neg \psi')$, "eventually" $F \psi ::= \text{true} U \psi$, and "globally" $G \psi ::= \text{false} R \psi$.

Hereafter we consider also the ATL fragment of ATL*, where trace formulas $\psi$ are restricted as follows: $\psi ::= X \varphi | \tilde{X} \varphi | \varphi U \varphi | \varphi R \varphi$.

Notice that operators $\tilde{X}$ and $R$ have to be assumed as primitive in ATL. We discuss the reason why in Remark 2, but we need first to introduce the formal semantics of ATL.

**Definition 3 (Strategies).** A (perfect recall or memoryfull) uniform strategy for agent $a$ is a function $\sigma_a : \text{Hist} \to \text{act}_a$ such that for every history $h, h' \in \text{Hist}$, (i) action $\sigma_a(h)$ is available to agent $a$: $\sigma_a(h) \in P_a(\text{last}(h_a))$, and (ii) $h \sim_a h'$ implies $\sigma_a(h) = \sigma_a(h')$.

A (uniform) strategy $\sigma$ is *positional* or *memoryless* if for all $h, h' \in \text{Hist}$, $\text{last}(h') = \text{last}(h)$ implies $\sigma(h) = \sigma(h')$. The set of all memoryfull (resp. memoryless) strategies is denoted as $\Sigma_R$ (resp. $\Sigma_r$). For $A \subseteq Ag$ and $y \in \{R, r\}$, let $\sigma_A : A \to \Sigma_y$ denote a joint strategy associating a (memoryfull or memoryless) strategy $\sigma_a$ with each agent $a \in A$. For history $h \in \text{Hist}$ and joint strategy $\sigma_A$, let $\text{out}_{\text{obj}}(h, \sigma_A)$, called the *objective outcomes of* $\sigma_A$ from $h$, include all traces $\pi$ (recall that traces are histories that end in final states) consistent with $\sigma_A$ and $h$, that is, $\pi_{\le |h|} = h$, and for every $i \ge |h|$ there exists $J_i \in \text{Jact}$ such that $\pi_{i+1} \in \tau(\pi_i, J_i)$ and for every $a \in A$ we have $J_i(a) = \sigma_A(a)(\pi_{\le i})$. Then, let the set $\text{out}_{\text{subj}}(h, \sigma_A)$ of *subjective outcomes of* $\sigma_A$ from $h$ be defined as $\bigcup_{i \in A, h' \sim_i h} \text{out}_{\text{obj}}(h', \sigma_A)$. That is, we consider all (objective) outcomes from any history that is indistinguishable from the current history for some agent $a$ in coalition $A$. The distinction between objective and subjective outcomes has been introduced in [19], to which we refer for an in-depth discussion.

We can now define the interpretation of formulas on the finite trace semantics.

**Definition 4.** Fix an ISf M with final states. For $x \in \{\text{obj, subj}\}$ and $y \in \{R, r\}$, we define, by induction on the structure of formulas, the relation $(M, h, m) \models_{xy} \phi$, where $h \in \text{Hist}$, $\phi$ is a formula, and $m \le |h|$,

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
(M, h, m) & \models_{xy} p & \text{iff } p \in \lambda(h(m)) \\
(M, h, m) & \models_{xy} \neg \varphi & \text{iff } (M, h, m) \not\models_{xy} \varphi \\
(M, h, m) & \models_{xy} \varphi \wedge \varphi' & \text{iff } (M, h, m) \models_{xy} \varphi \text{ and } (M, h, m) \models_{xy} \varphi' \\
(M, h, m) & \models_{xy} \langle\langle A \rangle\rangle \psi & \text{iff for some joint strategy } \sigma_A \in \Sigma_y, \\
& & \text{for all traces } \pi \in \text{out}_x(h_{\le m}, \sigma_A), (M, \pi, m) \models_{xy} \psi \\
(M, h, m) & \models_{xy} \neg \psi & \text{iff } (M, h, m) \not\models_{xy} \psi \\
(M, h, m) & \models_{xy} \psi \wedge \psi' & \text{iff } (M, h, m) \models_{xy} \psi \text{ and } (M, h, m) \models_{xy} \psi' \\
(M, h, m) & \models_{xy} X \psi & \text{iff } h_{> m} \neq \epsilon \text{ and } (M, h, m+1) \models_{xy} \psi \\
(M, h, m) & \models_{xy} \psi \cup \psi' & \text{iff for some } j, m \le j \le |h|, (M, h, j) \models_{xy} \psi', \text{ and} \\
& & \text{for all } k, m \le k < j \text{ implies } (M, \pi, k) \models_{xy} \psi
\end{array}
$$

For a formula $\phi$, we write $M \models_{xy} \phi$ to mean that $(M, s, 1) \models_{xy} \phi$, for every $s \in S_0$; whereas $\phi$ is a validity, or $\models_{xy} \phi$, iff $M \models_{xy} \phi$ for every ISf M with final states.

**Remark 1.** Notice that the clause for formulas $\langle\langle A \rangle\rangle \psi$ in Def. 4 is well-defined as traces are histories in particular.
Moreover, in the case of the memoryless semantics, we can show that a history formula $\varphi$ is true in history $h$, at point $m$, iff $\varphi$ is true at state $h(m)$, that is,

$$ (M, h, m) \models_{xr} \varphi \text{ iff } (M, h(m), 1) \models_{xr} \varphi $$

So, for the memoryless semantics, we can forget about the past when evaluating history formulas (which are then really state formulas). However, this is not the case in general when we assume perfect recall.

**Remark 2.** As anticipated above, it is well-known that, differently from the case of infinite traces, on finite traces the next operator X is not self-dual. In particular, according to the semantics for $\models_f$ given in [10] in LTL$_f$ we have that

$$ \models_f X \psi \rightarrow \neg X \neg \psi \text{ but } \not\models_f \neg X \neg \psi \rightarrow X \psi $$

This remark justifies the introduction of weak next $\tilde{X}\psi$ as $\neg X \neg \psi$ (thus, e.g., differently from the case of infinite traces, $\langle\langle A \rangle\rangle \tilde{X} \varphi$ is no longer equivalent to $\langle\langle A \rangle\rangle X \varphi$).

**Remark 3.** Finite traces have already been considered in the framework of interpreted systems in [21], even though without final states, or what is equivalent in our notation, assuming all states are final. Then, all finite executions are accounted for in the semantics. Unfortunately, in branching-time logics this modelling choice brings about the collapse of truth in the current state and truth in all possible future states, as remarked in [5] (for instance, if all states are final). Hence, here we restrict the range of strategy operators on executions terminating in a final state only.

That said, it is not hard to see that the semantics with final states can be simulated by the special case in which all states are final. This can be done by introducing a fresh atom final that labels the final states, and replacing each formula of the form $\langle\langle A \rangle\rangle \psi$ by $\langle\langle A \rangle\rangle (F G \text{ final } \rightarrow \psi')$, where $\psi'$ is the result of applying the translation recursively to $\psi$. Indeed, this works because a finite trace ends in a final state iff it satisfies F G final. Note, however, that this translation does not preserve the fragment ATL since e.g., the translation of the ATL formula $\langle\langle A \rangle\rangle G q$ is the ATL* formula $\langle\langle A \rangle\rangle (F G \text{ final } \rightarrow G q)$ which is not in ATL.

We observe that [21] does not suffer from the collapse of modalities as they focus on an epistemic extension of linear-time LDL$_f$.

# 3 The Model Checking Problem

We now state the decision problem that we will analyse in the rest of the paper.

**Definition 5 (Model Checking).** Given an IS$_f$ M and a formula $\varphi$, model checking M against $\varphi$ on finite traces, w.r.t. the objective (resp. subjective) interpretation and perfect (resp. imperfect) recall amounts to determining whether $M \models_{xy} \varphi$ for $x = \text{obj}$ (resp. $x = \text{subj}$) and $y = R$ (resp., $y = r$).

We investigate the model checking problem by considering imperfect recall first and then perfect recall. Since the resulting computational complexity is the same for the subjective and objective interpretation (notice that for checking strategy formulas $\langle\langle A \rangle\rangle \psi$ we need to consider all states indistinguishable from the current one, of which there are only linearly many), in the following we focus on the objective interpretation.
**Theorem 1 (ATL<sub>r</sub>).** *Model checking ATL<sub>r</sub> is Δ<sub>2</sub><sup>P</sup>-complete.*

We now consider the full language of ATL\*.

**Theorem 2 (ATL<sub>r</sub><sup>*</sup>).* Model checking ATL<sub>r</sub><sup>*</sup> is PSPACE-complete.

In the case of perfect recall, the model checking problem is undecidable for both languages, as it is the case for infinite traces [12].

**Theorem 3 (ATL<sub>R</sub>).** *Model checking ATL<sub>R</sub> is undecidable.*

By Theorem 3 the following immediately holds.

**Corollary 1 (ATL<sub>R</sub><sup>*</sup>).* Model checking ATL<sub>R</sub><sup>*</sup> is undecidable.

The following table summarizes the complexity results for the model checking problem of ATL and ATL\* on finite traces.

<table><thead><tr><th></th><th>r</th><th>R</th></tr></thead><tbody><tr><td>ATL</td><td>Δ<sub>2</sub><sup>P</sup>-complete</td><td>undecidable</td></tr><tr><td>ATL\*</td><td>PSPACE-complete</td><td>undecidable</td></tr></tbody></table>

Observe that the complexity results are the same as those for infinite traces. However, it should be noted that the algorithms tackling decidable cases sidestep intrinsic difficulties in model checking ATL/ATL\* that are due to automata operating over infinite words or trees, e.g., determinisation of Büchi automata, which has been resistant to efficient implementation [26], or emptiness of alternating parity tree automata, [14]. This may in turn lead to more efficient implementations.

# 4 Decidability via Public Actions

We now identify a subclass of the class of interpreted systems with final states for which the model checking problem is decidable even under the assumptions of imperfect information and perfect recall. Specifically, this is the class of interpreted systems with public actions [4, 6].

**Definition 6 (IS with Public Actions).** An interpreted system with public actions (and final states) is a tuple $\langle Ag, \{L\_pr_a, act_a, pb\_act_a, P_a, \tau_a\}_{a \in Ag}, S_0, F, \lambda \rangle$ such that $\langle Ag, \{L_a, act_a, P_a, \tau_a\}_{a \in Ag}, S_0, F, \lambda \rangle$ is an IS with final states where, for every agent $a \in Ag$:

1. $pb\_act_a \subseteq act_a$ is the set of public actions of agent $a$;

2. $L_a = L\_pr_a \times \prod_{b \in Ag} (pb\_act_b \cup \{\epsilon\})$ is the set of local states;

3. the local transition function $\tau_a$ satisfies the property that $\tau_a(l, j) = (p', j')$ implies that for all $b \in Ag$, if $j_b \in pb\_act_b$ then $j'_b = j_b$ and otherwise $j'_b = \epsilon$.

Intuitively, the set $L\_pr_a$ consists of the private (local) states of agent $a$. Then, the full local state of $a$ comprises her private state and all public actions that have been played by any agent in the previous round.

Then, the following class of IS<sub>f</sub> is the focus of this section.
**Definition 7 (PAIS).** Let public-action interpreted systems be the class of interpreted systems with public actions (and final states) such that $act_a = pb\_act_a$ for all $a \in Ag$.

We remark briefly that rounds in a number of community card games (bridge, poker, etc.) can as well be encoded as PAIS.

Here is the main result of this section:

**Theorem 4.** The model-checking problem for $ATL_R^*$ on PAIS is 2EXPTIME-complete.

As for the lower bound, we use the fact that concurrent game structures (CGS) of perfect information can be embedded into PAIS by using a polynomial reduction. We here provide only a sketch of proof, and refer to [1] for a presentation of CGS. Intuitively, given a CGS $G$, the local state of each agent in the associated PAIS $IS_f$ is defined as the current state of the CGS. Further, all actions in the CGS can be assumed to be public. Then, the transition relation in $IS_f$ just mimics the one in $G$. We can check that the size of the state space of $IS_f$ is polynomial (indeed linear) in the size of $G$. In particular, it can then be shown that the two structures satisfy the same formulas in $ATL_R^*$. Finally, model checking CGS against $ATL_R^*$, interpreted on finite traces, is 2EXPTIME-hard (c.f., [5]), since the latter can encode the synthesis problem for $LTL_f$, which is 2EXPTIME-hard [10].

# 5 Conclusions

In this contribution we introduced a novel interpretation of Alternating-time Temporal Logic under imperfect information, based on finite traces. To do so, we extended the framework of Interpreted Systems with final states, representing intuitively notable check-points in the system's execution. Then, we analysed the corresponding model checking problem for various flavours of ATL, depending on syntax and memory. We remarked that the complexity results obtained are analogous to those available for the case of infinite traces, with the notable difference that the related decision procedures make use of finite automata only, rather than infinite ones. Most importantly, for the specific case of $IS_f$ with public actions only, we were able to obtain decidability also for the case of imperfect information and perfect recall, which is undecidable in general.

In future work we plan to test our intuition that manipulations on finite automata are more amenable to practical model checking through an implementation.

**Acknowledgements.** The authors acknowledge support of ANR JCJC Project SVeDaS (ANR-16-CE40-0021). Alessio Lomuscio is supported by a Royal Academy Chair in Emerging Technologies.

# References

1. Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

2. Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Art.Int. 116(1-2), 123–191 (2000)
3. Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals using heuris- tic search. In: AAAI. pp. 788–795 (2006)

4. Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with imperfect information and public actions. In: AAMAS. pp. 1268–1276 (2017)

5. Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Alternating-time temporal logic on finite traces. In: IJCAI. pp. 77–83 (2018), https://doi.org/10.24963/ijcai.2017/14

6. Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Decidable verification of multi-agent systems with bounded private actions. In: AAMAS. pp. 1865–1867 (2018)

7. Camacho, A., Triantafillou, E., Muise, C., Baier, J., McIlraith, S.: Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In: AAAI. pp. 3716–3724 (2017)

8. De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: Monitoring busi- ness metaconstraints based on LTL and LDL for finite traces. In: BPM. pp. 1–17 (2014)

9. De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: Insensi- tivity to infiniteness. In: AAAI. pp. 1027–1033 (2014)

10. De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: IJCAI. pp. 1558–1564 (2015)

11. De Giacomo, G., Vardi, M.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI. pp. 854–860 (2013)

12. Dima, C., Tiplea, F.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR abs/1102.4225 (2011), http://arxiv.org/abs/1102.4225

13. Emerson, E. A., Halpern, J.Y.: "sometimes" and "not never" revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986).

14. Emerson, E., Jutla, C., Sistla, A.: On model checking for the µ-calculus and its fragments. Theor. Comp. Science 258(1–2), 491–522 (2001)

15. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT (1995)

16. Filiot, E., N.J, Raskin, J.: Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design 39(3), 261–296 (2011).

17. Gerevini, A., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artificial Intelligence 173(5-6), 619–668 (2009). https://doi.org/10.1016/j.artint.2008.10.012

18. Gutierrez, J., Perelli, G., M.Wooldridge: Iterated games with LDL goals over finite traces. In: AAMAS. pp. 696–704 (2017)

19. Jamroga, W., van der Hoek, W.: Agents that know how to play. Fund. Inf. 62, 1–35 (2004)

20. Kominis, F., Geffner, H.: Multiagent online planning with nested beliefs and dialogue. In: ICAPS. pp. 186–194 (2017)

21. Kong, J., Lomuscio, A.: Model checking multi-agent systems against LDLK specifications on finite traces. In: AAMAS. pp. 166–174 (2018)

22. Kupferman, O., Piterman, N., Vardi, M.: Safraless compositional synthesis. In: CAV. pp. 31–44 (2006)

23. Montali, M., Pesic, M., van der Aalst, W., Chesani, F., Mello, P., Storari, S.: Declarative specification and verification of service choreographiess. ACM Transactions on the Web (TWEB) 4(1), 3 (2010)

24. Pesic, M., Bosnacki, D., van der Aalst, W.: Enacting declarative languages using LTL: avoid- ing errors and improving performance. In: SPIN. pp. 146–161 (2010)

25. Pesic, M., van der Aalst, W.: A declarative approach for flexible business process manage- ment. In: BPM. pp. 169–180. LNCS 4103 (2006)

26. Tsai, M.H., Fogarty, S., Vardi, M., Tsay, Y.K.: State of Büchi complementation. LMCS 10(4) (2014). https://doi.org/10.2168/LMCS-10(4:13)2014

27. Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of pro- grams. In: STOC. pp. 240–251 (1985)