# On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

Nicolaj Ø Jensen, Kim G Larsen, Didier Lime, Jiří Srba

► To cite this version:

Nicolaj Ø Jensen, Kim G Larsen, Didier Lime, Jiří Srba. On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions. 36th International Conference on Concurrency Theory (CONCUR 2025), Aug 2025, Aarhus, Denmark. 10.4230/LIPIcs.CONCUR.2025.25 . hal-05513209

HAL Id: hal-05513209

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

Submitted on 16 Feb 2026

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_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

Nicolaj Ø. Jensen [ID

Department of Computer Science, Aalborg University, Denmark

Kim G. Larsen [ID

Department of Computer Science, Aalborg University, Denmark

Didier Lime [ID

Nantes Université, École Centrale Nantes, CNRS, LS2N, UMR 6004, F-44000 Nantes, France

Jiří Srba [ID

Department of Computer Science, Aalborg University, Denmark

## Abstract

Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed CTL verification in the abstract dependency graph (ADG) framework, which allows for easy creation of on-the-fly algorithms that only explore the state space as needed. In addition, we generalize the conventional inclusion check to the ADG framework which enables dynamic reductions of the dependency graph. Using the insights from the generalization, we present a novel abstraction that eliminates the need for inclusion checking altogether in our domain. We implement our algorithms in UPPAAL and our experiments show that while inclusion checking considerably enhances performance, our abstraction provides even more significant improvements, almost two orders of magnitude faster than the naive method. In addition, we outperform UPPAAL TIGA, which can verify only a strict subset of TATL. After implementing our new abstraction in UPPAAL TIGA, we also improve its performance by almost an order of magnitude.

**2012 ACM Subject Classification** Software and its engineering → Model checking; Theory of computation → Dynamic programming

**Keywords and phrases** Timed ATL, Symbolic Algorithms, Dependency Graphs, Timed Games

**Digital Object Identifier** 10.4230/LIPIcs.CONCUR.2025.25

**Related Version** Full Version: https://arxiv.org/abs/2506.07802

## Supplementary Material

Software (Reprod. Package): https://doi.org/10.5281/zenodo.15195408

**Funding** VILLUM INVESTIGATOR project S4OS and ANR project BisoUS ANR-22-CE48-0012.

# 1 Introduction

Correctness is essential for many real-time systems, including distributed communication networks, energy grid management, and air traffic control. Ensuring the correctness of such systems is challenging due to the number of concurrent internal and external components. The interleaved behavior of all these components leads to an exponential growth in the number of states, a phenomenon known as the state-space explosion problem [14]. Addressing this challenge is a core focus of the field of model checking. In this paper, we consider real-time systems with components controlled by more than two parties, some cooperative, others adversarial. Real examples of such systems include electronic circuits with multiple components, perhaps some counterfeit [27], and networks of routers located in different

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

© Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba;

licensed under Creative Commons License CC-BY 4.0

36th International Conference on Concurrency Theory (CONCUR 2025).

Editors: Patricia Bouyer and Jaco van de Pol; Article No. 25; pp. 25:1–25:19

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
25:2 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

<figure><img src="image_4.png" /><figcaption>(a) An example timed game $\mathcal{A}$ with three players: I, II, and III and a single clock $x$ that increases as time passes. Multiple TATL properties of the system are shown on the right.</figcaption></figure>

$$
I : \langle \ell, \nu \rangle \mapsto \begin{cases} a_1 & \text{if } \ell = \mathbf{A} \\ a_2 & \text{if } \ell = \mathbf{B} \wedge \nu(x) = 5 \\ \lambda & \text{otherwise} \end{cases} \quad III : \langle \ell, \nu \rangle \mapsto \begin{cases} a_3 & \text{if } \ell = \mathbf{B} \wedge \nu(x) \le 2 \\ a_6 & \text{if } \ell = \mathbf{D} \\ \lambda & \text{otherwise} \end{cases}
$$

(b) An example strategy profile for player I and III that witnesses $\mathcal{A} \models \langle\langle \text{I, III} \rangle\rangle (\neg \mathcal{U} \text{ Goal})$.

<figure><img src="image_5.png" /><figcaption>Figure 1</figcaption></figure>

countries [16, 6]. We model these systems as timed multiplayer games (TMG) and consider
properties described in timed alternating-time temporal logic (TATL) [14, 4]. TMGs are
generalized timed game automata [26, 7] and can have more than two players. Like in timed
games, each discrete action belongs to a specific player and can be executed only at the
discretion of that player. Consider the example TMG in Figure 1a with three players, I,
II, and III, and a single real-valued clock $x$, initially at 0, that increases as time passes.
From the starting location, **A**, player III has no strategy to ensure that the system reaches
the **Goal** location, expressed as $\mathcal{A} \nvDash \langle\langle \text{III} \rangle\rangle \diamond \text{Goal}$ in TATL. This is because player I can
wait in location **A** until $x > 3$ and then direct the system to location **C** without giving III
any influence. Here, the system can remain indefinitely. On the other hand, II can ensure
**Goal** is reached as I and III cannot leave the system in a location where II cannot make
progress. TATL also allows us to consider coalitions of collaborating players. If players
I and III work together, then they can ensure **Goal** is reached without visiting location
**C**, expressed as $\mathcal{A} \models \langle\langle \text{I, III} \rangle\rangle (\neg \mathcal{U} \text{ Goal})$. We also consider nested properties, such as
$\mathcal{A} \models \langle\langle \text{I} \rangle\rangle \Box \neg \langle\langle \text{III} \rangle\rangle \diamond \text{Goal}$ which states that I can ensure that in all reached states, III does not
have a strategy to ensure **Goal** is reached. Furthermore, timed properties add conditions on
the time passed. For example, $\mathcal{A} \nvDash \langle\langle \text{II} \rangle\rangle \diamond_{<5} \text{Goal}$ states that II cannot guarantee **Goal** is
reached strictly within 5 time units.

For verification, it is often unnecessary to explore the entire state space to determine
the correctness of a property. One approach that reduces unnecessary work is to decompose
the problem into sub-problems and lazily structure them in a dependency graph [25, 17, 18].
As the process unfolds, sub-problems eventually become trivial, and their solutions are
used to resolve the more complex dependent problems. In many cases, the root problem
can be answered without first constructing the entire dependency graph and the process
can terminate early. This framework was formalized in [17, 18] using extended abstract
dependency graphs (EADGs) and has been used to create on-the-fly algorithms for other
model checking domains [12, 13, 20].
## Our contributions

We develop an on-the-fly TATL algorithm within the EADG framework by providing a sound encoding of the problem. Our approach builds upon previous work involving encodings for timed systems and alternating-time temporal logic, showing their orthogonality, and we provide many semantic details that were left out in previous work. Since TATL is a superset of TCTL [1, 2, 4], our algorithm is also the first on-the-fly algorithm for TCTL with the generic freeze operator. Moreover, we formalize vertex merging in EADGs as a generalization of inclusion checking from prior work [13] and incorporate it into our encoding. In addition, this generalization also leads to an expansion abstraction that removes the need for conventional inclusion checking in our encoding altogether. Finally, we implement and evaluate various configurations of our algorithm and compare their performance to the state-of-the-art model checker for real-time games UPPAAL TIGA [13, 9]. Our configuration with inclusion checking is, as expected, on par with TIGA on the subset of formulae that TIGA can handle, however, incorporating our expansion abstraction improves performance by nearly an order of magnitude.

## Related work

The tool UPPAAL TIGA [13, 9], which has since been integrated in UPPAAL [19], uses a similar method to solve a simpler version of the problem: strategy synthesis in two-player timed games. In fact, [13] was published 20 years ago at CONCUR'05, and our paper brings the foundational work of that paper into the modern framework and expands it to the broader TATL logic. TIGA was the first to adapt the dependency graph-based on-the-fly algorithm by Liu and Smolka [25] to model checking, and the idea was eventually generalized into the EADG framework [17, 18]. TIGA relies on inclusion checking to merge vertices and improve performance, a detail that has not been generalized to the EADG framework until this paper. This paper also includes many semantic details that were left out in [13]. Alternating-time temporal logic (ATL), defined by T. Henzinger and R. Alur in [4] as an extension to branching-time logic [14], introduces ways to quantify over possible outcomes resulting from coalitions of players working together. ATL properties with a single coalition can be reduced to a synthesis problem in a two-player game, a problem that has already been intensively studied [26, 7, 15, 13]. However, it is also possible to nest the coalition quantifiers to express more intriguing properties. Recently, Carlsen et al. [12] used the EADG framework for on-the-fly verification of (untimed) ATL properties in concurrent games with multiple players. We extend this work to the setting of timed games and timed logics [1, 2]. An alternative approach to checking branching-time logic properties is the bottom-up algorithm [1, 14, 7]. This method begins by identifying all states that satisfy the relevant atomic propositions. It then iteratively propagates these results to compute states satisfying larger sub-properties until the original property is fully evaluated. While efficient when processing all reachable states is unavoidable, this approach may also waste time on unreachable states or irrelevant state-property combinations. Our on-the-fly algorithm mitigates these issues by computing only the necessary states and sub-properties on demand. Our new expansion abstraction relaxes the relevance criteria, bringing it closer to the bottom-up algorithm in this regard.

## Paper structure

In Section 2, we present the TMG formalism and TATL logic followed by the general EADG framework. Then we present our encoding of the TATL problem in EADGs in Section 3. In Section 4, we introduce vertex merging to EADGs and an updated algorithm, allowing us
to perform inclusion checking in our encoding, and we introduce our expansion abstraction. Finally, in Section 5, we evaluate our algorithm and compare it against UPPAAL TIGA on the problem instances where it is possible.

## 2 Preliminaries

We shall first introduce the model of timed games with multiple players as well as a timed logics for describing properties of such systems. Afterwards, we present the extended abstract dependency graph framework.

### 2.1 Timed Multiplayer Games

Let $X$ be a finite set of real-valued variables called *clocks*. Let $C(X)$ be the set of *clock constraints* over the clocks $X$ generated by the following abstract syntax:

$$ g ::= x \bowtie k \mid x - y \bowtie k \mid g_1 \land g_2 $$

where $k \in \mathbb{Z}$ and $x, y \in X$ and $\bowtie \in \{<, \leq, =, \geq, >\}$. Let $B(X) \subseteq C(X)$ be the subset that does not use any diagonal constraints of the form $x - y \bowtie k$. Let $\hat{B}(X) \subseteq B(X)$ be the subset that also does not use any constraints of the form $x < k$. A clock valuation $\nu: X \to \mathbb{R}_{\geq 0}$ assigns each clock a real value. The valuation denoted $\overrightarrow{0}$ assigns 0 to each clock. We write $\nu[Y]$ for a valuation that assigns 0 to any clock $x \in Y$ and assigns $\nu(x)$ to any clock $x \in X \setminus Y$. If $\delta \in \mathbb{R}_{\geq 0}$ then $\nu + \delta$ denotes the valuation such that $(\nu + \delta)(x) = \nu(v) + \delta$ for all $x \in X$. If $g \in C(X)$, we write $\nu \models g$ and say that $\nu$ satisfies $g$ if replacing all clocks in $g$ with their respective value in $\nu$ makes the expression evaluate to true.

**Definition 1 (Timed Automaton).** A timed automaton (TA) is a 6-tuple $(L, \ell_{\text{init}}, X, A, T, I)$ where $L$ is a finite set of locations, $\ell_{\text{init}} \in L$ is the initial location, $A$ is a set of actions, $X$ is a finite set of real-valued clocks, $T \subseteq L \times B(X) \times A \times 2^X \times L$ is a finite set of edges each with a unique action from $A$, and $I: L \to \hat{B}(X)$ assigns an invariant to each location.

The semantics of a TA $A = (L, \ell_0, X, A, T, I)$ can be described with a labeled transition system. The states are pairs $(\ell, \nu)$ where $\ell \in L$ is a location and $\nu: X \to R_{\geq 0}$ is a valuation such that $\nu \models I(\ell)$ and $Q$ is the set of all states. Transition labels are discrete actions or real-valued delays, i.e. $A \cup R_{\geq 0}$, and the transition relation $\to$ is a union of the binary relations $\xrightarrow{a}$ and $\xrightarrow{\delta}$ defined over states as follows:

- $\langle \ell, \nu \rangle \xrightarrow{a} \langle \ell', \nu' \rangle$ if there exists an edge $\langle \ell, g, a, Y, \ell' \rangle \in T$ such that $v \models I(\ell) \land g, v' = v[Y]$, and $v' \models I(\ell')$, and

- $\langle \ell, \nu \rangle \xrightarrow{\delta} \langle \ell, \nu' \rangle$ if $\delta > 0$, $v \models I(\ell)$, $v' = v + \delta$, and $v' \models I(\ell)$.

A run in a TA is a sequence $\langle \ell_0, \nu_0 \rangle \xrightarrow{t_0} \langle \ell_1, \nu_1 \rangle \xrightarrow{t_1} \langle \ell_2, \nu_2 \rangle \cdots$ such that $t_i \in A \cup R_{\geq 0}$. A run is maximal if it contains an infinite number of discrete action transitions, ends with an infinite number of delay transitions that sum to $\infty$ (divergence), or no transition is possible in the final state (a deadlock). For the latter case, there is always a well-defined final state since invariants of the form $x < k$ are disallowed. The set $\text{Runs}_A(\langle \ell, \nu \rangle)$ contains all maximal runs starting from $\langle \ell, \nu \rangle$. Given a run $\sigma$ we write $\sigma[i]$ for the $i$th state $\langle \ell_i, \nu_i \rangle$.

**Definition 2 (Timed Multiplayer Game).** A timed multiplayer game (TMG) with $N$ players is a timed automaton where the actions $A$ have been partitioned into $N$ disjoint sets, $A = A_1 \cup \cdots \cup A_N$. We denote by $\Sigma = \{1, \dots, N\}$ the set of players.
## Strategies and outcomes

A (memoryless) strategy for a player $p \in \Sigma$ is a function $f_p : Q \to A_p \cup \{\lambda\}$ that maps each state to $\lambda$ or a discrete action that is enabled in the state and belongs to $p$. The strategy informs $p$ what to do in the given state and $\lambda$ is a special symbol indicating that player $p$ should do nothing and wait. For states where a delay transition is not possible, a strategy can only output $\lambda$ if the player has no enabled actions available. Let $F_p$ be the set of all strategies for the player $p$. By $\xi_S$ we denote a strategy profile that assigns to each player $p \in S \subseteq \Sigma$ a strategy $f_p \in F_p$, and $\Xi(S)$ is the set of all such strategy profiles over $S$. When players pick actions according to their strategies, it restricts the possible runs. We write $Out_A(\xi_S, \langle l, v \rangle) \subseteq Runs_A(\langle l, v \rangle)$ for the subset of outcomes (runs) induced when the players of $S$ adhere to the strategies of $\xi_S$.

**► Definition 3 (Outcomes).** Let $\mathcal{A} = \langle L, \ell_{init}, X, A, T, I \rangle$ be a TMG with players $\Sigma = \{1, \dots, N\}$, let $\langle \ell_0, \nu_0 \rangle$ be a state where $\nu_0 \models I(\ell_0)$, and let $\xi_S \in \Xi(S)$ be a strategy profile for $S \subseteq \Sigma$. A maximal run $\sigma = \langle \ell_0, \nu_0 \rangle \xrightarrow{t_0} \langle \ell_1, \nu_1 \rangle \xrightarrow{t_1} \langle \ell_2, \nu_2 \rangle \dots \in Runs_A(\langle \ell_0, \nu_0 \rangle)$ is in $Out_A(\xi_S, \langle \ell_0, \nu_0 \rangle)$ iff the following conditions hold:

- for all $i \ge 0$ such that $t_i = \delta \in \mathbb{R}_{\ge 0}$ we have that $\xi_S(p)(\langle \ell_i, \nu_i + \delta' \rangle) = \lambda$ for all $0 \le \delta' < \delta$ and all $p \in S$,

- for all $i \ge 0$ such that $t_i = a \in A$ we have either $a \notin \bigcup_{p \in S} A_p$ or $\xi_S(p)(\langle \ell_i, \nu_i \rangle) = a$ with $a \in A_p$ for some $p \in S$.

Note that we allow Zeno behavior (an infinite subsequence consisting of no delays) from both the coalition $S$ and the opposition $\bar{S}$.

## 2.2 Timed Alternating-Time Temporal Logic

The alternating-time temporal logic [4] is a logic that offers quantification over possible outcomes resulting from a coalition of players in a multiplayer game.

**► Definition 4 (Alternating-Time Temporal Logic).** Given a set of atomic propositions $\Pi$, a set of clocks $X$, and a set of players $\Sigma$, an alternating-time temporal logic (ATL) property conforms to the abstract syntax:

$$ \phi ::= \pi \mid g \mid \neg\phi_1 \mid \phi_1 \lor \phi_2 \mid \langle S \rangle \circ \phi_1 \mid \langle S \rangle(\phi_1 \mathcal{U} \phi_2) \mid [S](\phi_1 \mathcal{U} \phi_2) $$

where $\pi \in \Pi$, $g \in C(X)$, and $S \subseteq \Sigma$ is a coalition of players.

Given a TMG $\mathcal{A}$ with players $\Sigma = \{1, \dots, N\}$ and a function $Lab : L \to 2^\Pi$ labeling locations with atomic propositions, the satisfaction relation $\models$ over states and ATL properties is defined inductively as follows:

- $\langle l, v \rangle \models \pi$ iff $\pi \in Lab(l)$,

- $\langle l, v \rangle \models g$ iff $v \models g$,

- $\langle l, v \rangle \models \neg\phi$ iff $\langle l, v \rangle \nvDash \phi$,

- $\langle l, v \rangle \models \phi_1 \lor \phi_2$ iff there exists a strategy profile $\xi_S \in \Xi(S)$ such that for all maximal runs $\sigma = \langle \ell_0, \nu_0 \rangle \xrightarrow{t_0} \langle \ell_1, \nu_1 \rangle \xrightarrow{t_1} \langle \ell_2, \nu_2 \rangle \dots \in Out_A(\xi_S, \langle \ell, v \rangle)$ we have $\sigma[i+1] \models \phi_1$ where $i \ge 0$ is the smallest $i$ such that $t_i \in A$ and such an $i$ must exist,<fnref n="1" />

- $\langle l, v \rangle \models \langle S \rangle \circ \phi_1$ iff there exists a strategy profile $\xi_S \in \Xi(S)$ such that for all maximal runs $\sigma = \langle \ell_0, \nu_0 \rangle \xrightarrow{t_0} \langle \ell_1, \nu_1 \rangle \xrightarrow{t_1} \langle \ell_2, \nu_2 \rangle \dots \in Out_A(\xi_S, \langle l, v \rangle)$ we have $\sigma[i+1] \models \phi_1$ where $i \ge 0$ is the smallest $i$ such that $t_i \in A$ and such an $i$ must exist,<fnref n="1" />

<footnote n="1">¹ The next operator is usually left out of timed systems, but it is well-defined with action-based semantics like here.</footnote>
25:6 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

■ $\langle\ell, \nu\rangle \models \langle\langle S\rangle\rangle(\phi_1\mathcal{U}\phi_2)$ iff there exists a strategy profile $\xi_S \in \Xi(S)$ such that for all maximal runs $\sigma \in \text{Out}_A(\xi_S, \langle\ell, \nu\rangle)$ we have $\sigma \Vdash_r \phi_1\mathcal{U}\phi_2$ (defined below),

■ $\langle\ell, \nu\rangle \models \llbracket S\rrbracket(\phi_1\mathcal{U}\phi_2)$ iff for all strategy profiles $\xi_S \in \Xi(S)$ there exists a maximal run $\sigma \in \text{Out}_A(\xi_S, \langle\ell, \nu\rangle)$ such that $\sigma \Vdash_r \phi_1\mathcal{U}\phi_2$, and for a maximal run $\sigma = \langle\ell_0, \nu_0\rangle \xrightarrow{t_0} \langle\ell_1, \nu_1\rangle \xrightarrow{t_1} \langle\ell_2, \nu_2\rangle \dots$ we have $\sigma \Vdash_r \phi_1\mathcal{U}\phi_2$ iff there exists an $i \ge 0$ such that:

■ for all $j < i$:

■ if $t_j \in \mathbb{R}_{\ge 0}$ then for all $\delta \in [0, t_j)$ we have $\langle\ell_j, \nu_j + \delta\rangle \models \phi_1$, or

■ if $t_j \in A$ instead then $\langle\ell_j, \nu_j\rangle \models \phi_1$, and

■ either $\langle\ell_i, \nu_i\rangle \models \phi_2$ or $t_i \in \mathbb{R}_{\ge 0}$ and there exists a $\delta \in [0, t_i)$ such that $\langle\ell_i, \nu_i + \delta\rangle \models \phi_2$, and for all $\delta' \in [0, \delta)$ we have $\langle\ell_i, \nu_i + \delta'\rangle \models \phi_1 \lor \phi_2$. We note that the disjunction $\phi_1 \lor \phi_2$ is necessary for timed big-step runs (instead of simply $\phi_1$). See [5] for details.

We note that $\llbracket\emptyset\rrbracket \equiv \exists$ and $\langle\langle\emptyset\rangle\rangle \equiv \forall$ and thus ATL is a superset of CTL [4]. Other notable abbreviations and equivalences are $\pi \lor \neg\pi \equiv \mathbf{true}$ and $\langle\langle S\rangle\rangle(\mathbf{true}\mathcal{U}\phi) \equiv \langle\langle S\rangle\rangle\diamond\phi$ and $\neg\langle\langle S\rangle\rangle\diamond\phi \equiv \llbracket S\rrbracket\Box\neg\phi$ and $\neg\langle\langle S\rangle\rangle \circ \phi \equiv \llbracket S\rrbracket \Box \neg\phi$.

**► Definition 5 (Timed ATL).** Timed alternating-time temporal logic (TATL) is the timed extension of ATL and is defined as ATL but with a new freeze operator: $z.\phi$, where $z \in X$ is a formula clock and $\phi$ is another TATL property. Note that a formula clock $z$ may not be used in the guards and invariants of the TMG. Given a state $\langle\ell, \nu\rangle \in Q$ we have $\langle\ell, \nu\rangle \models z.\phi$ iff $\langle\ell, \nu[z]\rangle \models \phi$.

The TATL freeze operator is commonly used indirectly through the more intuitive temporal operator $\mathcal{U}_{\triangleleft k}$ (where $\triangleleft \in \{<, \le\}$). For example, if $z$ is a new clock that does not appear elsewhere in the model or the formula then:

$$ \langle\langle S\rangle\rangle(\phi_1\mathcal{U}_{\triangleleft k}\phi_2) \equiv z.\langle\langle S\rangle\rangle((\phi_1 \wedge z \triangleleft k)\mathcal{U}\phi_2) $$

meaning that coalition $S \subseteq \Sigma$ has a strategy profile such that when adhered to, the system always reaches a state satisfying $\phi_2$ (strictly) within $k$ time units by a path where $\phi_1$ invariantly holds.

An example strategy profile that witnesses $\mathcal{A} \Vdash \langle\langle I, III\rangle\rangle(\neg\mathcal{C}\mathcal{U}\mathbf{Goal})$ for the TMG $\mathcal{A}$ in Figure 1a is given in Figure 1b. Since some states are never visited under this strategy, a partial strategy profile would also suffice as a witness. Such partial strategy witnesses enable our algorithm to terminate early for positive cases.

2.3 Extended Abstract Dependency Graphs

A partially ordered set $\langle\mathcal{D}, \sqsubseteq\rangle$ is a set $\mathcal{D}$ together with a binary relation $\sqsubseteq \subseteq \mathcal{D} \times \mathcal{D}$ that is reflexive, transitive and anti-symmetric. Given partially ordered sets $\langle\mathcal{D}_1, \sqsubseteq_1\rangle$ and $\langle\mathcal{D}_2, \sqsubseteq_2\rangle$, a function $f: \mathcal{D}_1 \rightarrow \mathcal{D}_2$ is *monotonically increasing* if $d \sqsubseteq_1 d'$ implies $f(d) \sqsubseteq_2 f(d')$ and *monotonically decreasing* if $d \sqsubseteq_1 d'$ implies $f(d) \sqsupseteq_2 f(d')$. When we just say *monotonic* we refer to increasing monotonicity. When a function has multiple inputs, monotonicity is with respect to a specific input. Unless we specify further, our monotonic multi-input functions are monotonic with respect to all inputs.

**► Definition 6 (Noetherian Ordering Relation).** A Noetherian ordering relation with a least element (NOR) is a triple $\langle\mathcal{D}, \sqsubseteq, \perp\rangle$ such that $\langle\mathcal{D}, \sqsubseteq\rangle$ is a partially ordered set, $\perp \in \mathcal{D}$ is the least element such that $\perp \sqsubseteq d$ for all $d \in \mathcal{D}$, and $\sqsubseteq$ satisfies the stabilizing ascending chain condition: for any chain $d_1 \sqsubseteq d_2 \sqsubseteq d_3 \sqsubseteq \dots$ there exists a point $i$ such that $d_i = d_j$ for all $j > i$.
<figure><img src="image_6.png" /><figcaption>(a) Example EADG.</figcaption></figure>

<table><caption>(b) Fixed points of components $C_0$ and $C_1$.</caption><thead><tr><th>v</th><th>α<sub>min</sub><sup>C<sub>0</sub></sup></th><th>α<sub>min</sub><sup>C<sub>1</sub></sup></th></tr></thead><tbody><tr><td>A</td><td>-</td><td>8</td></tr><tr><td>B</td><td>-</td><td>8</td></tr><tr><td>C</td><td>-</td><td>3</td></tr><tr><td>D</td><td>14</td><td>14</td></tr><tr><td>E</td><td>6</td><td>6</td></tr><tr><td>F</td><td>3</td><td>3</td></tr><tr><td>G</td><td>10</td><td>10</td></tr><tr><td>H</td><td>2</td><td>2</td></tr></tbody></table>

<figure><img src="image_7.png" /><figcaption>(c) The EADG after merge by $E \preceq_f F$ where $f(x) = x + 3$.</figcaption></figure>

**Figure 2** (a) An example EADG $\mathcal{G}$ over $\mathcal{D} = \langle \mathbb{N}_0 \cup \{\infty\}, \geq, \infty \rangle$. For each vertex $v$, the value function $\mathcal{E}(v)$ is displayed below the vertex, and the edges $E(v)$ are displayed using small circles inside the value functions, indicating the arity of the value function as well as which vertex assignment is used as input. Leaf nodes $F$, $G$, and $H$ have no dependencies and their value function is a constant function. Since $\mathcal{E}(B)$ is non-monotonic, the graph has two components $C_0$ and $C_1$ which are highlighted with dashed boxes. (b) The fixed-point assignments of component $C_0$ and $C_1$ found by a fixed-point computation. (c) The EADG $\mathcal{G}[E \mapsto_f F]$ where vertex $E$ has been removed through derivation $E \preceq_f F$. The value function of vertex $B$ is pointwise composed with the derive function $f$ on the second input which now points to the assignment of $F$ instead. Vertex $H$ now has no dependents and can be pruned.

**Definition 7 (Abstract Dependency Graph).** An abstract dependency graph (ADG) is tuple $(V, E, \mathcal{D}, \mathcal{E})$ where $V$ is a finite set of vertices, $E: V \to V^*$ is an edge function from vertices to strings of vertices, $\mathcal{D}$ is a NOR, and $\mathcal{E}(v) : \mathcal{D}^n \to \mathcal{D}$ is a monotonic value function at vertex $v \in V$ that takes $n$ arguments where $n = |E(v)|$.

We write $v \to v'$ if $v, v' \in V$ and $v' \in E(v)$, and $\to^+$ denotes the transitive closure of $\to$. The empty string of vertices is denoted $\varepsilon$. Vertices $v$ where $E(v) = \varepsilon$ have constant value functions by definition.

**Definition 8 (Extended Abstract Dependency Graph).** An extended abstract dependency graph (EADG) is a tuple $(V, E, \mathcal{D}, \mathcal{E})$ where $V, E$, and $\mathcal{D}$ are defined as for ADGs, but now $\mathcal{E}(v) : \mathcal{D}^n \to \mathcal{D}$ is a (possibly non-monotonic) value function at vertex $v \in V$ that takes $n$ arguments with $n = |E(v)|$. Furthermore, if $\mathcal{E}(v)$ is non-monotonic, then $v$ is not in a cycle, i.e. it is not the case that $v \to^+ v$.

EADGs can be used to encode and solve various problems. Each vertex in the graph represents a problem and the NOR values $\mathcal{D}$ represent possible answers to problems with increasing accuracy. The value function at each vertex describes how the answer to the problem represented by the vertex can be derived from the answers to other (sub)problems. To describe this formally, we must partition the graph into components. Consider the function:

$$ \begin{aligned} dist(v) &= \max\{m \in \mathbb{N} \mid \exists v_0 v_1 \cdots v_n \in V^*, v = v_0, \forall i \in \{1, \dots, n\}, v_{i-1} \to v_i, \\ & \qquad m = |\{v_i \mid \mathcal{E}(v_i) \text{ is non-monotonic}\}| \} \end{aligned} \quad (1) $$

describing how many non-monotonic value functions a vertex depends on. Since an EADG has no cycles with non-monotonic functions, $dist(v)$ is well-defined. The subgraphs induced by $dist$ are called components and $C_i \subseteq V$ is the $i$th component where $dist(v) \le i$ for all $v \in C_i$. Component $C_0$ depends only on monotonic value functions.
25:8 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

Let $\alpha: V \to \mathcal{D}$ be an assignment from vertices to NOR values with $\alpha_{\perp}$ being the assignment such that $\alpha_{\perp}(v) = \perp$ for all vertices $v \in V$. Let $F_0$ be an update function such that:

$$F_0(\alpha)(v) = \mathcal{E}(v)(\alpha(v_1), \alpha(v_2), \dots, \alpha(v_n)) \qquad (2)$$

where $v \in C_0$ and $E(v) = v_1v_2\dots v_n$. Since all value functions in $C_0$ are monotonic and $\mathcal{D}$ is a NOR, repeated application of $F_0$ on $\alpha_{\perp}$ eventually reaches a least fixed point, i.e. there exists an $m > 0$ such that $F_0^m(\alpha_{\perp}) = F_0^{m+1}(\alpha_{\perp})$. We denote this fixed point $\alpha_{\min}^{C_0}$. For each component $C_i$ where $i > 0$ the update function $F_i$ is defined as follows:

$$F_i(\alpha)(v) = \begin{cases} \mathcal{E}(v)(\alpha(v_1), \alpha(v_2), \dots, \alpha(v_n)) & \text{if } \mathcal{E}(v) \text{ is monotonic} \\ \mathcal{E}(v)(\alpha_{\min}^{C_{i-1}}(v_1), \alpha_{\min}^{C_{i-1}}(v_2), \dots, \alpha_{\min}^{C_{i-1}}(v_n)) & \text{otherwise} \end{cases} \qquad (3)$$

where $E(v) = v_1v_2\dots v_n$ and the assignment $\alpha_{\min}^{C_{i-1}}$ is the minimal fixed point on component $C_{i-1}$, i.e. the fixed points are defined inductively [18]. Finally, let $C_{\max}$ be the component associated with the greatest dist in EADG $G$, and let $\alpha_{\min}^G$ denote $\alpha_{\min}^{C_{\max}}$. Given a vertex $v_0 \in V$, the value $\alpha_{\min}^G(v_0)$ can be efficiently found using the sound and complete on-the-fly algorithm introduced in [18].

A small example EADG can be seen in Figure 2a with the NOR $\mathcal{D} = \langle \mathbb{N}_0 \cup \{\infty\}, \geq, \infty \rangle$. In this domain, chains are descending, stabilizing before or at 0. In Figure 2b we show the minimum fixed-point assignment of the components in the example EADG.

3 Encoding TATL to EADGs

In this section we will introduce our symbolic encoding of the TATL problem to EADGs.

Symbolic Operations on Zones and Federations

Due to the uncountable size of the state space, automated verification of timed automata groups the concrete states into effectively representable sets of states and valuations [1, 10]. We shall now define some useful operators on such sets. Let $[[g]] = \{\nu \in \mathbb{R}_{\geq 0}^X | \nu \models g\}$ be the set of all valuations satisfying $g \in C(X)$. A zone is a set $Z \subseteq \mathbb{R}_{\geq 0}^X$ of valuations where for some $g \in C(X)$ we have $[[g]] = Z$. A finite union of zones is called a federation. If $W \subseteq \mathbb{R}_{\geq 0}^X$ is a set of valuations, then:

- $W^{\perp} = \{\nu + \delta | \nu \in W, \delta \in \mathbb{R}_{\geq 0}\}$ are the timed successors of $W$,

- $W^{\perp} = \{\nu' \in \mathbb{R}_{\geq 0}^X | \exists \nu \in W, \exists \delta \in \mathbb{R}_{\geq 0}, \nu' + \delta = \nu\}$ are the timed predecessors of $W$,

- $W[Y] = \{\nu[Y] | \nu \in W\}$ is a reset of the clocks $Y \subseteq X$ in $W$,

- $W^{\#x} = \{\nu' \in \mathbb{R}_{\geq 0}^X | \exists \nu \in W, \forall y \in X, y \neq x \implies \nu(y) = \nu'(y)\}$ frees clock $x \in X$ in $W$.

Zones are closed under all the above operations [10]. Now consider a set of states $Q' \subseteq Q$ of a timed automaton $\langle L, \ell_{\text{init}}, X, A, T, I \rangle$. We extend these operations on clock valuations to the sets of states such that if $F \in \{\cdot^{\perp}, \cdot^{\perp}, [Y], \cdot^{\#x}\}$ then $F(Q') = \{\langle \ell, \nu' \rangle | \exists \langle \ell, \nu \rangle \in Q', \nu' \in F(\{\nu\}) \cap [[I(\ell)]]\}$. Given an action $a \in A$, we define the discrete $a$-predecessors and $a$-successors as $Pred_a(Q') = \{\langle \ell, \nu \rangle | \exists \langle \ell', \nu' \rangle \in Q', \langle \ell, \nu \rangle \xrightarrow{a} \langle \ell', \nu' \rangle\}$ and $Post_a(Q') = \{\langle \ell, \nu \rangle | \exists \langle \ell', \nu' \rangle \in Q', \langle \ell', \nu' \rangle \xrightarrow{a} \langle \ell, \nu \rangle\}$, respectively. Both $Pred_a$ and $Post_a$ preserve zones and federations [10]. When the automata is a TMG with players $\Sigma = \{1, \dots, N\}$ and $S \subseteq \Sigma$ is a coalition, then we let $A_S$ denote $\bigcup_{p \in S} A_p$. The $S$-controllable discrete predecessors of the coalition is defined by $Pred_S(Q') = \bigcup_{a \in A_S} Pred_a(Q')$. Similarly, the $S$-uncontrolled
discrete predecessors is Pred<sub>S</sub>(Q') where S = Σ \ S. Safe timed predecessors are those that avoid a set of states Q'' ⊆ Q even as time elapses. As defined in [13]:

$$Pred_{\lambda}(Q', Q'') = \{ \langle \ell, \nu - \delta \rangle \mid \langle \ell, \nu \rangle \in Q', \delta \ge 0, \forall \delta' \in [0, \delta], \langle \ell, \nu - \delta' \rangle \notin Q'' \}.$$

The states of Q' where time cannot pass are defined as $Q'^{\lambda} = \{\langle \ell, \nu \rangle \in Q' | \exists x \le k \in I(\ell), \nu(x) = k\}$. These states are also called time-locked. We note that the $^{\lambda}$ operator preserves federations. Finally, let Zone(Q) ⊆ 2Q be all subsets of Q that can be represented with a location-zone pair $\langle \ell, Z \rangle$ (also called a symbolic state), and let Fed(Q) ⊆ 2Q be all subsets of Q that can be represented with a location-federation pair $\langle \ell, \cup_i Z_i \rangle$.

## The Encoding

We shall now encode the TATL problem on TMGs as an EADG G in order to answer the question: given a TMG A = (L, $\ell_{init}$, X, A, T, I) with players Σ = {1, ..., N} and a TATL formula $\phi_0$, is it the case that $\langle \ell_{init}, \vec{0} \rangle \models \phi_0$? The vertices in EADG will have the form $\langle R, \phi \rangle$ where R ∈ Zone(Q) is a symbolic state and $\phi$ is a TATL formula (a sub-formula of $\phi_0$). We shall sometimes specify the location and zone of R and write $\langle \ell, Z, \phi \rangle$ for vertices instead, but the notation is often simpler for sets of states so we use R in those cases. Our root vertex is $\langle \ell_{init}, \{\vec{0}\}^{\lambda} \cap [I(\ell_{init})], \phi_0 \rangle$ and all dependencies of all vertices are generated using operators that preserve symbolic states. Without loss of generality, we assume all clocks are bounded<fnref n="2" /> [13, 10] and hence there are only finitely many symbolic states in practice, and therefore the dependency graph is finite. Our assignment domain is the NOR $\langle Fed(Q), \subseteq, \emptyset \rangle$ and we typically denote elements from our NOR using W. We restrict ourselves such that $\alpha_{\min}^{G}(\langle R, \phi \rangle) \subseteq R$ by construction and our goal is that $\langle \ell, \nu \rangle \in \alpha_{\min}^{G}(\langle R, \phi \rangle)$ iff $\langle \ell, \nu \rangle \models \phi$. The value functions of our EADG rely on the helper function Forceable<sub>S</sub>(W<sub>φ₁</sub>, W<sub>φ₂</sub>, W) and its counterpart Unavoidable<sub>S</sub>(W<sub>φ₁</sub>, W<sub>φ₂</sub>, W) where S is a coalition of players, W<sub>φ₁</sub> and W<sub>φ₂</sub> are sets of states (typically associated with two TATL formulae), and W is a set of states. We have $\langle \ell, \nu \rangle \in Forceable_S(W_{\phi_1}, W_{\phi_2}, W)$ if and only if there exists a $\delta \ge 0$ such that $\langle \ell, \nu \rangle \stackrel{\delta}{\rightarrow} \langle \ell, \nu + \delta \rangle$ and

- for all $\delta' \in [0, \delta]$ either $\langle \ell, \nu + \delta' \rangle \in W_{\phi_2}$, or $\langle \ell, \nu + \delta' \rangle \in W_{\phi_1}$ and for all $a_i \in A_S$ if $\langle \ell, \nu + \delta' \rangle \stackrel{a_i}{\rightarrow} \langle \ell', \nu' \rangle$ then $\langle \ell', \nu' \rangle \in W$,

- and additionally

- $\langle \ell, \nu + \delta \rangle \in W_{\phi_2}$, or

- $\langle \ell, \nu + \delta \rangle \stackrel{a_j}{\rightarrow} \langle \ell', \nu' \rangle \in W$ for some $a_j \in A_S$, or

- $\langle \ell, \nu + \delta \rangle \stackrel{\delta''}{\rightarrow} \langle \ell', \nu' \rangle \in W$ for some $a_j \in A_S$.

That is, the set is the subset of $W_{\phi_1} \cup W_{\phi_2}$ where coalition S can controllably get to $W_{\phi_2}$ with delays or to W with delays and a discrete action all while staying in $W_{\phi_1}$ until then. The set can be described symbolically as follows:

$$ \text{Forceable}_S(W_{\phi_1}, W_{\phi_2}, W) = \text{Pred}_{\lambda}(W_{\phi_2} \cup \text{Pred}_S(W) \cup \mathcal{H}, [\overline{W_{\phi_1}} \cup \text{Pred}_{\overline{S}}(\overline{W})] \setminus W_{\phi_2}) \quad (4) $$

$$ \text{where } \mathcal{H} = Q^{\lambda} \cap \text{Pred}_{\overline{S}}(W) \setminus \text{Pred}_{\Sigma}(\overline{W}). \quad (5) $$

Similarly, we have $\langle \ell, \nu \rangle \in Unavoidable(W_{\phi_1}, W_{\phi_2}, W)$ if and only if there exists a $\delta \ge 0$ such that $\langle \ell, \nu \rangle \stackrel{\delta}{\rightarrow} \langle \ell, \nu + \delta \rangle$ and

<footnote n="2">² It is also possible to use extrapolation techniques instead [8].</footnote>
25:10 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

for all $\delta' \in [0, \delta)$ we have $\langle \ell, \nu + \delta' \rangle \in W_{\phi_1}$ and for all $a_i \in A_S$ if $\langle \ell, \nu + \delta' \rangle \xrightarrow{a_i} \langle \ell', \nu' \rangle$ then $\langle \ell', \nu' \rangle \in W$,

and additionally

$\langle \ell, \nu + \delta \rangle \in W_{\phi_2}$, or

$\langle \ell, \nu + \delta \rangle \in W_{\phi_1}$ and $\langle \ell, \nu + \delta \rangle \xrightarrow{a_j} \langle \ell', \nu' \rangle \in W$ for some $a_j \in A_{\overline{S}}$, or

$\langle \ell, \nu + \delta \rangle \in W_{\phi_1}$ and $\langle \ell, \nu + \delta \rangle \xrightarrow{\delta''} \langle \ell', \nu' \rangle$ for any $\delta'' > 0$ and for all $a_i \in A_S$ if $\langle \ell, \nu + \delta' \rangle \xrightarrow{a_i} \langle \ell', \nu' \rangle$ then $\langle \ell', \nu' \rangle \in W$ and there exists at least one $a_i \in A_S$ such that $\langle \ell, \nu + \delta \rangle \xrightarrow{a_i} W$.

That is, the set contains the subset of $W_{\phi_1} \cup W_{\phi_2}$ where coalition $S$ cannot avoid that the system stays in $W_{\phi_1}$ and eventually reaches $W_{\phi_2}$ through delays, or reaches $W$ through a delay followed by a discrete action. The set can be described symbolically as follows:

$$ \text{Unavoidable}_S(W_{\phi_1}, W_{\phi_2}, W) = \text{Pred}_{\lambda}(W_{\phi_2} \cup \text{Pred}_{\overline{S}}(W) \cup \mathcal{H}, [\overline{W_{\phi_1}} \cup (\text{Pred}_S(\overline{W}) \setminus \text{Pred}_{\overline{S}}(W))] \setminus W_{\phi_2}) \quad (6) $$

$$ \text{where } \mathcal{H} = Q^{\mathcal{X}} \cap \text{Pred}_S(W). \quad (7) $$

Assuming a fixed ordering of actions $A = \{a_1, \dots, a_n\}$, we now define $E(v)$ and $\mathcal{E}(v)$ of the EADG as follows based on the form of vertex $v$:

Case $v = \langle R, \pi \rangle$: $E(v) = \varepsilon$ and $\mathcal{E}(v)(\varepsilon) = \{\langle \ell, \nu \rangle \in R \mid \pi \in \text{Lab}(\ell)\}$.

Case $v = \langle R, g \rangle$: $E(v) = \varepsilon$ and $\mathcal{E}(v)(\varepsilon) = \{\langle \ell, \nu \rangle \in R \mid \nu \in [g]\}$.

Case $v = \langle R, \neg\phi \rangle$: $E(v) = \langle R, \phi \rangle$ and $\mathcal{E}(v)(W) = R \setminus W$.

Case $v = \langle R, \phi_1 \lor \phi_2 \rangle$: $E(v) = \langle R, \phi_1 \rangle \langle R, \phi_2 \rangle$ and $\mathcal{E}(v)(W_1, W_2) = W_1 \cup W_2$.

Case $v = \langle R, \phi_1 \land \phi_2 \rangle$: $E(v) = \langle R, \phi_1 \rangle \langle R, \phi_2 \rangle$ and $\mathcal{E}(v)(W_1, W_2) = W_1 \cap W_2$.

Case $v = \langle R, z.\phi \rangle$: $E(v) = \langle R[z]^\mathcal{X}, \phi \rangle$ and $\mathcal{E}(v)(W) = (W \cap Q[z])\#z \cap R$.

Case $v = \langle R, \langle S \rangle \rangle \circ \phi$:

$$ \begin{gathered} E(v) = v_{a_1} \dots v_{a_n} \quad \text{where } v_{a_i} = \langle \text{Post}_{a_i}(R)^{\mathcal{X}}, \phi \rangle \\ \mathcal{E}(v)(W_{a_1}, \dots, W_{a_n}) = \text{Forceable}_S(R, \emptyset, \bigcup_i W_{a_i}) \end{gathered} $$

Case $v = \langle R, \langle S \rangle \rangle (\phi_1 U \phi_2)$:

$$ \begin{gathered} E(v) = \langle R, \phi_1 \rangle \langle R, \phi_2 \rangle v_{a_1} \dots v_{a_n} \quad \text{where } v_{a_i} = \langle \text{Post}_{a_i}(R)^{\mathcal{X}}, \langle S \rangle \rangle (\phi_1 U \phi_2) \\ \mathcal{E}(v)(W_{\phi_1}, W_{\phi_2}, W_{a_1}, \dots, W_{a_n}) = \text{Forceable}_S(W_{\phi_1}, W_{\phi_2}, \bigcup_i W_{a_i}) \end{gathered} $$

Case $v = \langle R, \llbracket S \rrbracket (\phi_1 U \phi_2) \rangle$:

$$ \begin{gathered} E(v) = \langle R, \phi_1 \rangle \langle R, \phi_2 \rangle v_{a_1} \dots v_{a_n} \quad \text{where } v_{a_i} = \langle \text{Post}_{a_i}(R)^{\mathcal{X}}, \llbracket S \rrbracket (\phi_1 U \phi_2) \rangle \\ \mathcal{E}(v)(W_{\phi_1}, W_{\phi_2}, W_{a_1}, \dots, W_{a_n}) = \text{Unavoidable}_S(W_{\phi_1}, W_{\phi_2}, \bigcup_i W_{a_i}) \end{gathered} $$

We remark that the elements of the NOR $\langle \text{Fed}(Q), \subseteq, \emptyset \rangle$ have finite representations using the data structure known as a *difference bound matrix* [10, 14]. All value functions are effectively computable since all constituent operations have known algorithms on difference bound matrices [10, 13].

In Figure 3, we show a fragment of the dependency graph generated when checking if $\phi = \langle \text{I, III} \rangle (\neg \mathcal{C} \cup \mathcal{U} \text{ Goal})$ holds in the initial state of $\mathcal{A}$ from Figure 1a. Eventually, the algorithm assigns $\llbracket x \le 3 \rrbracket$ to the vertex $\langle \mathbf{A}, x \le 4, \phi \rangle$ and then we can terminate as we now know that the $\phi$ holds for the initial state $\langle \mathbf{A}, \bar{0} \rangle$.

We will now state the correctness of the encoding and its supporting lemma.
<figure><img src="image_8.png" /><figcaption>Figure 3 A fragment of the EADG for $\phi = \langle\langle I, III \rangle\rangle(\neg C \cup Goal)$ in $\mathcal{A}$ from Figure 1a.</figcaption></figure>

**► Lemma 9 (Monotonically Safe).** The EADG encoding of TATL has no cycles of non-monotonic value functions and $dist(\langle R, \phi \rangle)$ is the greatest number of nested negations in $\phi$.

**► Theorem 10 (Encoding Correctness).** Given a TMG $\mathcal{A} = \langle L, \ell_{init}, X, A, T, I \rangle$, a set of states $R \in Zone(Q)$ such that $R = R^{\uparrow}$, a state $\langle \ell, \nu \rangle \in R$, and a TATL formula $\phi$, then $\langle \ell, \nu \rangle \models \phi$ iff $\langle \ell, \nu \rangle \in \alpha_{\min}^{G}(\langle R, \phi \rangle)$ using the presented EADG encoding of TATL.

## 3.1 Unsatisfied states

We now detail an improvement also investigated in [13]. In the encoding presented above, the NOR domain represents the states for which the formula is definitely satisfied. It is also possible to define an encoding in which the NOR domain represents the states in which the formula is definitely not satisfied. It is easy to see that the composition of two NORs is also a NOR [17], so we can do both simultaneously. If the initial state is ever included in the set of unsatisfied valuations then we know that the property does not hold. Hence, with this extension, we can terminate early for many negative cases as well. The encoding using the unsat NOR is trivial for clock constraints $g \in C(X)$, and operators $\wedge, \vee$, and $\neg$, but for completeness, we state the encoding of formulae containing the $\bigcirc$ and $\cup$ operator below. For all $v \in V$, we use the same edges $E(v)$, but different value functions, denoted $\mathcal{E}^c$, for updating the unsatisfied part of the composed NOR. Here $M$ is used to denote elements in the unsat NOR and we assume the same ordering of actions $A = \{a_1, \dots, a_n\}$ from earlier:

- Case $v = \langle R, \langle\langle S \rangle\rangle \circ \phi$: $\mathcal{E}^c(v)(M_{a_1}, \dots, M_{a_n}) = Unavoidable_S(R, \emptyset, \bigcup_i M_{a_i})$

- Case $v = \langle R, \langle\langle S \rangle\rangle(\phi_1 \cup \phi_2)$:

$$ \mathcal{E}^c(v)(M_{\phi_1}, M_{\phi_2}, M_{a_1}, \dots, M_{a_n}) = Unavoidable_S(M_{\phi_2}, M_{\phi_1}, \bigcup_i M_{a_i}) $$

- Case $v = \langle R, \llbracket S \rrbracket(\phi_1 \cup \phi_2)$:

$$ \mathcal{E}^c(v)(M_{\phi_1}, M_{\phi_2}, M_{a_1}, \dots, M_{a_n}) = Forceable_S(M_{\phi_2}, M_{\phi_1}, \bigcup_i M_{a_i}) $$

As seen, the difference between $\mathcal{E}$ and $\mathcal{E}^c$, is that every use of *Forceable* has been replaced by *Unavoidable*, and vice versa, and the terms involving $\phi_1$ and $\phi_2$ have been swapped in $\mathcal{U}$ formulae.

# 4 Dynamical Vertex Merge in EADGs

Usually, automated verification of timed systems takes advantage of inclusion checking, i.e. if one discovered symbolic state is included within another, then there is no reason to investigate the smaller one. To do this in the EADG framework, we must first introduce the general concept of vertex merging, which can be used to dynamically reduce the size of the graph.
Consider the NOR $\langle D, \sqsubseteq, \perp \rangle$ and an EADG $G = \langle V, E, D, \mathcal{E} \rangle$. If $u \in V^*$ is a string of vertices, then $u[i]$ denotes the $i$th vertex in the string and $u[v_1 \mapsto v_2]$ denotes the string $u$ where all occurrences of $v_1$ are replaced with $v_2$. Given an $n$-ary function $h : D^n \to D$, a unary function $f : D \to D$ and an index $i$, $1 \le i \le n$, we use $\circ_i$ to denote pointwise function composition on the $i$th input, defined as $(h \circ_i f)(x_1, \dots, x_n) = h(x_1, \dots, f(x_i), \dots, x_n)$, and its extension to multiple points $\circ_{\{i_1, \dots, i_k\}}$ given by $(h \circ_{\{i_1, \dots, i_k\}} f) = ((h \circ_{i_1} f) \circ_{i_2} \cdots) \circ_{i_k} f$ where notably $h \circ_{\emptyset} f = h$.

**Definition 11 (Derivation).** Let $v_1, v_2 \in V$ be vertices in EADG $G = \langle V, E, D, \mathcal{E} \rangle$ with $\mathrm{dist}(v_1) \le \mathrm{dist}(v_2)$ and let $f : D \to D$ be a monotonic function such that $f(\alpha_{\min}^G(v_2)) = \alpha_{\min}^G(v_1)$. We call $f$ a derive function and say that $v_1$ is derivable from $v_2$ through $f$, denoted by $v_1 \preceq_f v_2$.

Derivable vertices can be removed by merging without loss of precision.

**Definition 12 (Vertex Merge).** Let $v_1, v_2 \in V$ be vertices in EADG $G = \langle V, E, D, \mathcal{E} \rangle$ with $\mathrm{dist}(v_1) \le \mathrm{dist}(v_2)$ and let $f : D \to D$ be a monotonic function such that $v_1 \preceq_f v_2$. A vertex merge of $v_1$ into $v_2$ by $f$ is an operation that results in a new EADG denoted $G[v_1 \mapsto_f v_2] = \langle V', E', D, \mathcal{E}' \rangle$ where

- $V' = V \setminus \{v_1\}$,

- $E'(v) = E(v)[v_1 \mapsto v_2]$ for all $v \in V'$, and

- $\mathcal{E}'(v) = \mathcal{E}(v) \circ_I f$ for all $v \in V'$ where $I = \{i \mid E(v)[i] = v_1\}$.

We can now present a theorem that shows that a vertex merge does not change the minimum fixed-point value of any vertex in the dependency graph.

**Theorem 13 (Merge Preserves $\alpha_{\min}^G$).** Let $G = \langle V, E, D, \mathcal{E} \rangle$ be an EADG. If $v_1, v_2 \in V$ and $f : D \to D$ such that $v_1 \preceq_f v_2$ then $\alpha_{\min}^G(v) = \alpha_{\min}^{G[v_1 \mapsto_f v_2]}(v)$ for all $v \in V \setminus \{v_1\}$.

There are two main reasons why merging vertices can be beneficial when $v_1 \preceq_f v_2$. First, $f$ may be computationally cheaper than computing $\mathcal{E}(v_1)$. Second, it reduces the size of the graph, making other operations such as back-propagation of updates and pruning cheaper. However, if $f$ is expensive, it may be better to keep $v_1$ for the memoization it provides.

On Figure 2c, we show how the EADG from Figure 2a looks after a merge by derivation $E \preceq_f F$ where $f(x) = x + 3$. The existence of this derivation depends on the user's domain knowledge. In this case, the user might know that the first input to the max function of $E$ can never exceed 3, and hence its value can be derived from the second input $F$. As shown in the figure, the resulting graph is smaller and it is also possible to prune the vertex $H$.

## 4.1 Algorithm with Vertex Merging

Here we present our modification to the fixed-point algorithm from [18], enabling it to take advantage of vertex merging whenever $v_1 \preceq_f v_2$. The updated algorithm uses the following data structures:

- $\hat{v}$ is the current root vertex, initialized to $v_0$,

- $\hat{f}$ is the root deriving function, initialized to $id$ (the identity function),

- $\alpha : V \to D$ is the current assignment, initialized to $\alpha_\perp$,

- $W$ is a waiting set of vertices pending exploration or reevaluation,

- Pass is a set of explored vertices,

- $\mathrm{Dep} : V \to 2^V$ is a function that for each vertex $v$ returns a set of dependent vertices that should be reevaluated if the assignment of $v$ changes,
**Algorithm 1** Minimum fixed-point computation on an EADG. The lines highlighted in gray are our additions to the algorithm from [18].

Input: An EADG $(V, E, \mathcal{D}, \mathcal{E})$ and $v_0 \in V$
Output: $d \in \mathcal{D}$ s.t. $d \supseteq \alpha_{\min}(v_0)$
1 &nbsp;&nbsp;&nbsp;&nbsp;Dep$(v) = \emptyset$, Edges$(v) := E(v)$, and Eval$(v) = \mathcal{E}(v)$ for all $v \in V$;
2 &nbsp;&nbsp;&nbsp;&nbsp;$\hat{v} := v_0$; $\hat{f} := id$; $\alpha := \alpha_{\perp}$;
3 &nbsp;&nbsp;&nbsp;&nbsp;$W := \{v_0\}$; Pass := $\emptyset$; Active := $\{v_0\}$;
4 &nbsp;&nbsp;&nbsp;&nbsp;while $W \neq \emptyset$ do
5 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let $v \in W$ where $v$ is pickable;
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$W := W \setminus \{v\}$;
7 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v = \hat{v}$ or Dep$(v) \neq \emptyset$ then
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v \notin Pass$ then
9 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$v := \text{EXPLORE}(v)$;
10 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v \in Pass$ or $\mathcal{E}(v)$ is non-monotonic then
11 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let $v_1v_2 \dots v_k := \text{Edges}(v)$;
12 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$d := \mathcal{E}(v)(\alpha(v_1), \alpha(v_2), \dots, \alpha(v_k))$;
13 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $\alpha(v) \subseteq d$ then
14 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$W := W \cup \{u \in \text{Dep}(v) \mid \exists i. \text{Edges}(u)[i] = v \land i \notin \text{IGNORE}(\alpha, u)\}$;
15 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\alpha(v) := d$;
16 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v = \hat{v}$ and $\{1, 2, \dots, k\} \subseteq \text{IGNORE}(\alpha, \hat{v})$ then
17 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{return } \hat{f}(\alpha(\hat{v}))$;
18 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Pass := Pass $\cup \{v\}$;
19 &nbsp;&nbsp;&nbsp;&nbsp;return $\hat{f}(\alpha(\hat{v}))$
20 &nbsp;&nbsp;&nbsp;&nbsp;proc $\text{EXPLORE}(v)$:
21 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$v_* = v$;
22 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for $i = 1$ to $|\text{Edges}(v)|$ do
23 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let $v_i = \text{Edges}(v)[i]$ (generate it if needed);
24 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v_i \notin \text{Active}$ then
25 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Active} := \text{Active} \cup \{v_i\}$;
26 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall $v' \in \text{Active}$ where $v' \neq v_i$ do
27 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v_i \preceq_f v'$ for some $f$ then
28 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Active} := \text{Active} \setminus \{v_i\}$;
29 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Eval}(v) := \text{Eval}(v) \circ_i f$;
30 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Edges}(v) := \text{Edges}(v)[v_i \mapsto v']$;
31 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;continue outer loop;
32 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v' \preceq_f v_i$ for some $f$ then
33 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{REPLACE}(v', f, v_i)$;
34 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v' = \hat{v}$ then
35 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\hat{v} := v_i$;
36 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\hat{f} := \hat{f} \circ f$;
37 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v' = v_*$ then
38 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/* We replaced the vertex we were exploring. Record replacement. */
39 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$v_* := v_i$;
40 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v_* \neq v$ then
41 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return $\text{EXPLORE}(v_i)$
42 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Dep}(v_i) := \text{Dep}(v_i) \cup \{v\}$;
43 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $v_i \notin \text{Pass}$ then $W := W \cup \{v_i\}$;
44 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return $v$
45 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;proc $\text{REPLACE}(v_1, f, v_2)$:
46 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Dep}(v_2) := \text{Dep}(v_1)$;
47 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall $v' \in \text{Active} \cap \text{Dep}(v_1)$ do
48 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Eval}(v') := \text{Eval}(v') \circ_I f$ where $I = \{i \mid \text{Edges}(v')\}$;
49 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Edges}(v') := \text{Edges}(v')[v_1 \mapsto v_2]$;
50 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Pass} := \text{Pass} \setminus \{v_1\}$;
51 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{Active} := \text{Active} \setminus \{v_1\}$;
52 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$W := W \setminus \{v_1\}$;

- Edges: $V \to V^*$ is a function that for each vertex $v$ returns the current edges of $v$, initialized to $E(v)$,

- Eval($v$) : $\mathcal{D}^n \to \mathcal{D}$ is the current value function for vertex $v$ where $n = |E(v)|$, initialized to $\mathcal{E}(v)$,

- Active is a set of vertices that are (still) relevant for the root node $\hat{v}$ and considered during vertex merging.
25:14 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

The variables $\hat{v}$ and $\hat{f}$, and the data structures *Edges*, *Eval*(*v*), and *Active* are introduced by us to keep track of the reduced graph. In Algorithm 1, we show the EADG minimum fixed point computation algorithm from [18] updated with vertex merging.<fnref n="3" /> Incorporating vertex merging is relatively straightforward, but there are some edge cases to discuss. Vertex merging, highlighted in gray in Algorithm 1, occurs during the exploration of the vertex *v* (line 20-43). Each dependency $v_i$ of *v* is checked against all other active vertices. If $v_i$ can be merged into another active vertex $v'$, then we make *v* depend on $v'$ instead and make $v_i$ inactive (lines 27-31). If an active vertex $v'$ can be merged into $v_i$ then we make $v'$ inactive and replace $v'$ with $v_i$ in all our data structures (line 33). Additionally, if $v'$ is the root vertex $\hat{v}$ then we make $v_i$ the new root and update $\hat{f}$ by composing it with *f* so that the root assignment can be derived later (lines 34-36). In (presumably) rare cases, $v'$ is the explored vertex *v*, and if so, exploration must be restarted (lines 37-40).

**Lemma 14.** *At the start and end of the EXPLORE procedure, there exists no $v_1, v_2 \in Active$ such that $v_1 \neq v_2$ and $v_1 \preceq_f v_2$.*

**Theorem 15.** *The algorithm terminates and returns $\alpha_{\min}^G(v_0)$.*

4.2 Inclusion Checking as Derivation

Finally, we can do vertex merging in our problem domain. If one symbolic state is included within another and the associated query is the same, we merge the smaller one into the bigger one, since it contains the same valuations and more (conventional inclusion checking).

**Theorem 16 (Derivation by Intersection).** Let $\langle R, \phi \rangle, \langle R', \phi \rangle \in V$ be vertices and let $f_R : \mathcal{D} \to \mathcal{D}$ be a function such that $f_R(W) = W \cap R$. If $R \subseteq R'$, then $\langle R, \phi \rangle \preceq_{f_R} \langle R', \phi \rangle$ is a derivation.

4.3 Expansion Abstraction

It is known that EADGs can be refined using abstractions [18, 21, 22]. We now present a
simple abstraction for our domain that has superior performance compared to the inclusion
checking. As discussed, *R* is a symbolic state and $\langle \ell, Z, \phi \rangle$ is the actual form of vertices in
the dependency graph. For any vertex *v* = $\langle \ell, Z, \phi \rangle$ there exists a vertex *v'* = $\langle \ell, [I(\ell)], \phi \rangle$
and *v* can be merged into *v'* if it is generated. *v'* will not be merged into another vertex
as it is the biggest w.r.t. our derivation function in Theorem 16. Assuming that *v'* has a
high chance of being generated whenever *v* is, it makes sense to use an abstraction that
takes *v* directly to *v'* immediately, as the merge is likely to happen later anyway, and their
value functions require a similar number of operations but *v'* holds more information. Doing
so for all vertices induces a new smaller EADG where inclusion checking and merging are
unnecessary, as for every location there is a unique zone to be explored. In other words, our
abstracted vertices are defined only by the discrete part of the state. If the assumption is
wrong, i.e. *v'* is not discovered although *v* was, we may end up exploring states and edges
that are not relevant in practice as more discrete transitions may be enabled in the zone
$[I(\ell)]$ than in *Z*. However, we assess that timed automata with useless edges are rare in real
use cases, and most valuations are eventually reached. As a consequence, the downside of
this abstraction is insignificant, as also demonstrated by our experiments.

<footnote n="3">³ We also rearranged and renamed some procedures for clarity and omitted the pruning procedure. Additionally, IGNORE returns a set of indices instead of vertices in our version.</footnote>
Formally, we apply the following expansion abstraction $\mathcal{X}: V \to V$ to each vertex upon generation:

$$ \mathcal{X}(\langle \ell, Z, \phi \rangle) = \langle \ell, \llbracket I(\ell) \rrbracket, \phi \rangle. \qquad (8) $$

**► Theorem 17.** Applying abstraction $\mathcal{X}$ from Equation (8) to all vertices preserves encoding correctness, i.e. $\langle \ell, \nu \rangle \models \phi \text{ iff } \langle \ell, \nu \rangle \in \alpha_{\min}^{\mathcal{X}(G)}(\langle R, \phi \rangle)$ for every $\langle \ell, \nu \rangle \in R$.

If follows, that the vertex merging using the derivation we defined in Theorem 16 becomes redundant when using $\mathcal{X}$ because there is only one vertex per location-formula pair. The forward exploration done by the algorithm now only considers whether there exists a valuation such that a location can transition another location. This is less strict than a traditional reachability analysis, but it avoids expensive inclusion checks of zones while still restricting the backward propagation to the location-formula pairs we care about.

# 5 Implementation and Experimental Evaluation

We implement our algorithm in UPPAAL [19]. We use two stacks for the waiting list, one for vertices waiting for exploration and one for vertices waiting for updates. We always prioritize vertices from the update stack over vertices from the exploration stack, as this was found to be favorable in [24]. To improve performance, the EADG framework also allows us to specify a function IGNORE($\alpha, v$) describing which vertices of $E(v)$ can be skipped given the current assignment $\alpha$. We use the universally sound ignore function suggested in [18] by leveraging that $\alpha(\langle R, \phi \rangle) \subseteq R$. We can reduce the number of non-monotonic functions and thus graph components by rewriting the TATL formulae and pushing negations downward to the atomic propositions when possible.

## The Benchmark

We benchmark various configurations:

- EQUAL: The traditional EADG algorithm without vertex merging.

- INCL: We use vertex merging through inclusion checking as by Theorem 16.

- EXPAND: We use the expansion abstraction $\mathcal{X}$ described in Section 4.3 (and no vertex merging).

- +UNSAT: We additionally compute unsatisfied states as described in Section 3.1.

- TIGA(+UNSAT): The verifyta engine distributed with UPPAAL version 5.0.0 [9, 19] and specifically the TIGA algorithm.<fnref n="4" />

The benchmark suite consists of 3 types of TMG models, each instantiated in various sizes and with multiple associated TATL properties, totaling 236 model and query executions. The models are:

- Train Gate [3]: $N$ trains share the same bridge and a controller signals the trains if the bridge is occupied. Each train and the controller is a different player. Example queries include:

- $\langle T_1, T_2, T_3 \rangle \diamond num\_crossing \geq 1$; Can train $T_1$, $T_2$, and $T_3$ create a situation where more than one train is crossing at the same time? (No)

- $\langle T_1 \rangle \diamond crossed(T_1)$; Can train $T_1$ ensure that it eventually crosses the bridge? (No)

<footnote n="4">⁴ TIGA always keeps track of losing states without a strategy, i.e. the UNSAT modification.</footnote>
25:16 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

<figure><img src="image_9.png" /><figcaption>(a) Time usage.</figcaption></figure>

<caption>(b) Memory usage.</caption>

Figure 4 Cactus plots showing how many queries are answered within the indicated per-query resource limit. A configuration performs better if it can answer more queries using fewer resources.

<figure><img src="image_10.png" /><figcaption>(a) Time usage.</figcaption></figure>

<caption>(b) Memory usage.</caption>

Figure 5 Cactus plots showing how many TIGA-compatible queries are answered within the indicated per-query resource limit. A configuration performs better if it can answer more queries using fewer resources.

- Mexican Standoff [12] extended with reload time: *N* cowboys are shooting at each other and must reload their gun between each shot. Each cowboy is a different player and the gun reloading system is also a player. Example queries include:

- $\langle\langle C_1 \rangle\rangle$ (alive($C_1$)U $t > 1$); Can cowboy $C_1$ guarantee staying alive for 1 second? (No)

- $\langle\langle Guns, C_1, \dots, C_{\lceil N/2 \rceil} \rangle\rangle \Box \neg \bigvee_{c \in \{C_1, \dots, C_{\lceil N/2 \rceil}\}} alive(c)$; If half the cowboys cooperate and the gun reloading is on their side, can they ensure one of them survives? (Yes)

- Phase King [11]: A consensus algorithm for *N* nodes where time is divided into phases and rounds, and the king of each phase decides the voting tiebreaker. Each node is controlled by a unique player. Example queries include:

- $\langle\rangle \Diamond \text{consensus}(n_1, n_2, n_3)$; Node $n_1, n_2, n_3$ will reach consensus in some trace? (Yes)

- $\langle\rangle \Diamond \text{consensus}(n_1, n_2, n_3)$; Node $n_1, n_2, n_3$ will reach consensus in all traces? (No)

- $\langle\rangle \Box (\neg \text{consensus}(n_1, n_2, n_3) \lor \langle\langle n_1, n_2, n_3 \rangle\rangle \Box \text{consensus}(n_1, n_2, n_3))$; If nodes $n_1, n_2,$ and $n_3$ have consensus, can they stay in consensus? (Yes, if $N \le 5$)

Evaluation

Performance comparison of the configurations can be seen in Figure 4. Here the query executions are ordered (independently for each method) by their running time. Note that the y-axis is logarithmic. The INCL configuration using vertex merging is more than one order of magnitude faster than the EQUAL configuration using no merging, and EXPAND is almost
another order of magnitude faster for the most difficult instances. The UNSAT modification further improves the three configurations matching the conclusion in [13]. We find a similar improvements for memory usage. As described in Section 4.3, EXPAND may explore edges unnecessarily, since the abstraction enables all transitions in a location, assuming they will be relevant eventually. In the plots, we see that the EXPAND configuration performs worse on easy queries since these extra edges hinder early termination. However, after just 1 second this downside is eliminated by the advantages of the method.

Of our 236 total queries, 150 have no nested coalitions and can be solved by UPPAAL TIGA as well. However, for a large portion of them, modifications to the TMG model are required to get the edges' controllability to correspond to the actions of the coalition. In Figure 5, we compare the performance with TIGA on this subset of 150 queries. As expected, INCL+UNSAT and TIGA+UNSAT have similar performance on challenging queries, as these two configurations are very similar in practice. Our implementation seems slightly faster on easy queries. When we add the EXPAND abstraction to TIGA and remove its now redundant inclusion checking (configuration TIGA+EXPAND+UNSAT), the runtime performance matches that of our EXPAND+UNSAT, almost an order of magnitude faster than the previous state-of-the-art TIGA implementation.

A reproducibility package is available at [23].

# 6 Conclusion

We presented an encoding of the timed alternating-timed temporal logic problem in the extended abstract dependency graph (EADG) framework. This involved combining previous work on timed games, timed CTL, and alternating-time temporal logic. Our work is thus an example of how various encodings of model-checking problems in the EADG framework are orthogonal and can be combined to solve the combined logic extensions. We also took this opportunity to provide many details left out in the previous paper on UPPAAL TIGA [13]. Furthermore, we formalized a generalization of conventional inclusion checking for the EADG framework. The resulting vertex merging technique can be used to remove vertices that can be derived from other vertices, which is especially useful when the derivation is cheaper than the computation of the value function of the removed vertex. Other domains where we foresee vertex merging being useful include model checking for Petri nets where one marking can cover other markings with less behavior. The vertex merging also allowed us to easily show that we can better exploit the symbolic representation of states using an expansion abstraction. In essence, our abstraction simplifies our symbolic states to discrete locations and their invariants. Hence, all valuations satisfying the given property in the location are propagated backward through the dependency graph, instead of restricting it to valuations that the exploration currently considers reachable. Thus, this abstraction makes the algorithm slightly closer to a traditional backward algorithm.

Our implementation and experiments showed that inclusion checking improves the performance of the naive encoding, while the expansion abstraction outperforms it by almost an additional order of magnitude. We also found that our algorithm is comparable to state-of-the-art UPPAAL TIGA when both use inclusion checking. By integrating our expansion abstraction in TIGA we also improved its performance by almost an order of magnitude. The algorithms presented in this paper will be made available in an upcoming release of UPPAAL.
25:18 On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

References

1 R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In *Fifth Annual IEEE Symposium on Logic in Computer Science*, pages 414–425, 1990. doi:10.1109/LICS.1990.113766.

2 R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. *Information and Computation*, 104(1):2–34, 1993. doi:10.1006/inco.1993.1024.

3 Rajeev Alur. Timed automata. In Nicolas Halbwachs and Doron Peled, editors, *Computer Aided Verification*, volume 1633 of LNCS, pages 8–22, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. doi:10.1007/3-540-48683-6_3.

4 Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. *J. ACM*, 49(5):672–713, September 2002. doi:10.1145/585265.585270.

5 Hugh Anderson and P.S. Thiagarajan. Verification of real-time systems. Course material for CS5270 at NUS Computing, chapter 6, 2007.

6 Ruwaifa Anwar, Haseeb Niaz, David R. Choffnes, Ítalo F. S. Cunha, Phillipa Gill, and Ethan Katz-Bassett. Investigating interdomain routing policies in the wild. *Proceedings of the 2015 Internet Measurement Conference*, 2015. doi:10.1145/2815675.2815712.

7 Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. *IFAC Proceedings Volumes*, 31(18):447–452, 1998. 5th IFAC Conference on System Structure and Control 1998 (SSC’98), Nantes, France, 8-10 July. doi:10.1016/S1474-6670(17)42032-5.

8 Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, and Kim G. Larsen. Static guard analysis in timed automata verification. In Hubert Garavel and John Hatcliff, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, volume 2619 of LNCS, pages 254–270, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. doi:10.1007/3-540-36577-X_18.

9 Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Uppaal-tiga: Time for playing games! In Werner Damm and Holger Hermanns, editors, *Computer Aided Verification*, LNCS, pages 121–125, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-7.

10 Johan Bengtsson and Wang Yi. *Timed Automata: Semantics, Algorithms and Tools*, pages 87–124. LNCS. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. doi:10.1007/978-3-540-27755-2_3.

11 Piotr Berman and Juan A. Garay. Cloture votes:n/4-resilient distributed consensus int + 1 rounds. *Mathematical systems theory*, 26(1):3–19, January 1993. doi:10.1007/BF01187072.

12 Falke B. Ø. Carlsen, Lars Bo P. Frydenskov, Nicolaj Ø. Jensen, Jener Rasmussen, Mathias M. Sørensen, Asger G. Weirsøe, Mathias C. Jensen, and Kim G. Larsen. Cgaal: Distributed on-the-fly ATL model checker with heuristics. *Electronic Proceedings in Theoretical Computer Science*, 390:99–114, September 2023. doi:10.4204/eptcs.390.7.

13 Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, editors, *CONCUR 2005 — Concurrency Theory*, volume 3653 of LNCS, pages 66–80, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. doi:10.1007/11539452_9.

14 Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. *Handbook of Model Checking*. Springer Publishing Company, Incorporated, 1st edition, 2018. doi:10.1007/978-3-319-10575-8.

15 Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Symbolic algorithms for infinite-state games. In Kim G. Larsen and Mogens Nielsen, editors, *CONCUR 2001 — Concurrency Theory*, LNCS, pages 536–550, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. doi:10.1007/3-540-44685-0_36.

16 Anne Edmundson, Roya Ensafi, Nick Feamster, and Jennifer Rexford. Nation-state hegemony in internet routing. *Proceedings of the 1st ACM SIGCAS Conference on Computing and Sustainable Societies*, 2018. doi:10.1145/3209811.3211887.
17 S. Enevoldsen, K.G. Larsen, and J. Srba. Abstract dependency graphs and their application to model checking. In *Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)*, volume 11427 of LNCS, pages 316-333. Springer-Verlag, 2019. doi:10.1007/978-3-030-17462-0_18.

18 Søren Enevoldsen, Kim Guldstrand Larsen, and Jiří Srba. Extended abstract dependency graphs. *International Journal on Software Tools for Technology Transfer*, 24(1):49-65, February 2022. doi:10.1007/s10009-021-00638-8.

19 M. Hendriks, Wang Yi, P. Petterson, J. Hakansson, K.G. Larsen, A. David, G. Behrmann, M. Hendriks, Wang Yi, P. Petterson, J. Hakansson, K.G. Larsen, A. David, and G. Behrmann. Uppaal 4.0. In *Third International Conference on the Quantitative Evaluation of Systems - (QEST'06)*, pages 125-126, 2006. doi:10.1109/QEST.2006.59.

20 Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiří Srba, and Lars Kaerlund Oestergaard. Efficient model-checking of weighted CTL with upper-bound constraints. *International Journal on Software Tools for Technology Transfer*, 18(4):409-426, August 2016. doi:10.1007/s10009-014-0359-5.

21 Nicolaj Ø. Jensen, Peter G. Jensen, and Kim G. Larsen. Dynamic extrapolation in extended timed automata. In Yi Li and Sofiène Tahar, editors, *Formal Methods and Software Engineering*, LNCS, pages 83-99, Singapore, 2023. Springer Nature Singapore. doi:10.1007/978-981-99-7584-6_6.

22 Nicolaj Ø. Jensen, Kim G. Larsen, and Jiří Srba. Token elimination in model checking of petri nets. In *Tools and Algorithms for the Construction and Analysis of Systems*, LNCS, 2025. doi:10.1007/978-3-031-90643-5_11.

23 Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiri Srba. On-the-fly symbolic algorithm for timed atl with abstractions reproducibility package, April 2025. doi:10.5281/zenodo.15195408.

24 Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiří Srba, and Nikolaj Jensen Ulrik. Elimination of detached regions in dependency graph verification. In Georgiana Caltais and Christian Schilling, editors, *Model Checking Software*, LNCS, pages 163-179, Cham, 2023. Springer Nature Switzerland. doi:10.1007/978-3-031-32157-3_9.

25 Xinxin Liu and Scott A. Smolka. Simple linear-time algorithms for minimal fixed points. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, *Automata, Languages and Programming*, pages 53-66, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. doi:10.1007/BFb0055040.

26 Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems. In Ernst W. Mayr and Claude Puech, editors, *STACS 95*, LNCS, pages 229-242, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. doi:10.1007/3-540-59042-0_76.

27 Mark (Mohammad) Tehranipoor, Ujjwal Guin, and Domenic Forte. *Counterfeit Integrated Circuits*, pages 15-36. Springer International Publishing, Cham, 2015. doi:10.1007/978-3-319-11824-6_2.