# CTL Model Checking of Concurrent Self Modifying Code*

Tayssir Touili

touili@irif.fr

IRIF, CNRS, and University Paris Cité

Paris, France

## Abstract

Analysing programs without actually executing them is crucial for binary analysis but poses many challenges especially if we consider programs with the ability to spawn parallel processes (concurrency) and to modify their own instructions (self-modification). Modern malware uses this complexity to obfuscate the virus programs and make them hard to analyse. This paper proposes an efficient model checking approach for handling such type of programs. A natural abstraction of concurrent and self-modifying programs is Self-Modifying Dynamic Pushdown Network (SM-DPN). It is a set of Pushdown Systems, each with the ability to spawn new processes and modify its own set of rules. We consider single indexed CTL model checking of these processes. A single indexed CTL formula represents a conjunction of CTL formulas, each corresponding to a single process. The problem is not trivial because a process may or may not be spawned, which affects the result. Our approach is to construct finite automata that accept process configurations satisfying the corresponding formula. Then, we iteratively exclude configurations that spawn violating processes. We implemented the algorithm and conducted practical experiments showing promising results. In particular, our tool was able to detect several self-modifying concurrent malware.

## CCS Concepts

* **Theory of computation** → Verification by model checking; Modal and temporal logics.

## Keywords

CTL model checking, pushdown automata

## ACM Reference Format:

Tayssir Touili and Olzhas Zhangeldinov. 2026. CTL Model Checking of Concurrent Self Modifying Code. In *The 41st ACM/SIGAPP Symposium on Applied Computing (SAC '26), March 23–27, 2026, Thessaloniki, Greece*. ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3748522.3779956

## 1 Introduction

A lot of modern programs employ concurrency for executing several tasks in parallel. However, programs with parallel processes are known to be error-prone and hard to analyse. Several approaches have been proposed for the analysis of concurrent programs [19, 38, 3, 16, 24, 34, 25].

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

This work is licensed under a Creative Commons Attribution 4.0 International License. SAC '26, Thessaloniki, Greece

© 2026 Copyright held by the owner/authors.

ACM ISBN 978-8-4007-2294-3/2026/03

https://doi.org/10.1145/3748522.3779956

Olzhas Zhangeldinov

zhangeldinov@irif.fr

IRIF, CNRS, and University Paris Cité

Paris, France

<table><caption>Listing 1: Example of self-modifying and concurrent code.</caption><thead><tr><th># Address</th><th>Bytecode</th><th>Assembly</th></tr></thead><tbody><tr><td>0x10</td><td>6a10</td><td>push 0x10</td></tr><tr><td>0x12</td><td>50</td><td>push eax</td></tr><tr><td>0x13</td><td>53</td><td>push ebx</td></tr><tr><td>0x14</td><td>ff1500000000</td><td>call [CreateThread]</td></tr><tr><td>0x1a</td><td>c6051100000026</td><td>mov [0x11], 0x26</td></tr><tr><td>0x21</td><td>ebed</td><td>jmp 0x10</td></tr><tr><td>0x26</td><td>ff1501000000</td><td>call [InternetOpenA]</td></tr></tbody></table>

<table><caption>Listing 2: Example of self-modifying and concurrent code after self-modification.</caption><thead><tr><th># Address</th><th>Assembly</th></tr></thead><tbody><tr><td>0x10</td><td>push 0x10</td><td>#-- executing</td><td>--&gt; push 0x26</td></tr><tr><td></td><td></td><td># mov [0x11], 0x26</td><td></td></tr><tr><td>0x12</td><td>push eax</td><td></td><td></td></tr><tr><td>0x13</td><td>push ebx</td><td></td><td></td></tr><tr><td>0x14</td><td>call [CreateThread]</td><td></td><td></td></tr><tr><td>0x1a</td><td>mov [0x11], 0x26</td><td></td><td></td></tr><tr><td>0x21</td><td>jmp 0x10</td><td></td><td></td></tr><tr><td>0x26</td><td>call [InternetOpenA]</td><td></td><td></td></tr></tbody></table>

On the other hand, sometimes one does not have access to the source code of the program they want to analyse. This is often the case when we want to analyse malware or proprietary software. Therefore, it is important to be able to analyse binary programs.

However, several binary programs modify their instructions in real time to obfuscate some parts of their code, making it harder to analyse. Such code is called self-modifying. This technique is often used by developers of malware because self-modifying programs can hide their fingerprints from static virus detections such as hex search. Several approaches have been proposed to analyse self-modifying code [10, 35, 7, 25].

In this work, we consider the analysis of self-modifying and concurrent binary code, which can be encountered in malware. Let us show an example of a code that is both self-modifying and concurrent in Listing 1. The first column shows the addresses of the code, the second column displays the bytecodes stored at each address, and the third column contains the assembly instructions corresponding to the bytecodes. The code is supposed to run on a x86 architecture under the Windows operating system.

The execution of the code starts at address **0x10**, which contains bytes **6a10** corresponding to the assembly instruction **push 0x10**. This instruction pushes value **0x10** onto the stack. Next, the program executes byte **50** at the address **0x12**. The assembly code for this byte is **push eax**, which pushes the value of the register **eax** onto the stack. Next, the address **0x13** contains the byte **53**, which corresponds to the assembly instruction **push ebx**. This instruction pushes the values of the register **ebx** onto the stack. Then, the program executes the bytecode **ff1500000000** at the address **0x14**,

<footnote>*This work was partially funded by the french ANR grant Defmal “ANR-22-PECY-0007”</footnote>
which corresponds to the instruction **call [CreateThread]**. This instruction calls the Windows API function *CreateThread*, which creates a new thread running in parallel. The start address of the new thread is defined by the third value on the stack. Since the third value on the stack is **0x10**, the thread will start with the **push 0x10** instruction. Then, the program will execute the bytecode `c6051100000026` located at the address **0x1a** and corresponding to instruction **mov [0x11], 0x26**. It replaces the content stored at address **0x11** with **0x26**. Thus, the **mov** instruction will replace bytecode **6a10** stored at address **0x10** with **6a26**. The bytecode **6a26** corresponds to assembly instruction **push 0x26**. Therefore, instruction **push 0x10** at address **0x10** will be replaced with instruction **push 0x26**. Hence, **mov [0x11], 0x26** is a self-modifying instruction that replaces instruction **push 0x10** with **push 0x26**. Then, the next address **0x21** contains the bytecode **ebed**, which corresponds to the assembly instruction **jmp 0x10**. This instruction jumps to the location **0x10** to execute the next instruction. Note that the instruction at **0x10** was modified by the **mov** instruction. The program will execute the modified instruction **push 0x26**, which pushes **0x26** onto the stack. The code of the program after the self-modification is presented in Listing 2. Then, the program will execute instructions **push eax**, **push ebx**, and **call [CreateThread]**. This time, the third value on the stack is **0x26** pushed by the modified instruction. Therefore, the *CreateThread* function will spawn a new thread starting at the address **0x26**. This address contains the bytecode `ff1501000000`, which corresponds to the instruction **call [InternetOpenA]**. This instruction calls the Windows API function *InternetOpenA*, which allows the program to access the internet. Discovery of the call to the *InternetOpenA* function is possible only if the analysis considers the self-modifying instruction **mov [0x11], 0x26** and the concurrent instruction **call [CreateThread]**. Therefore, it is important to be able to analyse *self-modifying* and *concurrent* programs.

Model checking has been proposed to analyse concurrent and self-modifying code by [25, 37]. However, these works only consider reachability analysis and LTL model checking of such programs. In this work, we go one step further and consider CTL model checking of this class of binaries. Indeed, several malicious behaviours can be described by CTL formulas and not by LTL [32].

First, to perform model checking of binary programs, one needs a good abstraction of the binary code. It is well known that Pushdown Systems (PDS) is an adequate model for sequential programs because PDS can accurately model the execution stack [33, 32, 13]. To model concurrent systems with dynamic thread creation, Dynamic Pushdown Networks (DPNs) were introduced [9]. A DPN can be seen as a set of PDSs, such that each PDS corresponds to some parallel process that can spawn other parallel processes. On the other hand, to consider self-modification, [35] introduced Self-Modifying Pushdown Systems (SM-PDS), which are PDSs with the ability to change their rules at runtime. Later, [25] introduced Self-Modifying Dynamic Pushdown Networks (SM-DPNs) to model programs that are both concurrent and self-modifying, and they proposed an efficient algorithm for reachability analysis. SM-DPNs are similar to DPNs, but each process is modelled by a *self-modifying* Pushdown System instead of standard PDS. Then, [37] proposed LTL model checking of SM-DPNs.

In this work, we adopt this SM-DPN model to describe self-modifying concurrent programs. We go one step further and consider the CTL model checking problem of SM-DPNs. Unfortunately, this problem is undecidable if we consider unrestricted CTL formulas over parallel processes [29]. Therefore, we consider single-indexed CTL formulas. If a program can spawn *n* parallel processes, a single-indexed CTL formula *f* is a conjunction of *n* CTL formulas: $f = \bigwedge_{i=1}^n f_i$, where each CTL formula $f_i$ reasons about a single process *i*. Indeed, model checking against double-indexed formulas even for two processes is undecidable [18].

Model checking non self-modifying DPNs against single indexed CTL formulas was studied previously in [34], where an efficient CTL model checking algorithm was proposed. Since an SM-DPN can be translated into an equivalent DPN [25], one can think of applying a naive approach that consists in translating the SM-DPN into an equivalent DPN, and then model checking the equivalent DPN using the existing method. However, this approach is not efficient as will be shown in Section 4. Therefore, we propose a *direct* and *efficient* algorithm to model check SM-DPNs against single-indexed CTL formulas.

Since SM-DPNs allow processes to spawn other threads, it is not trivial to only model check each initial process $P_i$ against its CTL formula $f_i$ because, firstly, the process might spawn another process that violates the formula. In this case, we also need to model check the spawned process as well. Second, model checking every possibly spawned process is too restrictive because some processes that violate the formula might not be spawned. We tackle this problem by reducing the CTL model checking for each separate process $P_i$ over a CTL formula $f_i$ to the emptiness problem on a finite state automaton $A_i$ that keeps track of spawned processes. Then, we compute the largest set of spawned processes $D_{fp}$, s.t. every process $P_j$ in $D_{fp}$ satisfies $f_j$ and spawns only processes in $D_{fp}$.

We implemented our algorithm and compared its performance against the naive approach that necessitates the translation of the SM-DPN model into a standard DPN. Our approach demonstrated significant improvement in the performance. The implemented algorithm was incorporated into a tool for the analysis of concurrent self-modifying binary code. This tool translates a concurrent self-modifying binary program into an SM-DPN model and performs model checking against a given single-indexed CTL formula. We obtained encouraging results. In particular, our tool was able to detect several concurrent and self-modifying malwares.

*Related Work.* Previous studies [32, 5, 41, 21] developed different approaches for model checking binary programs. [32] consists in modelling programs as Pushdown Systems (PDS). Model checking programs using PDS was well studied using reachability analysis [8], LTL model checking [33, 14, 17, 13], and CTL model checking [15, 32, 39]. However, standard PDS do not consider concurrency and self-modification.

Model checking concurrent programs using networks of PDS was proposed in [18, 20, 28, 27]. However, these PDS models cannot represent process creation. Dynamic Pushdown Network (DPN) model that allows spawning processes was studied in [9, 23, 34, 26, 22]. However, these works do not consider self-modifying behaviours.
On the other hand, dealing with self modifying programs is a difficult task. Some studies proposed abstractions to model such programs [10, 11, 7] but these works do not provide an automatic approach for model checking. Other research [6, 2] provided static analysis techniques applicable to self-modifying code. However, the models provided are too abstract and the stack of the program is ignored. [35, 36] provided LTL and CTL model checking algorithms for SM-PDS, which can be directly obtained from binary code. However, the SM-PDS model does not consider parallel processes.

As far as we know, the only works that consider model checking of concurrent self-modifying programs are [25, 37]. However, these works only consider reachability and LTL model checking of such programs. In this work, we go one step further and consider the CTL model checking problem of concurrent self-modifying programs.

*Outline.* This paper is structured as follows. Section 2 introduces the reader to the core concepts used throughout the paper, such as Self-Modifying Dynamic Pushdown Networks and single-indexed CTL formulas. Section 3 describes our contribution - the efficient algorithm for CTL model checking SM-DPNs. Section 4 presents the results of our practical experiments.

# 2 Preliminaries

## 2.1 Self-Modifying Dynamic Pushdown Network

A Self-Modifying Dynamic Pushdown Network (SM-DPN) is a set of sequential Self-Modifying Dynamic Pushdown Systems (SM-DPDSs), where each SM-DPDS corresponds to a parallel process, can modify its own set of transition rules, and can spawn processes.

**Definition 2.1.** A Self-Modifying Dynamic Pushdown Network (SM-DPN) is a tuple $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$, where for $i, 1 \le i \le n$, $\mathcal{P}_i$ is a Self-Modifying Dynamic Pushdown System (SM-DPDS) $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$, such that $P_i$ is a finite set of control locations ($P_j$ and $P_i$ are disjoint for any $j \neq i$), $\Gamma_i$ is the stack alphabet, $\Delta_i$ is a finite set of rules of the forms: (1) $p\gamma \hookrightarrow p_1\omega_1$ and (2) $p\gamma \hookrightarrow p_1\omega_1\triangleright p_2\omega_2\theta_2$, where $p, p_1 \in P_i$, $\gamma \in \Gamma_i$, $\omega_1 \in \Gamma_i^*$, $p_2 \in P_j$, $\omega_2 \in \Gamma_j^*$, $\theta_2 \subseteq \Delta_j \cup \Delta_j^c$ for some $1 \le j \le n$; and $\Delta_i^c$ is a finite set of self-modifying rules of the form $p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p_1$, where $\rho_1, \rho_2 \subseteq \Delta_i \cup \Delta_i^c$. A Dynamic Pushdown System (DPDS) is an SM-DPDS, such that $\Delta_i^c = \emptyset$. A Dynamic Pushdown Network (DPN) is an SM-DPN $\mathcal{M}' = (\mathcal{P}'_1, \mathcal{P}'_2, \dots, \mathcal{P}'_m)$, such that for every $1 \le i \le m$, $\mathcal{P}'_i$ is a DPDS.

Let us consider an SM-DPN $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$, where for $1 \le i \le n$, $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ is an SM-DPDS. The idea behind self-modifying behaviour is that only some of the rules from $\Delta_i$ and $\Delta_i^c$ are present at a given time. We call the current set of these rules a *phase* $\theta \subseteq \Delta_i \cup \Delta_i^c$. The phase changes during the execution using self-modifying rules from $\Delta_i^c$. When an SM-DPDS executes a self-modifying rule of the form $p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p_1$ in the current phase $\theta$, it moves from control location $p$ to control location $p_1$, removes from $\theta$ every rule contained in $\rho_1$, and then adds all rules from $\rho_2$ to $\theta$. A standard rule of the form $p\gamma \hookrightarrow p_1\omega_1 \in \theta$ moves the SM-DPDS from control location $p$ to control location $p_1$, pops $\gamma$ from the top of the current stack, and pushes word $\omega_1$ onto the stack. A spawning rule of the form $p\gamma \hookrightarrow p_1\omega_1 \triangleright p_2\omega_2\theta_2 \in \theta$ moves the SM-DPDS from $p$ to $p_1$, pops $\gamma$ from the stack, pushes $\omega_1$, and

also spawns a process starting from control location $p_2$, having $\omega_2$ as its stack content, and $\theta_2$ as the current phase.

## 2.2 Configurations and DCLICs

The current state of an SM-DPDS is called a *local configuration*. Consider an SM-DPN $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$. Given $1 \le i \le n$ and an SM-DPDS $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$, the local configuration $c$ of $\mathcal{P}_i$ is a tuple $((p, \omega), \theta)$, where $p \in P_i$ is its current control location, $\omega \in \Gamma_i^*$ is its current stack content, and $\theta \subseteq \Delta_i \cup \Delta_i^c$ is its current phase. Let $\text{Conf}_i$ be the set of all local configurations of $\mathcal{P}_i$. A global configuration $\mathcal{G}$ of $\mathcal{M}$ is a multi-set over $\bigcup_{i=1}^n \text{Conf}_i$.

If some SM-DPDS spawns a process at control location $p'$, stack contents $\omega'$, and phase $\theta'$, then $p'\omega'\theta'$ is a *Dynamically Created Local Initial Configuration* (DCLIC). Let $\mathcal{D}_i$ be the set of all DCLICs spawned by $\mathcal{P}_i$: $\mathcal{D}_i = \{p'\omega'\theta' \in P_j \times \Gamma_j^* \times 2^{\Delta_j \cup \Delta_j^*} | \exists p, p_1 \in P_i, \gamma \in \Gamma_i, \omega_1 \in \Gamma_i^* \text{, } p\gamma \hookrightarrow p_1\omega_1 \triangleright p'\omega'\theta' \in \Delta_i\}$.

For two local configurations $((p, \omega), \theta), ((p', \omega'), \theta') \in \text{Conf}_i$ of $\mathcal{P}_i$ and a set of DCLICs $D \subseteq \mathcal{D}_i$, the *successor relation* $((\langle p, \omega \rangle, \theta) \stackrel{D}{\Rightarrow} i$) $((\langle p', \omega' \rangle, \theta')$ holds in three cases:

(1) $\exists p\gamma \hookrightarrow p'v \in \theta$, where $\gamma \in \Gamma_i$, $u, v \in \Gamma_i^*$, s.t. $\omega = \gamma u, \omega' = vu, \theta = \theta'$, and $D = \emptyset$; or

(2) $\exists p\gamma \hookrightarrow p'v \triangleright p_2\omega_2\theta_2 \in \theta$, where $\gamma \in \Gamma_i$, $u, v \in \Gamma_i^*$, s.t. $\omega = \gamma u, \omega' = vu, \theta = \theta'$, and $D = \{p_2\omega_2\theta_2\}$; or

(3) $\exists p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p' \in \theta$, where $\rho_1, \rho_2 \subseteq \Delta_i \cup \Delta_i^c$, s.t. $\rho_1 \subseteq \theta, \omega = \omega'$, $D = \emptyset$, and $\theta' = (\theta \setminus \rho_1) \cup \rho_2$.

Intuitively, $((\langle p, \omega \rangle, \theta) \stackrel{D}{\Rightarrow} i$) $((\langle p', \omega' \rangle, \theta')$ if there is a rule in $\theta$ that changes the current state of $\mathcal{P}_i$ from $((\langle p, \omega \rangle, \theta) \text{ into } ((\langle p', \omega' \rangle, \theta')$ and spawns $D$. Case (1) defines successors obtained by applying standard pushdown rules. For example, if the current local configuration is $((\langle p, \gamma u \rangle, \theta),$ then, if we apply a rule $p\gamma \hookrightarrow p'v$, we will obtain the local configuration $((\langle p', vu \rangle, \theta)$ and $D = \emptyset$ because the rule does not spawn any process. According to case (2), if we apply a rule of the form $p\gamma \hookrightarrow p'v \triangleright p_2\omega_2\theta_2$, then we obtain $((\langle p', vu \rangle, \theta)$ and $D = \{p_2\omega_2\theta_2\}$ is the spawned process. Case (3) defines the self-modifying behaviour of a rule $p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p'$ that changes the current control location $p$ to the control location $p'$, removes from $\theta$ every rule of $\rho_1$ and adds every rule from $\rho_2$ to $\theta$, resulting in $((\langle p', \gamma u \rangle, (\theta \setminus \rho_1) \cup \rho_2)$.

A *local run* $\eta$ of a SM-DPDS $\mathcal{P}_i$ is a sequence of local configurations $\eta = c_0 c_1 c_2 \dots$, s.t. $\forall j \ge 0 : c_j \in \text{Conf}_i$ and $\exists D \subseteq \mathcal{D}_i : c_j \stackrel{D}{\Rightarrow} i$ $c_{j+1}$. An *execution tree* is a tree whose nodes are labelled by local configurations, and such that each branch is a local run.

From now on, we fix an SM-DPN $\mathcal{M} = (\mathcal{P}_1, \dots, \mathcal{P}_n)$, where for $1 \le i \le n$, $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ is an SM-DPDS. Let $\wp$ be a function that maps each control location to its corresponding process, i.e. for any $j, 1 \le j \le n, \wp(p) = j$ if $p \in P_j$.

## 2.3 CTL formulas

Without loss of generality, we assume that CTL formulas are given in their positive-normal forms. We use the *release operator* $\mathbf{R}$ as the dual form of the *until operator* $\mathbf{U}$. Let $\mathbf{AP}$ be a set of atomic propositions. Let $a \in \mathbf{AP}$. Then:
**Definition 2.2.** A CTL formula $\psi$ is defined as follows:

$$ \psi ::= \text{True} \mid \text{False} \mid a \mid \neg a \mid \psi \land \psi \mid \psi \lor \psi \mid \mathbf{AX}\psi \mid \mathbf{EX}\psi \mid \mathbf{A}[\psi\mathbf{U}\psi] \mid \mathbf{E}[\psi\mathbf{U}\psi] \mid \mathbf{A}[\psi\mathbf{R}\psi] \mid \mathbf{E}[\psi\mathbf{R}\psi] $$

A single-indexed CTL formula $f$ is a conjunction $f = \bigwedge_{i=1}^n f_i$, where $f_i$ is a CTL formula on $\mathcal{P}_i$, i.e. whose atomic propositions $AP_i$ depend only on the SM-DPDS $\mathcal{P}_i$.

Let $f = \bigwedge_{i=1}^n f_i$ be a single-indexed CTL formula on $\mathcal{M}$, where for $1 \le i \le n$, $f_i$ is a CTL formula on $\mathcal{P}_i$ with a corresponding set of atomic propositions $AP_i$. Consider a valuation function $v_i: AP_i \to 2^{\mathcal{P}_i}$ that assigns a set of control locations to every atomic proposition. Let $c = (\langle p, \omega \rangle, \theta) \in \mathcal{G}$ be a local configuration of $\mathcal{P}_i$. For some $D \subseteq \mathcal{D}_i$, we define the satisfaction relation $\models_D$. Intuitively, $c \models_D f_i$ iff there is an execution tree starting from $c$ that satisfies $f_i$ and spawns $D$, i.e. $D$ is a collection of DCLICs $p_2\omega_2\theta_2$ obtained from the rules of the form $p\gamma \to p'\omega \triangleright p_2\omega_2\theta_2$ applied to construct the execution tree. $\models_D$ is defined as follows:

(1) $c \models_\emptyset a$, where $a \in AP_i$, if $p \in v_i(a)$;

(2) $c \models_\emptyset \neg a$, where $a \in AP_i$, if $p \notin v_i(a)$;

(3) $c \models_D \psi_1 \land \psi_2$ if $\exists D_1, D_2 \subseteq \mathcal{D}_i$, s.t. $D = D_1 \cup D_2$, $c \models_{D_1} \psi_1$ and $c \models_{D_2} \psi_2$;

(4) $c \models_D \psi_1 \lor \psi_2$ if $c \models_D \psi_1$ or $c \models_D \psi_2$;

(5) $c \models_D \mathbf{AX}\psi_1$: if $c$ has successors $c_1, \dots, c_m \in Conf_i$, where for each $j$, $1 \le j \le m$, $\exists D_j \subseteq \mathcal{D}_i$, $c \stackrel{D_j}{\rightleftharpoons} c_j$, then $c \models_D \mathbf{AX}\psi_1$ if for each $1 \le j \le m$, $\exists D'_j \subseteq \mathcal{D}_i$, $c_j \models_{D'_j} \psi_1$, and $D = \bigcup_{j=1}^m (D_j \cup D'_j)$;

(6) $c \models_D \mathbf{EX}\psi_1$ if there exist $c' \in Conf_i$ and $D', D'' \subseteq \mathcal{D}_i$, s.t. $c \stackrel{D'}{\rightleftharpoons} c'$, $c' \models_{D''} \psi_1$, and $D = D' \cup D''$;

(7) $c \models_D \mathbf{A}[\psi_1\mathbf{U}\psi_2]$; for all local runs $\eta = c_0c_1\dots$, s.t. $c_0 = c$ (for $j \ge 1$, let $D_j \subseteq \mathcal{D}_i$, s.t. $c_{j-1} \stackrel{D_j}{\rightleftharpoons} c_j$), $c \models_D \mathbf{A}[\psi_1\mathbf{U}\psi_2]$ if $\exists k \ge 0$, s.t. $\exists D'_k \subseteq \mathcal{D}_i$, $c_k \models_{D'_k} \psi_2$, and $\forall l, 0 \le l < k$, $\exists D'_l \subseteq \mathcal{D}_i$, $c_l \models_{D'_l} \psi_1$, and $D = \bigcup_{l=1}^k D_l \cup \bigcup_{l=0}^k D'_l$;

(8) $c \models_D \mathbf{E}[\psi_1\mathbf{U}\psi_2]$ if there exists a local run $\eta = c_0c_1\dots$, s.t. $c_0 = c$ (for $j \ge 1$, let $D_j \subseteq \mathcal{D}_i$, s.t. $c_{j-1} \stackrel{D_j}{\rightleftharpoons} c_j$), and $\exists k \ge 0$, s.t. $\exists D'_k \subseteq \mathcal{D}_i$, $c_k \models_{D'_k} \psi_2$ and $\forall l, 0 \le l < k$, $\exists D'_l \subseteq \mathcal{D}_i$, $c_l \models_{D'_l} \psi_1$, and $D = \bigcup_{l=1}^k D_l \cup \bigcup_{l=0}^k D'_l$;

(9) $c \models_D \mathbf{A}[\psi_1\mathbf{R}\psi_2]$; for all local runs $\eta = c_0c_1\dots$, s.t. $c_0 = c$ (for $j \ge 1$, let $D_j \subseteq \mathcal{D}_i$, s.t. $c_{j-1} \stackrel{D_j}{\rightleftharpoons} c_j$), and if (1) $\forall l \ge 0$, $\exists D'_l \subseteq \mathcal{D}_i$, $c_l \models_{D'_l} \psi_2$, then let $D_\eta = \bigcup_{l \ge 1} D_l \cup \bigcup_{l \ge 0} D'_l$, or if (2) $\exists k \ge 0$, $\exists D''_k \subseteq \mathcal{D}_i$, s.t. $c_k \models_{D''_k} \psi_1$ and $\forall l, 0 \le l \le k$, $\exists D'_l \subseteq \mathcal{D}_i$, $c_l \models_{D'_l} \psi_2$ then let $D_\eta = \bigcup_{l=1}^k D_l \cup D''_k \cup \bigcup_{l=0}^k D'_l$. $c \models_D \mathbf{A}[\psi_1\mathbf{R}\psi_2]$ if one of the conditions above hold for every path $\eta$ and $D = \bigcup_\eta D_\eta$;

(10) $c \models_D \mathbf{E}[\psi_1\mathbf{R}\psi_2]$ if there exists a local run $\eta = c_0c_1\dots$, s.t. $c_0 = c$ (for $j \ge 1$, let $D_j \subseteq \mathcal{D}_i$, s.t. $c_{j-1} \stackrel{D_j}{\rightleftharpoons} c_j$), and either (1) $\forall l \ge 0$, $\exists D'_l \subseteq \mathcal{D}_i$, $c_l \models_{D'_l} \psi_2$, and $D = \bigcup_{l \ge 1} D_l \cup \bigcup_{l \ge 0} D'_l$, or (2) $\exists k \ge 0$, $\exists D''_k \subseteq \mathcal{D}_i$, s.t. $c_k \models_{D''_k} \psi_1$ and $\forall l, 0 \le l \le k$, $\exists D'_l \subseteq \mathcal{D}_i$, $c_l \models_{D'_l} \psi_2$ and $D = \bigcup_{l=1}^k D_l \cup D''_k \cup \bigcup_{l=0}^k D'_l$;

Additional eventually and globally CTL operators are defined as follows: $\mathbf{EF}\psi = \mathbf{E}[\text{TrueU}\psi]$, $\mathbf{AF}\psi = \mathbf{A}[\text{TrueU}\psi]$, $\mathbf{EG}\psi = \mathbf{E}[\text{FalseR}\psi]$, $\mathbf{AG}\psi = \mathbf{A}[\text{FalseR}\psi]$.

**Definition 2.3.** We say that a global configuration $\mathcal{G}$ satisfies $f$, i.e. $\mathcal{G} \models f$, if for every local configuration $c = (\langle p, \omega \rangle, \theta) \in \mathcal{G}$, there exists $D \in \mathcal{D}_{\varphi(p)}$, such that $c \models_D f_i$ and for every $p'\omega'\theta' \in D$, $(\langle p', \omega' \rangle, \theta') \models f$.

# 3 Single-Indexed CTL Model Checking of SM-DPNs

This section presents our main contribution - a direct algorithm for single-indexed CTL model checking SM-DPNs. To effectively model check SM-DPNs over single-indexed CTL formulas, we follow the approach of [34] and extend it to self-modifying DPNs. We split the model checking algorithm into the following steps:

(1) We reduce the problem of model checking $\mathcal{P}_i$ against $f_i$ to the emptiness problem of a corresponding Self-Modifying Alternating Büchi Dynamic Pushdown System (SM-ABDPDS) $\mathcal{B}\mathcal{P}_i$. $\mathcal{B}\mathcal{P}_i$ corresponds to a kind of product between the CTL formula $f_i$ and the SM-DPDS $\mathcal{P}_i$, such that a configuration $c$ of $\mathcal{P}_i$ satisfies $f_i$ over DCLICs $D$, i.e. $c \models_D f_i$, if there is an accepting run in $\mathcal{B}\mathcal{P}_i$ starting from $c$ and spawning $D$.

(2) Then, to find accepting runs of $\mathcal{B}\mathcal{P}_i$, we perform a kind of reachability analysis to compute the set $Y_{\mathcal{B}\mathcal{P}_i}$ that contains pairs of the form $(c, D)$, where $c$ is a configuration of $\mathcal{B}\mathcal{P}_i$ from which there is an accepting run spawning $D \subseteq D_i$.

(3) To finitely represent possibly infinite sets of configurations, we use a kind of finite alternating automaton $\mathcal{A}_i$ to compute $Y_{\mathcal{B}\mathcal{P}_i}$.

(4) Then, we use the obtained automata $\mathcal{A}_i$ for each $i$, $1 \le i \le n$ to find the maximal set of DCLICs $\mathcal{D}_{fp}$ containing only DCLICs $p\omega\theta$ that satisfy $f$, i.e., s.t. $(\langle p, \omega \rangle, \theta) \models f$. And thus, for a global configuration $\mathcal{G}$, to check whether $\mathcal{G} \models f$, we need to check that for every local configuration $(\langle p, \omega \rangle, \theta) \in \mathcal{G}$ there is a set of DCLICs $D \subseteq \mathcal{D}_{fp}$, such that $\mathcal{A}_{\varphi(p)}$ accepts $((\langle p, \omega \rangle, \theta), D)$.

The following sections describe these different steps in details.

## 3.1 Self-Modifying Alternating Büchi Dynamic Pushdown Systems

Since CTL formulas can be represented by alternating Büchi automata [38], to compute a kind of product between the SM-DPDS and the CTL formula, we introduce Self-Modifying Alternating Büchi Dynamic Pushdown Systems (SM-ABDPDS). It is a kind of SM-DPDS with alternating transitions (since CTL is branching-time) and Büchi accepting control locations. Since the current phase of the computed SM-ABDPDS should correspond to the phase of the initial SM-DPDS, while defining SM-ABDPDS, we introduce a phase alphabet $\delta_i$ that is independent from the set of rules of the SM-ABDPDS. Instead, it is meant to contain rules of the original SM-DPDS (as will be seen in Section 3.2). Formally:

**Definition 3.1.** A Self-Modifying Alternating Büchi Dynamic Pushdown System (SM-ABDPDS) is a tuple $\mathcal{B}\mathcal{P}_i = (P'_i, \Gamma_i, \Delta'_i, \Delta''_i, F_i, \delta_i)$, where $P'_i$ is a finite set of states, $\Gamma_i$ is the stack alphabet, $F_i \subseteq P'_i$ is the set of accepting states, $\delta_i$ is the phase alphabet, $\Delta'_i$ is the set
of rules of the form $p\gamma \mathrel{\substack{\xrightarrow{[\sigma_1, \dots, \sigma_h]} \\[-0.5ex] \xleftarrow{p_1\omega_1} \{p_1\omega_1, \dots, p_h\omega_h\}}} \{D_1, \dots, D_h\}$, where $p \in P'_i$, $\gamma \in \Gamma_i$, and for every $j$, $1 \le j \le h$, $\sigma_j \subseteq \delta_i$, $p_j \in P'_i$, $\omega_j \in \Gamma_i^*$, $D_j \subseteq D_i$. The set of self-modifying rules $\Delta_i^{c'}$ contains transitions of the form $p \xrightarrow{(\rho_1, \rho_2)} p'$, where $p, p' \in P'_i$, $\rho_1, \rho_2 \subseteq \delta_i$.

Consider an SM-ABDPDS $\mathcal{B}\mathcal{P}_i = (P'_i, \Gamma_i, \Delta_i^{c'}, \hat{F}_i, \delta_i)$. A configuration of $\mathcal{B}\mathcal{P}_i$ is a tuple $c = ((p, \omega), \theta)$, where $p \in P'_i$, $\omega \in \Gamma_i^*$, and $\theta \subseteq \delta_i$. Let $\text{Conf}_{\mathcal{B}\mathcal{P}_i}$ be the set of all configurations of $\mathcal{B}\mathcal{P}_i$. The successor relation $c \mathrel{\substack{\xrightarrow{D} \\[-0.5ex] \xleftarrow{S}}}$ between a configuration $c \in \text{Conf}_{\mathcal{B}\mathcal{P}_i}$ and a set of configurations $S \subseteq \text{Conf}_{\mathcal{B}\mathcal{P}_i}$ over a set of DCLICs $D \subseteq D_i$ means that we can apply a rule from $\Delta_i^c \cup \Delta_i^{c'}$ that changes $c$ into the configurations $S$, and the transition spawns DCLICs $D$. Formally, given $c = ((p, \omega), \theta)$, $c \mathrel{\substack{\xrightarrow{D} \\[-0.5ex] \xleftarrow{S}}}$ is defined as follows:

(1) There exists $p\gamma \mathrel{\substack{\xrightarrow{[\sigma_1, \dots, \sigma_h]} \\[-0.5ex] \xleftarrow{p_1\omega'_1, \dots, p'_h\omega'_h}}} \{D_1, \dots, D_h\} \in \Delta'_i$, such that $\omega = \gamma u$, $S = \{((p'_i, \omega'_i u), \theta) \mid \sigma_j \subseteq \theta\}$, $D = \bigcup_{\sigma_j \subseteq \emptyset} D_j$, and either $\forall 1 \le j \le h$, $\sigma_j = \emptyset$ or $\exists j$, $\sigma_j \subseteq \theta$ and $\sigma_j \neq \emptyset$.

(2) There exists $p \xrightarrow{(\rho_1, \rho_2)} p' \in \Delta_i^{c'}$, such that $S = \{(\langle p', \omega \rangle, \theta')\}$, $D = \emptyset$, $\rho_1 \subseteq \theta$ and $\theta' = (\theta \setminus \rho_1) \cup \rho_2$.

Intuitively, let $c = ((p, \gamma u), \theta)$ be the current configuration of $\mathcal{B}\mathcal{P}_i$ and consider a rule $p\gamma \mathrel{\substack{\xrightarrow{[\sigma_1, \dots, \sigma_h]} \\[-0.5ex] \xleftarrow{p'_1\omega'_1, \dots, p'_h\omega'_h}}} \{D_1, \dots, D_h\} \in \Delta'_i$. For each $j$, $1 \le j \le h$, if $\sigma_j \subseteq \theta$, then $\mathcal{B}\mathcal{P}_i$ transitions into the configuration $((p'_j, \omega'_j u), \theta)$ and spawns DCLICs $D_j$. When this rule is applied, $c$ forks into the set of configurations $\{(\langle p'_k, \omega'_k u \rangle, \theta), \dots, (\langle p'_{km}, \omega'_{km} u \rangle, \theta)\}$, where for $1 \le l \le m$, $\sigma_{kl} \subseteq \theta$. Moreover, the rule spawns DCLICs $D = D_{k_1} \cup \dots \cup D_{k_m}$. Furthermore, if there is at least one $\sigma_j \neq \emptyset$, then the rule can only be applied if at least one $\sigma_{kl} \neq \emptyset$. The reason behind this condition is explained later in Section 3.2 (along the intuition of $A[\psi_1 \Uparrow \psi_2]$). On the other hand, if we have a self-modifying rule $p \xrightarrow{(\rho_1, \rho_2)} p' \in \Delta_i^{c'}$, then $\mathcal{B}\mathcal{P}_i$ transitions into $((\langle p', \gamma u \rangle, (\theta \setminus \rho_1) \cup \rho_2))$, i.e. changes the control location to $p'$, removes symbols of $\rho_1$ from $\theta$, and adds symbols of $\rho_2$ to $\theta$.

A run $\eta$ of $\mathcal{B}\mathcal{P}_i$ is a tree, where each node is labelled with a configuration of the form $((p, \omega), \theta)$, and if, for $D \subseteq D_i$, a transition of the form $((p, \omega), \theta) \mathrel{\substack{\xrightarrow{D} \\[-0.5ex] \xleftarrow{\{((p_1, \omega_1), \theta_1), \dots, ((p_m, \omega_m), \theta_m)\}}}}$ took place at the node labelled by $((p, \omega), \theta)$, then the node has exactly $m$ children, and for each $j$, $1 \le j \le m$, the $j$-th child is labelled by $((p_j, \omega_j), \theta_j)$. A run $\eta$ is accepting if every branch of $\eta$ visits some accepting control locations from $F_i$ infinitely often. We say that $\mathcal{B}\mathcal{P}_i$ accepts a pair of a configuration and a set of DCLICs (c, D) if there is an accepting run that starts from c and D is the set of DCLICs spawned across all branches. We denote by $\mathcal{L}(\mathcal{B}\mathcal{P}_i)$ the set of all pairs (c, D) accepted by $\mathcal{B}\mathcal{P}_i$.

## 3.2 From CTL Model Checking of SM-DPDS to the Emptiness Problem of SM-ABDPDS

We fix a single-indexed CTL formula $f = \bigwedge_{i=1}^n f_i$ on $\mathcal{M}$, where for $1 \le i \le n$, $f_i$ is a CTL formula on $\mathcal{P}_i$ with a corresponding set of atomic propositions $AP_i$ and a valuation function $v_i$. We show in this section how to compute the SM-ABDPDS that corresponds to the product between the SM-DPDS and the CTL formula. For readability, rules of the form $p\gamma \mathrel{\substack{\xrightarrow{p_1\omega_1} \\[-0.5ex] \xleftarrow{\emptyset}}}$ may be denoted as $p\gamma \mathrel{\substack{\xrightarrow{p_1\omega_1} \\[-0.5ex] \xleftarrow{p_2\omega_2\theta_2}}}$, and rules of the form $p\gamma \mathrel{\substack{\xrightarrow{p_1\omega_1} \\[-0.5ex] \xleftarrow{p_2\omega_2\theta_2}}}$ may be denoted

as $p\gamma \mathrel{\substack{\xrightarrow{p_1\omega_1} \\[-0.5ex] \xleftarrow{p_2\omega_2\theta_2}}}$). We suppose w.l.o.g. that the set of control locations $P_i$ is in the form of $P_i = P_i^N \cup P_i^S$, such that $P_i^N$ contains control locations from which only rules of the form $p\gamma \mathrel{\substack{\xrightarrow{p_1\omega_1} \\[-0.5ex] \xleftarrow{D}}}$ can apply, $P_i^S$ contains control locations from which only self-modifying rules from $\Delta_i^c$ can apply, and $P_i^N \cap P_i^S = \emptyset$.

There are several problems that arise when we compute the product of CTL formulas and SM-DPDS. Solving these problems necessitates the complex structure of SM-ABDPDS rules. The idea is that we want to encode the CTL formula $\psi$ into control locations of the SM-ABDPDS, such that $((\langle p, \omega \rangle, \theta))$ satisfies $\psi$ in the SM-DPDS only if there is an accepting run in the SM-ABDPDS starting from $((\langle p, \psi \rangle, \omega), \theta)$. Intuitively, let e.g. $\psi = \mathbf{AX}\psi_1$ and let $((\langle p_1, \omega_1 \rangle, \theta_1), \dots, (\langle p_m, \omega_m \rangle, \theta_m))$ be all successors of $((\langle p, \omega \rangle, \theta))$ in the SM-DPDS. Following the idea inductively, the computed SM-ABDPDS should be such that for every $j$, $1 \le j \le m$, the successor $((\langle p_j, \omega_j \rangle, \theta_j))$ satisfies $\psi_1$ in the SM-DPDS only if there is an accepting run in the SM-ABDPDS starting from $((\langle p_j, \psi_1 \rangle, \omega_j), \theta_j)$. To achieve this, we extend the method proposed in [32]. Suppose $\omega = \gamma v$ and there are exactly $h$ rules in the SM-DPDS with $p\gamma$ on the left-hand side: $r_1 = p\gamma \mathrel{\substack{\xrightarrow{p_1u_1} \\[-0.5ex] \xleftarrow{D_1, \dots, D_h}}}$, $r_h = p\gamma \mathrel{\substack{\xrightarrow{p_hu_h} \\[-0.5ex] \xleftarrow{p_1u_1} D_h}}$ (the case where self-modifying rules can be applied is treated later). Then, to guarantee that the SM-ABDPDS has an accepting run from $((\langle p, \psi \rangle, \gamma v), \theta)$ only if it has accepting runs from all the successors $((\langle p_j, \psi_1 \rangle, u_jv), \theta)$ for each $j$, $1 \le j \le h$, we add the rule $[p, \mathbf{AX}\psi_1]\gamma \mathrel{\substack{\xrightarrow{[r_1, \dots, r_h]} \\[-0.5ex] \xleftarrow{[p_1, \psi_1]u_1, \dots, [p_h, \psi_1]u_h} D_j}}$ to the SM-ABDPDS. However, this is not completely correct because of the presence of phases; i.e. the rules $r_j$, $1 \le j \le h$, are not guaranteed to be all in the phase $\theta$. Indeed, suppose the rule $r_h = p\gamma \mathrel{\substack{\xrightarrow{p_hu_h} \\[-0.5ex] \xleftarrow{D_h}}}$ is not in $\theta$. Then, $((\langle p_h, u_hv \rangle, \theta_h))$ is not a successor of $((\langle p, \gamma v \rangle, \theta))$, and even if $((\langle p_h, u_hv \rangle, \theta_h))$ does not satisfy $\psi_1$, $((\langle p, \gamma v \rangle, \theta))$ still satisfies $\mathbf{AX}\psi_1$. Moreover, $D_h$ cannot be spawned in the SM-DPDS and thus, the SM-ABDPDS should not spawn $D_h$ as well. Therefore, we introduce the $\sigma$-labels on rules of the SM-ABDPDS that check whether each rule $r_i$ of the SM-DPDS is in $\theta$ or not. The labels specify which rules must be present in the current phase for each (1) branch to be applied and (2) set of the DCLICs to be spawned. Therefore, we label our rule as follows: $[p, \mathbf{AX}\psi_1]\gamma \mathrel{\substack{\xrightarrow{[r_1, \dots, r_h]} \\[-0.5ex] \xleftarrow{[p_1, \psi_1]u_1, \dots, [p_h, \psi_1]u_h} D_1, \dots, D_h}}$. This rule uses the labels $[r_1, \dots, r_h]$ to impose that for $j$, $1 \le j \le h$, $((\langle p_j, \psi_1 \rangle, u_jv), \theta)$ is a successor of $((\langle p, \psi_1 \rangle, \gamma v), \theta)$ that spawns $D_j$ only if $r_j$ is in $\theta$. You can see that if $r_h$ is not in $\theta$, then the SM-ABDPDS branches into the set $((\langle p_1, \psi_1 \rangle, u_1v), \theta)$, $\dots$, $((\langle p_{h-1}, \psi_1 \rangle, u_{h-1}v), \theta)$, which corresponds to the accurate set of successors, and spawns $\bigcup_{j=1}^{h-1} D_j$, which is the accurate set of DCLICs.

However, this is not enough if we talk about self-modifying rules. Suppose instead of pushdown rules, we can apply self-modifying

rules $r_1 = p \xrightarrow{(\rho_1, \rho'_1)} p_1, \dots, r_h = p \xrightarrow{(\rho_h, \rho'_h)} p_h$ to the configuration $c = ((p, \omega), \theta)$. Now, suppose every rule $r_1, \dots, r_h$ is in $\theta$. This would still not guarantee that there are $h$ successors of $c$. Indeed, if $\rho_h$ contains some $r'$, such that $r' \notin \theta$, then $r_h$ cannot be applied. Therefore, we need to label the rules of the SM-ABDPDS by sets of rules as follows: $[p, \mathbf{AX}\psi_1]\gamma \mathrel{\substack{\xrightarrow{[\sigma_1, \dots, \sigma_h]} \\[-0.5ex] \xleftarrow{[p_1, \psi_1]u_1, \dots, [p_h, \psi_1]u_h} D_1, \dots, D_h}}$, where for $j$, $1 \le j \le h$, $\sigma_j = \rho_j \cup \{r_j\}$. This guarantees that $((\langle p_j, \psi_1 \rangle, \omega), \theta)$ is a successor of $((\langle p, \psi \rangle, \omega), \theta)$ only if $r_j \in \theta$
and $\rho_j \subseteq \theta$. Now, the labels represent the correct semantics of the SM-DPDS. To ensure that the SM-ABDPDS simulates the self-modifying behaviour of the corresponding SM-DPDS, for each $j$, $1 \le j \le h$, we introduce auxillary control locations of the form $p_{r_j}^{\psi_1}$, such that $[p, AX\psi_1]\gamma \xrightarrow{[\sigma_1, \dots, \sigma_h]} \{p_{r_1}^{\psi_1}, \omega, \theta\}, \dots, (p_{r_m}^{\psi_1}, \omega, \theta)\}$, and we add self-modifying rules of the form $p_{r_j}^{\psi_1} \xrightarrow{(\rho_j, \rho'_j)} [p_j, \psi_1]$. This guarantees that the SM-ABDPDS first branches into $\{((p_{r_1}^{\psi_1}, \omega), \theta), \dots, ((p_{r_m}^{\psi_1}, \omega), \theta)\}$, and then the self-modifying rules are applied, obtaining $\{((p_1, \psi_1], \omega), \theta_1), \dots, (([p_m, \psi_1], \omega), \theta_m)\}$, where for $j, 1 \le j \le m$, $((p_j, \omega), \theta_j)$ is a successor of $((p, \omega), \theta)$ in the SM-DPDS, i.e. $\theta_j = (\theta \setminus \rho_j) \cup \rho'_j$.

Now, we are ready to describe the formal computation of the product SM-ABDPDS. Let $cl(f_i)$ be the closure of $f_i$, i.e. the set of all subformulas in $f_i$. We construct an SM-ABDPDS $\mathcal{BP}_i = (P'_i, \Gamma_i, \Delta'_i, \Delta'_i, F_i, \Delta_i \cup \Delta'_i)$, where $P'_i = P_i \times cl(f_i) \cup P_i^{cl(f_i)}$, s.t. $P_i^{cl(f_i)}$ is a set of additional control locations of the form $p_r^{\psi}$ where $p \in P_i$, $\psi \in cl(f_i)$, $r \in \Delta'_i$. $F_i = (P \times \{a, \neg a\})$, where $cl_R(f_i)$ is the set of subformulas in $f_i$ of the form $A[\psi_1 R \psi_2]$ or $E[\psi_1 R \psi_2]$.

Now, we show the construction procedure for $\Delta'_i$ and $\Delta'_i$. Initially, $\Delta'_i = \Delta'_i^{c'} = \emptyset$. Then, for every $\psi \in cl(f_i)$, $\gamma \in \Gamma_i$, $p \in P_i$:

(1) if $\psi = a$, $a \in AP_i$, s.t. $p \in v(a)$, or $\psi = \neg a$ and $p \notin v(a)$, then $[p, \psi]\gamma \xrightarrow{[0]} \{[p, \psi]\gamma\} \triangleright \{\emptyset\} \in \Delta'_i$,

(2) if $\psi = \psi_1 \wedge \psi_2$, then $[p, \psi]\gamma \xrightarrow{[0,0]} \{[p, \psi_1]\gamma, [p, \psi_2]\gamma\} \triangleright \{\emptyset, \emptyset\} \in \Delta'_i$,

(3) if $\psi = \psi_1 \vee \psi_2$, then $[p, \psi]\gamma \xrightarrow{[0]} \{[p, \psi_1]\gamma\} \triangleright \{\emptyset\} \in \Delta'_i$ and $[p, \psi]\gamma \xrightarrow{[0]} \{[p, \psi_2]\gamma\} \triangleright \{\emptyset\} \in \Delta'_i$,

(4) if $\psi = EX\psi_1$, then:

(a) if $\exists r = p\gamma \hookrightarrow p'\omega \triangleright D \in \Delta_i$, then $[p, \psi]\gamma \xrightarrow{[r]} \{[p', \psi_1]\omega\} \triangleright \{D\} \in \Delta'_i$,

(b) if $\exists r = p \xrightarrow{(\rho_1, \rho_2)} p' \in \Delta'_i$, then $[p, \psi]\gamma \xrightarrow{[\{r\} \cup \rho_1]} \{p_r^{\psi_1}\gamma\} \triangleright \{\emptyset\} \in \Delta'_i$, and $p_r^{\psi_1} \xrightarrow{(\rho_1, \rho_2)} [p', \psi_1] \in \Delta'_i$.

(5) if $\psi = AX\psi_1$, then:

(a) if $p \in P_i^N$, let $\{r_1 = p\gamma \hookrightarrow p_1\omega_1 \triangleright D_1, \dots, r_m = p\gamma \hookrightarrow p_m\omega_m \triangleright D_m\}$ be the set of all rules in $\Delta_i$ that have $p\gamma$ as left-hand side. Then, $[p, \psi]\gamma \xrightarrow{[\{r_1\}, \dots, \{r_m\}]} \{[p_1, \psi_1]\omega_1, \dots, [p_m, \psi_1]\omega_m\} \triangleright \{D_1, \dots, D_m\} \in \Delta'_i$.

(b) if $p \in P_i^S$, let $\{r_1 = p \xrightarrow{(\rho_1, \rho'_1)} p_1, \dots, r_m = p \xrightarrow{(\rho_m, \rho'_m)} p_m\}$ be the set of all self-modifying rules in $\Delta'_i$ that have $p$ as left-hand side. Then, $[p, \psi]\gamma \xrightarrow{[\sigma_1, \dots, \sigma_m]} \{p_{r_1}^{\psi_1}, \dots, p_{r_m}^{\psi_1}\gamma\} \triangleright \{\emptyset, \dots, \emptyset\} \in \Delta'_i$, where for every $j, 1 \le j \le m$, $\sigma_j = \{r_j\} \cup \rho_j$, and $p_{r_j}^{\psi_1} \xrightarrow{(\rho_j, \rho'_j)} [p_j, \psi_1] \in \Delta'_i$.

(6) if $\psi = E[\psi_1 U \psi_2]$, $[p, \psi]\gamma \xrightarrow{[0]} \{[p, \psi_2]\gamma\} \triangleright \{\emptyset\} \in \Delta'_i$ and:

(a) if $\exists r = p\gamma \hookrightarrow p'\omega \triangleright D \in \Delta_i$, then $[p, \psi]\gamma \xrightarrow{[\{r\}, \{r\}]} \{[p, \psi_1]\gamma, [p', \psi]\omega\} \triangleright \{\emptyset, D\} \in \Delta'_i$,

(b) if $\exists r = p \xrightarrow{(\rho_1, \rho_2)} p' \in \Delta'_i$, then $[p, \psi]\gamma \xrightarrow{[\sigma, \sigma]} \{[p, \psi_1]\gamma, p'_r \gamma\} \triangleright \{\emptyset, \emptyset\} \in \Delta'_i$, where $\sigma = \{r\} \cup \rho_1$, and $p'_r \xrightarrow{(\rho_1, \rho_2)} [p', \psi] \in \Delta'_i$.

(7) if $\psi = A[\psi_1 U \psi_2]$, $[p, \psi]\gamma \xrightarrow{[0]} \{[p, \psi_2]\gamma\} \triangleright \{\emptyset\} \in \Delta'_i$ and:

(a) if $p \in P_i^N$, let $\{r_1 = p\gamma \hookrightarrow p_1\omega_1 \triangleright D_1, \dots, r_m = p\gamma \hookrightarrow p_m\omega_m \triangleright D_m\}$ be the set of all rules in $\Delta_i$ that have $p\gamma$ as left-hand side. Then, $[p, \psi]\gamma \xrightarrow{[0, \{r_1\}, \dots, \{r_m\}]} \{[p, \psi_1]\gamma, [p_1, \psi]\omega_1, \dots, [p_m, \psi]\omega_m\} \triangleright \{\emptyset, D_1, \dots, D_m\} \in \Delta'_i$,

(b) if $p \in P_i^S$, let $\{r_1 = p \xrightarrow{(\rho_1, \rho'_1)} p_1, \dots, r_m = p \xrightarrow{(\rho_m, \rho'_m)} p_m\}$ be the set of all self-modifying rules in $\Delta'_i$ that have $p$ as left-hand side. Then, $[p, \psi]\gamma \xrightarrow{[0, \sigma_1, \dots, \sigma_m]} \{[p, \psi_1]\gamma, p_{r_1}^{\psi_1}, \dots, p_{r_m}^{\psi_1}\gamma\} \triangleright \{\emptyset, \dots, \emptyset\} \in \Delta'_i$, where for every $j, 1 \le j \le m$ $j \le m$, $\sigma_j = \{r_j\} \cup \rho_j$, and $p_{r_j}^{\psi_1} \xrightarrow{(\rho_j, \rho'_j)} [p_j, \psi] \in \Delta'_i$.

(8) if $\psi = E[\psi_1 R \psi_2]$, then $[p, \psi]\gamma \xrightarrow{[0,0]} \{[p, \psi_1]\gamma, [p, \psi_2]\gamma\} \triangleright \{\emptyset, \emptyset\} \in \Delta'_i$ and:

(a) if $\exists r = p\gamma \hookrightarrow p'\omega \triangleright D \in \Delta_i$, then $[p, \psi]\gamma \xrightarrow{[\{r\}, \{r\}]} \{[p, \psi_2]\gamma, [p', \psi]\omega\} \triangleright \{\emptyset, D\} \in \Delta'_i$,

(b) if $\exists r = p \xrightarrow{(\rho_1, \rho_2)} p' \in \Delta'_i$, then $[p, \psi]\gamma \xrightarrow{[\sigma, \sigma]} \{[p, \psi_2]\gamma, p'_r \gamma\} \triangleright \{\emptyset, \emptyset\} \in \Delta'_i$, where $\sigma = \{r\} \cup \rho_1$, and $p'_r \xrightarrow{(\rho_1, \rho_2)} [p', \psi] \in \Delta'_i$.

(9) if $\psi = A[\psi_1 R \psi_2]$, then $[p, \psi]\gamma \xrightarrow{[0,0]} \{[p, \psi_1]\gamma, [p, \psi_2]\gamma\} \triangleright \{\emptyset, \emptyset\} \in \Delta'_i$ and:

(a) if $p \in P_i^N$, let $\{r_1 = p\gamma \hookrightarrow p_1\omega_1 \triangleright D_1, \dots, r_m = p\gamma \hookrightarrow p_m\omega_m \triangleright D_m\}$ be the set of all rules from $\Delta_i$ that have $p\gamma$ as left-hand side. Then, $[p, \psi]\gamma \xrightarrow{[0, \{r_1\}, \dots, \{r_m\}]} \{[p, \psi_2]\gamma, [p_1, \psi]\omega_1, \dots, [p_m, \psi]\omega_m\} \triangleright \{\emptyset, D_1, \dots, D_m\} \in \Delta'_i$.

(b) if $p \in P_i^S$, let $\{r_1 = p \xrightarrow{(\rho_1, \rho'_1)} p_1, \dots, r_m = p \xrightarrow{(\rho_m, \rho'_m)} p_m\}$ be the set of all self-modifying rules in $\Delta'_i$ that have $p$ as left-hand side. Then, $[p, \psi]\gamma \xrightarrow{[0, \sigma_1, \dots, \sigma_m]} \{[p, \psi_2]\gamma, p_{r_1}^{\psi_1}, \dots, p_{r_m}^{\psi_1}\gamma\} \triangleright \{\emptyset, \emptyset\} \in \Delta'_i$, where for every $j, 1 \le j \le m$, $\sigma_j = \{r_j\} \cup \rho_j$ and $p_{r_j}^{\psi_1} \xrightarrow{(\rho_j, \rho'_j)} [p_j, \psi] \in \Delta'_i$.

Then, we can show that:

**THEOREM 3.2.** *Given a local configuration $((p, \omega), \theta)$ and a set of DCLICs $D$ of $\mathcal{P}_i$, $((p, \omega), \theta) \models_D f_i$ iff $((\langle[p, f_i], \omega\rangle, \theta), D) \in \mathcal{L}(\mathcal{BP}_i)$.*

Intuitively, the resulting SM-ABDPDS $\mathcal{BP}_i = (P'_i, \Gamma_i, \Delta'_i, \Delta'_i, F_i, \Delta_i \cup \Delta'_i)$ has the set of control locations $P'_i$, which is a product between $P_i$ and $f_i$. The idea is that if for some configuration $((p, \gamma\omega), \theta)$ of $\mathcal{P}_i$, $((p, \gamma\omega), \theta) \models_D \psi$, then there is an accepting run of SM-ABDPDS $\mathcal{BP}_i$ from $((\langle p, \psi \rangle, \gamma\omega), \theta)$ that spawns $D$.

If $\psi = a$, $a \in AP_i$. Suppose $p \in v(a)$, then for any $\omega \in \Gamma_i^*$ and $\theta \subseteq \Delta_i \cup \Delta'_i$, $((p, \omega), \theta) \models_\emptyset a$. Thus, there should be an accepting run from $((\langle p, a \rangle, \omega), \theta)$. To guarantee this, Item 1 creates an infinite loop of the form $[p, a]\gamma \xrightarrow{[0]} \{[p, a]\gamma\} \triangleright \{\emptyset\}$ and we let $[p, a]$ be in $F_i$. The same logic is applied for the case if $\psi = \neg a$.

If $\psi = \psi_1 \wedge \psi_2$, then Item 2 adds rule of the form $[p, \psi]\gamma \xrightarrow{[0,0]} \{[p, \psi_1]\gamma, [p, \psi_2]\gamma\} \triangleright \{\emptyset, \emptyset\}$, which means that $\mathcal{BP}_i$ transitions into
both $((\langle[p, \psi_1], \gamma\omega\rangle, \theta) \text{ and } ((\langle[p, \psi_2], \gamma\omega\rangle, \theta))$. Therefore, there is an accepting run from $((\langle[p, \psi], \gamma\omega\rangle, \theta) \text{ if there are accepting runs from both } ((\langle[p, \psi_1], \gamma\omega\rangle, \theta) \text{ and } ((\langle[p, \psi_2], \gamma\omega\rangle, \theta))$. The rule does not spawn DCLICs and this is why it is contains $\triangleright\{\emptyset, \emptyset\}$. A similar approach applies for $\psi = \psi_1 \lor \psi_2$ and Item 3.

The intuition behind the case $\psi = \mathbf{AX}\psi_1$ and Item 5 was given previously (in the introduction of this section). A similar intuition applies to $\psi = \mathbf{EX}\psi_1$ from Item 4.

If $\psi = \mathbf{A}[\psi_1\mathbf{U}\psi_2]$, then Item 7 adds such rules that $\mathcal{B}\mathcal{P}_i$ has an accepting run from $((\langle[p, \psi], \omega\rangle, \theta) \text{ only if either } ((p, \omega), \theta) \text{ satisfies } \psi_2, \text{ or it satisfies } \psi_1, \text{ and all the successors of } ((p, \omega), \theta) \text{ in } \mathcal{P}_i \text{ satisfy } \mathbf{A}[\psi_1\mathbf{U}\psi_2]$. Since the control locations of the form $[p, \mathbf{A}[\psi_1\mathbf{U}\psi_2]]$ are not in $F_i$, then the accepting run from $((\langle[p, \psi], \omega\rangle, \theta) \text{ in } \mathcal{B}\mathcal{P}_i$ guarantees that $\psi_2$ is satisfied in the future. Note that if there are no successors, the rule in $\mathcal{B}\mathcal{P}_i$ will not be applied (because there is no such $\sigma_j \subseteq \theta$ and $\sigma_j \neq \emptyset$). This is guaranteed by the semantics of $\mathcal{B}\mathcal{P}_i$ - either $\forall j, \sigma_j = \emptyset \text{ or } \exists j, \sigma_j \subseteq \theta \text{ and } \sigma_j \neq \emptyset$. A similar intuition applies to $\psi = \mathbf{E}[\psi_1\mathbf{U}\psi_2]$ from Item 6.

If $\psi = \mathbf{A}[\psi_1\mathbf{R}\psi_2]$, then Item 9 adds rules such that $((p, \omega), \theta)$ satisfies $\psi$ in $\mathcal{P}_i$ only if it satisfies $\psi_2$ and either it also satisfies $\psi_1$, or all successors satisfy $\psi$. We let $[p, \psi]$ be in $F_i$ to guarantee that infinite runs that always satisfy $\psi_2$ are accepting. A similar intuition applies to $\psi = \mathbf{E}[\psi_1\mathbf{R}\psi_2]$.

## 3.3 Solving the Emptiness Problem of SM-ABDPDS

To compute $\mathcal{L}(\mathcal{B}\mathcal{P}_i)$, we introduce the *predecessors function* $\mathit{pre}\mathcal{B}\mathcal{P}_i$, s.t. for a set of configurations and DCLICs W with elements of the form $((\langle p, \omega \rangle, \theta), D) \in W$, where $p \in P'_i$, $\omega \in \Gamma_i^*$, $\theta \subseteq \Delta_i \cup \Delta_i^c$, $D \subseteq \mathcal{D}_i$, $\mathit{pre}\mathcal{B}\mathcal{P}_i(W) = \{(c, D) | c \xrightarrow{D_0} \{c_1, \dots, c_m\}, \forall j, 1 \le j \le m : (c_j, D_j) \in W \wedge D = \bigcup_{j=0}^m D_j\}$. We also define the reflexive-transitive closure: $\mathit{pre}^*_{\mathcal{B}\mathcal{P}_i}(W) = \{(c, D) | (c, D) \in W \text{ or } c \xrightarrow{D_0} \{c_1, \dots, c_m\}, \forall j, 1 \le j \le m : (c_j, D_j) \in \mathit{pre}^*_{\mathcal{B}\mathcal{P}_i}(W) \text{ and } D = \bigcup_{j=0}^m D_j\}$. Let $\mathit{pre}^+_{\mathcal{B}\mathcal{P}_i}(W) = \mathit{pre}^*_{\mathcal{B}\mathcal{P}_i}(\mathit{pre}\mathcal{B}\mathcal{P}_i(W))$. Intuitively, the set $\mathit{pre}^*(W)$ contains all pairs of the form $(c, D)$, where $c$ is the configuration that can reach one of the configurations from W in zero or more steps, and D is the set of DCLICs spawned to reach from c to W. On the other hand, $\mathit{pre}^+(W)$ requires at least one transition to reach W. We write $\mathit{pre}$, $\mathit{pre}^*$, and $\mathit{pre}^+$ when $\mathcal{B}\mathcal{P}_i$ can be understood from the current context.

We can compute set $Y_{\mathcal{B}\mathcal{P}_i}$ representing $\mathcal{L}(\mathcal{B}\mathcal{P}_i)$. Let $Y_0Y_1...$ be an infinite sequence of sets of configurations and DCLICs that computes configurations of $\mathcal{B}\mathcal{P}_i$ from which we can construct accepting runs. Let $Y_0 = P'_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta_i^c} \times \{\emptyset\}$, and for every $j \ge 0$, $Y_{j+1} = \mathit{pre}^+(Y_j \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta_i^c} \times 2^{\mathcal{D}_i})$. Let $Y_{\mathcal{B}\mathcal{P}_i} = \bigcap_{j \ge 1} Y_j$. Then:

**PROPOSITION 3.3.** $\mathcal{L}(\mathcal{B}\mathcal{P}_i) = Y_{\mathcal{B}\mathcal{P}_i}$.

Let us explain the intuition behind $Y_{\mathcal{B}\mathcal{P}_i}: Y_1$ contains pairs of configurations and DCLICs $(c_1, D_1)$, such that $c_1$ forks into $\{c_0^1, \dots, c_0^m\}$ and requires $D_1$ to be spawned, where $c_0^1, \dots, c_0^m$ are configurations at accepting control locations. Next, $Y_2$ contains pairs $(c_2, D_2)$, such that $c_2$ forks into $\{c_1^1, \dots, c_1^m\}$ and $(c_1^1, D_1^1), \dots, (c_1^m, D_1^m) \in Y_1$, $c_1^1, \dots, c_1^m$ are also at accepting control locations, and if this path spawns some $D'_2$, then $D_2 = D'_2 \cup \bigcup_{j=1}^m D_j^i$. In other words, $Y_2$ contains such pairs $(c_2, D_2)$ that have runs visiting accepting control

locations at least twice. In a similar fashion, for $j \ge 1$, $Y_j$ contains $(c_j, D_j)$, such that there is a run from $c_j$ that visits accepting control locations at least $j$ times and spawns DCLICs $D_j$. Inductively, if there is $(c, D)$, such that $(c, D) \in Y_j$ for every $j \ge 1$, then there is a run starting from $c$ that visits accepting control locations infinitely many times and spawns $D$. Since $Y_{\mathcal{B}\mathcal{P}_i} = \bigcap_{j \ge 1} Y_j$, then $(c, D) \in Y_{\mathcal{B}\mathcal{P}_i}$.

## 3.4 Computing $Y_{\mathcal{B}\mathcal{P}_i}$

To effectively compute $Y_{\mathcal{B}\mathcal{P}_i}$, we need to finitely represent possibly infinite sets of local configurations and DCLICs. We use *Alternating Multi-Automata (AMA)* for this purpose.

**Definition 3.4.** An Alternating Multi-Automaton (AMA) is a tuple $\mathcal{A}_i = (Q_i, \Gamma_i, T_i, I_i, \text{Acc}_i)$, where $Q_i$ is a finite set of states, $I_i = P'_i \times 2^{\Delta_i \cup \Delta_i^c} \subseteq Q_i$ is the set of initial states of the form $(p, \theta)$, $\text{Acc}_i \subseteq Q_i$ is the set of accepting states, and $T_i \subseteq Q_i \times \Gamma_i \times 2^{\mathcal{D}_i} \times 2^{Q_i}$ is the set of transitions.

Consider an AMA $\mathcal{A}_i = (Q_i, \Gamma_i, T_i, I_i, \text{Acc}_i)$. For readability, a transition of the form $(q, \gamma, D, \{q_1, \dots, q_m\})$ will be denoted by $q \xrightarrow{\gamma/D} \{q_1, \dots, q_m\}$, where $q, q_1, \dots, q_m \in Q_i$, $\gamma \in \Gamma_i$, $D \subseteq \mathcal{D}_i$. We define the reflexive-transitive relation $\to^*$ as follows: (1) $q \xrightarrow{\epsilon/\emptyset} \{q\}$ for every $q \in Q_i$, (2) if $q \xrightarrow{\gamma/D} \{q_1, \dots, q_m\}$ and if for every $j, 1 \le j \le m$, $q_j \xrightarrow{\omega/D_j} S_j$ for some $S_j \subseteq Q_i$, then $q \xrightarrow{\gamma\omega/D \cup \bigcup_{j=1}^m D_j} \{\omega/D\} \cup \bigcup_{j=1}^m S_j$. For $p \in P'_i$, $\omega \in \Gamma_i^*$, $\theta \subseteq \Delta_i \cup \Delta_i^c$, $D \subseteq \mathcal{D}_i$, $\mathcal{A}_i$ accepts a pair of a local configuration and a set of DCLICs $((\langle p, \omega \rangle, \theta), D)$ if there is $S \subseteq \text{Acc}_i$, such that $(p, \theta) \xrightarrow{\omega/D} S$. We denote by $\mathcal{L}(\mathcal{A}_i)$ the set of all such pairs accepted by $\mathcal{A}_i$.

We can show that we can effectively compute $Y_{\mathcal{B}\mathcal{P}_i}$ by constructing an AMA $\mathcal{A}_i = (Q_i, \Gamma_i, T_i, I_i, \{q_f\})$, where $q_f$ is the single accepting state; $I_i \subseteq P'_i \times 2^{\Delta_i \cup \Delta_i^c} \times \mathbb{N}$ is a set of enumerated states in the form $(p, \theta)^k$ for $p \in P'_i$, $\theta \subseteq \Delta_i \cup \Delta_i^c$, $k \in \mathbb{N}$; $Q_i = I_i \cup \{q_f\}$, and $T_i$ is a set of transitions computed by Algorithm 1. Intuitively, to compute $Y_{\mathcal{B}\mathcal{P}_i}$, we iteratively compute $Y_k$ for $k \ge 1$, such that $((\langle p, \omega \rangle, \theta), D) \in Y_k$ iff there is a path $(p, \theta)^k \xrightarrow{\omega/D} \{q_f\}$ in $\mathcal{A}_i$. In order to make the construction terminate, for some set of states $S \subseteq Q_i$, we introduce the projection function $\pi$:

$$ \pi^{-1}(S) = \begin{cases} \{q^k | q^{k+1} \in S\} \cup \{q_f\} & \text{if } q_f \in S \text{ or } \exists q^1 \in S \\ \{q^k | q^{k+1} \in S\} & \text{else} \end{cases} \\ \pi^k(S) = \{q^k | \exists j, 1 \le j \le k : q^j \in S\} \cup \{q_f | q_f \in S\} $$

Now, we introduce Algorithm 1 that computes an AMA $\mathcal{A}_i$, such that $\mathcal{L}(\mathcal{A}_i) = \mathcal{L}(\mathcal{B}\mathcal{P}_i)$. It consists of two nested loops: loop 1 and loop 2, where loop 2 is a saturation procedure to compute $\mathit{pre}^*(Y_{k-1} \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta_i^c} \times 2^{\mathcal{D}_i})$, and loop 1 iterates over $k$ and computes $Y_k$. We show that:

**THEOREM 3.5.** *Algorithm 1 terminates and computes $Y_{\mathcal{B}\mathcal{P}_i}$.*

Intuitively, for every $k \ge 0$, Algorithm 1 computes AMAs $A_k$, such that for a configuration $((\langle p, \omega \rangle, \theta), D) \in \mathcal{L}(A_k)$ if $(p, \theta)^k \xrightarrow{\omega/D} \{q_f\}$. $A_k$ is such that $\mathcal{L}(A_k) = Y_k$. The computation of $A_0$ is defined by line 1 ($A_0$ accepts all local configurations since $Y_0 = P'_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta_i^c} \times \{\emptyset\}$).
**Algorithm 1** Computation of $Y_{\mathcal{B}\mathcal{P}_i}$

**Input:** An SM-ABDPDS $\mathcal{B}\mathcal{P}_i = (P'_i, \Gamma_i, \Delta'_i, \Delta'_i, F_i, \Delta_i \cup \Delta'_i)$.

**Output:** An AMA $\mathcal{A}_i = (Q_i, \Gamma_i, T_i, I_i, \{q_f\})$.

1. $k := 0, T_i := \{q_f \xrightarrow{Y/\theta} \{q_f\} | \forall \gamma \in \Gamma_i\}, \forall p \in P'_i \text{ and } \forall \theta \subseteq \Delta_i \cup \Delta'_i$, $(p, \theta)^0 := q_f$;

2. **repeat**(we call this loop$_1$)

3. $k := k + 1$;

4. For all $p \in F_i$, $\theta \subseteq \Delta_i \cup \Delta'_i$, add $(p, \theta)^k \xrightarrow{\varepsilon/\theta} \{(p, \theta)^{k-1}\} \in T_i$;

5. **repeat**(we call this loop$_2$)

6. **for all** $\theta \subseteq \Delta_i \cup \Delta'_i$, $p\gamma \xrightarrow{[\sigma_1, \dots, \sigma_m]} \{p_1\omega_1, \dots, p_m\omega_m\} \triangleright \{D_1, \dots, D_m\} \in \Delta'_i$, s.t. for $j, 1 \le j \le m$, $(p_j, \theta)^k \xrightarrow{\omega_j/D'_j} R_j \text{ do}$

7. add $(p, \theta)^k \xrightarrow{Y/D} R \in T_i$, s.t. $R = \{q \in R_j | \exists j, 1 \le j \le m : \sigma_j \subseteq \theta\}$ and $D = \{d \in D_j \cup D'_j | \exists j, 1 \le j \le m : \sigma_j \subseteq \theta\}$

8. **end for**

9. **for all** $\theta \subseteq \Delta_i \cup \Delta'_i$, $p \xrightarrow{(\rho_1, \rho_2)} p' \in \Delta'_i$, and $\gamma \in \Gamma_i$, s.t. $(p', \theta')^k \xrightarrow{Y/D} R$, where $\theta' = (\theta\rho_1) \cup \rho_2 \text{ do}$

10. add $(p, \theta)^k \xrightarrow{Y/D} R \in T_i$;

11. **end for**

12. **until** No new transitions can be added;

13. For all $p \in F_i$, $\theta \subseteq \Delta_i \cup \Delta'_i$, remove $(p, \theta)^k \xrightarrow{\varepsilon/\theta} \{(p, \theta)^{k-1}\}$ from $T_i$;

14. For all $p \in P'_i$, $\theta \subseteq \Delta_i \cup \Delta'_i$, $\gamma \in \Gamma_i$, $R \subseteq Q_i$, $D \subseteq \mathcal{D}_i$, replace $(p, \theta)^k \xrightarrow{Y/D} R$ by $(p, \theta)^k \xrightarrow{Y/D} \pi^k(R)$;

15. **until** $k > 1$ and $\forall p \in P'_i$, $\gamma \in \Gamma_i$, $\theta \subseteq \Delta_i \cup \Delta'_i$, $R \subseteq P'_i \times 2^{\Delta_i \cup \Delta'_i} \times \{k\} \cup \{q_f\}, D \subseteq \mathcal{D}_i, (p, \theta)^k \xrightarrow{Y/D} R \in T_i \iff (p, \theta)^{k-1} \xrightarrow{Y/D} \pi^{-1}(R) \in T_i$;

loop$_1$ starting at line 2 iterates over $k \ge 1$ and computes $A_k$. Since $Y_k = \text{pre}^+(Y_{k-1} \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta'_i} \times 2^{\mathcal{D}_i})$, we first compute $Y_{k-1} \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta'_i} \times 2^{\mathcal{D}_i}$. Line 4 adds transitions $(p, \theta)^k \xrightarrow{\varepsilon/\theta} (p, \theta)^{k-1}$ for $p \in F_i$, therefore, $\mathcal{L}(A_k) = \mathcal{L}(A_{k-1}) \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta'_i} \times 2^{\mathcal{D}_i}$, which corresponds to $Y_{k-1} \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta'_i} \times 2^{\mathcal{D}_i}$. Then, loop$_2$ starting at line 5 adds predecessors of $A_k$ to the current AMA, obtaining $\mathcal{L}(A_k) = \text{pre}^*(Y_{k-1} \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta'_i} \times 2^{\mathcal{D}_i})$. Line 13 removes $\varepsilon$-transitions into states labelled by $k-1$. This excludes paths computed by $A_{k-1}$ from $A_k$, obtaining that $\mathcal{L}(A_k) = \text{pre}^+(Y_{k-1} \cap F_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta'_i} \times 2^{\mathcal{D}_i})$. If we reach the termination point at line 15, the condition implies that $A_k = A_{k-1}$ and thus, loop$_1$ has not modified $A_k$ at the last iteration. Which means, we could continue executing loop$_1$ indefinitely, obtaining the same AMA for every $l \ge k$, s.t. $A_l = A_k$. Thus, configurations recognized by $A_k$ not only visit accepting control locations at least $k$ times, but also can visit them at least $l$ times for every next AMA $A_l$, $l \ge k$, which can be obtained using loop$_1$. Therefore, if $(c, D) \in A_l$ for every $l, l \ge k$, then $(c, D) \in Y_l$ for every $l \ge k$ and thus, $(c, D) \in Y_{\mathcal{B}\mathcal{P}_i}$.

## 3.5 Effective Algorithm for Model Checking SM-DPNs

Now, we are ready to tackle the problem of efficient model-checking SM-DPNs over single-indexed CTL formulas. For each $i, 1 \le i \le n$, given the SM-DPDS $\mathcal{P}_i$ and the CTL formula $f_i$, we construct the product SM-ABDPDS $\mathcal{B}\mathcal{P}_i$. Then, we construct an AMA $\mathcal{A}_i$ using Algorithm 1. From Theorem 3.2, Proposition 3.3, and Theorem 3.5, $\mathcal{A}_i$ is such that for a local configuration $c$ and a set of DCLICs $D$, $(c, D) \in \mathcal{L}(\mathcal{A}_i)$ iff $c \models_D f_i$.

We then compute the maximal set of DCLICs $\mathcal{D}_{fp} \subseteq \bigcup_{i=1}^n \mathcal{D}_i$, s.t. for every $p\omega\theta \in \mathcal{D}_{fp}$, there exists $D \subseteq \mathcal{D}_{fp}$, s.t. $(\langle p, \omega \rangle, \theta) \models_D f_{\varphi(p)}$. Let $D_I = \bigcup_{i=1}^n \mathcal{D}_i$ be the whole set of DCLICs. We compute $\mathcal{D}_{fp}$ by finding the greatest fixpoint of the function $F: 2^{\bigcup_{j=1}^n \mathcal{D}_j} \to 2^{\bigcup_{j=1}^n \mathcal{D}_j}$, which is defined as follows: $F(D) = \{p\omega\theta \in D_I | \exists D' \subseteq D: ((\langle [p, f_{\varphi(p)}], \omega\rangle, \theta), D') \in \mathcal{L}(\mathcal{A}_{\varphi(p)})\}$. Let $D_1, D_2, \dots$ be the infinite sequence, such that $D_1 = D_I$ and for every $j, j \ge 2$, $D_j = F(D_{j-1})$. We can show that $\mathcal{D}_{fp} = \bigcap_{j \ge 1} D_j$.

**THEOREM 3.6.** We can effectively compute $\mathcal{D}_{fp}$, s.t. for every DCLIC $p\omega\theta \in \bigcup_{k=1}^n \mathcal{D}_k$, $(\langle p, \omega \rangle, \theta) \models f$ iff $p\omega\theta \in \mathcal{D}_{fp}$.

Intuitively, the computation of $\mathcal{D}_{fp}$ starts with every possible DCLIC $D_1 = D_I$. Then, $D_2$ excludes DCLICs that do not have an accepting run. Then $D_3$ will exclude such DCLICs that, during the accepting run, they must spawn DCLICs excluded by the previous step, etc. Since we have a finite number of DCLICs, this procedure terminates when it reaches $k \ge 1$, such that $D_{k+1} = D_k$. Finally, a global configuration $\mathcal{G} = (\langle p_1, \omega_1 \rangle, \theta_1) \dots (\langle p_m, \omega_m \rangle, \theta_m)$ satisfies a single-indexed CTL formula $f = \bigwedge_{i=1}^n f_i$ iff for every $j, 1 \le j \le m$, there exists $D_j \subseteq \mathcal{D}_{fp}$, s.t. $((\langle [p_j, f_{\varphi(p_j)}], \omega_j \rangle, \theta_j), D_j) \in \mathcal{L}(\mathcal{A}_{\varphi(p_j)})$.

# 4 Experiments

We implemented our approach in a tool and evaluated the algorithm's performance and capability to detect malware.

## 4.1 SM-DPN vs. DPN

An SM-DPN can be translated into a standard DPN by encoding its phase into the control locations of the DPN [25, 37]. Thus, to model check an SM-DPN over a single-indexed CTL formula, one could translate the SM-DPN into an equivalent DPN, and then apply the standard algorithm of CTL model-checking for DPNs [34]. However, this approach is not efficient. We have evaluated the performance of both our implementation and the one that consists in first translating the SM-DPN into a standard DPN and then applying the algorithm of [34]. We implemented the algorithms using the Zig programming language. Then, we compared the performance of both implementations on a set of randomly generated SM-DPNs. The experiments were run on a machine with Intel Core i3-4150 CPU with 4 cores at 3.50GHz each and 12GB available memory. The results of the comparison are presented in Table 1.

Our approach performs 1.84 times faster and consumes 5.79 times less memory than CTL model checking an equivalent DPN. We highlighted in the table some significant rows that show extreme differences in the memory required for both implementations. For example, for an SM-DPN with each process having 75 standard rules and 4 self-modifying rules, the naive approach required more than 4GB of memory, while our approach required only 620MB.
<table><caption>Table 1: Performance of our approach vs. DPN approach (|Δ| and |Δ<sup>c</sup>| are the numbers of pushdown and self-modifying rules respectively, OOM - out of memory).</caption><thead><tr><th rowspan="2">n</th><th rowspan="2">|Δ| + |Δ<sup>c</sup>|</th><th colspan="2">Our approach</th><th colspan="2">DPN approach</th></tr><tr><th>Time, s</th><th>Memory</th><th>Time, s</th><th>Memory</th></tr></thead><tbody><tr><td>2</td><td>79 + 4</td><td>23.95</td><td>209.10 MB</td><td>28.37</td><td>1.30 GB</td></tr><tr><td>2</td><td>32 + 5</td><td>1.35</td><td>42.13 MB</td><td>2.52</td><td>226.05 MB</td></tr><tr><td>2</td><td>58 + 5</td><td>9.79</td><td>257.13 MB</td><td>21.34</td><td>1.09 GB</td></tr><tr><td>2</td><td>73 + 5</td><td>23.33</td><td>554.66 MB</td><td>42.91</td><td>2.86 GB</td></tr><tr><td>2</td><td>86 + 7</td><td>160.46</td><td>2.32 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>2</td><td>113 + 7</td><td>668.78</td><td>4.98 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>2</td><td>69 + 11</td><td>428.01</td><td>8.88 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>2</td><td>90 + 11</td><td>354.67</td><td>5.93 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>3</td><td>60 + 3</td><td>102.7</td><td>706.90 MB</td><td>169.89</td><td>5.52 GB</td></tr><tr><td>3</td><td>87 + 3</td><td>9.66</td><td>146.71 MB</td><td>16.18</td><td>800.72 MB</td></tr><tr><td>3</td><td>89 + 3</td><td>1.76</td><td>53.90 MB</td><td>2.97</td><td>228.53 MB</td></tr><tr><td>3</td><td>72 + 4</td><td>9.24</td><td>258.34 MB</td><td>19.51</td><td>1.22 GB</td></tr><tr><td>3</td><td>112 + 4</td><td>15.87</td><td>417.59 MB</td><td>29.89</td><td>2.24 GB</td></tr><tr><td><strong>3</strong></td><td><strong>115 + 4</strong></td><td><strong>66.55</strong></td><td><strong>606.05 MB</strong></td><td><strong>89.04</strong></td><td><strong>3.92 GB</strong></td></tr><tr><td>3</td><td>57 + 5</td><td>10.53</td><td>352.55 MB</td><td>23.60</td><td>1.65 GB</td></tr><tr><td>3</td><td>112 + 5</td><td>234.69</td><td>1.64 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>3</td><td>68 + 6</td><td>97.05</td><td>709.04 MB</td><td>172.11</td><td>5.97 GB</td></tr><tr><td><strong>3</strong></td><td><strong>78 + 7</strong></td><td><strong>35.00</strong></td><td><strong>783.11 MB</strong></td><td><strong>88.05</strong></td><td><strong>5.09 GB</strong></td></tr><tr><td>3</td><td>96 + 7</td><td>103.03</td><td>1.85 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>3</td><td>44 + 8</td><td>781.39</td><td>5.32 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>3</td><td>56 + 8</td><td>108.63</td><td>1.86 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>3</td><td>90 + 8</td><td>253.22</td><td>3.50 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>4</td><td>66 + 3</td><td>2.89</td><td>104.74 MB</td><td>4.81</td><td>344.93 MB</td></tr><tr><td>4</td><td>31 + 4</td><td>37.89</td><td>445.64 MB</td><td>72.72</td><td>2.88 GB</td></tr><tr><td>4</td><td>56 + 4</td><td>60.17</td><td>465.05 MB</td><td>111.82</td><td>4.09 GB</td></tr><tr><td>4</td><td>78 + 5</td><td>23.65</td><td>361.00 MB</td><td>38.02</td><td>2.10 GB</td></tr><tr><td>4</td><td>117 + 6</td><td>834.59</td><td>5.79 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>4</td><td>45 + 8</td><td>74.70</td><td>1.48 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>5</td><td>93 + 3</td><td>4.52</td><td>139.67 MB</td><td>8.24</td><td>573.18 MB</td></tr><tr><td>5</td><td>51 + 4</td><td>7.52</td><td>144.61 MB</td><td>14.18</td><td>901.24 MB</td></tr><tr><td><strong>5</strong></td><td><strong>75 + 4</strong></td><td><strong>53.70</strong></td><td><strong>620.78 MB</strong></td><td><strong>93.21</strong></td><td><strong>4.42 GB</strong></td></tr><tr><td>5</td><td>111 + 5</td><td>39.39</td><td>773.61 MB</td><td>93.22</td><td>6.43 GB</td></tr><tr><td>5</td><td>72 + 7</td><td>503.52</td><td>4.43 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>5</td><td>59 + 8</td><td>1094.36</td><td>10.33 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>5</td><td>56 + 9</td><td>321.89</td><td>4.22 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr><tr><td>5</td><td>66 + 9</td><td>348.27</td><td>6.68 GB</td><td><strong>OOM</strong></td><td><strong>OOM</strong></td></tr></tbody></table>

Moreover, in many cases our implementation finished execution in a couple of minutes requiring several GBs of memory, while the naive approach runs out of memory.

## 4.2 Using CTL Model Checking for Malware Detection

Using our approach, we implemented a tool for model checking concurrent self-modifying code. Our tool takes as input a binary program and a single indexed CTL formula. The tool translates the given binary into an SM-DPN model. We used ANGR [30] to obtain the assembly code from the binary and then we followed

<table><caption>Table 2: Experimental results of applying our approach to detect malware.</caption><thead><tr><th>Type</th><th>Thread #</th><th># of rules</th><th>T, s</th></tr></thead><tbody><tr><td>Trojan-Proxy.km</td><td>14</td><td>1586</td><td>26.28</td></tr><tr><td>Trojan-Proxy.a</td><td>2</td><td>1564</td><td>0.08</td></tr><tr><td>Trojan-Proxy.b</td><td>5</td><td>375</td><td>5.16</td></tr><tr><td>Trojan-Proxy.bs</td><td>4</td><td>380</td><td>4.75</td></tr><tr><td>Trojan-Proxy.de</td><td>4</td><td>380</td><td>4.75</td></tr><tr><td>Trojan-Proxy.sb</td><td>3</td><td>235</td><td>166.70</td></tr><tr><td>Trojan-Proxy.sf</td><td>3</td><td>235</td><td>161.56</td></tr><tr><td>Trojan-Proxy.cl</td><td>4</td><td>255</td><td>0.67</td></tr><tr><td>Trojan-Proxy.ct</td><td>5</td><td>375</td><td>5.44</td></tr><tr><td>Trojan-Proxy.w</td><td>2</td><td>2131</td><td>2583.28</td></tr><tr><td>Trojan-Proxy.smb</td><td>2</td><td>1747</td><td>1130.35</td></tr><tr><td>Trojan-Proxy.dg</td><td>7</td><td>767</td><td>58.37</td></tr><tr><td>Trojan-Proxy.gen</td><td>5</td><td>390</td><td>5.26</td></tr><tr><td>Trojan-Proxy.e</td><td>5</td><td>490</td><td>10.53</td></tr><tr><td>Trojan-Proxy.di</td><td>7</td><td>771</td><td>111.95</td></tr><tr><td>Trojan-Proxy.dc</td><td>7</td><td>771</td><td>121.85</td></tr><tr><td>Trojan- Downloader.afl</td><td>2</td><td>247</td><td>1.02</td></tr><tr><td>Trojan.j</td><td>3</td><td>21051</td><td>2787.29</td></tr><tr><td>Trojan.ta</td><td>3</td><td>9040</td><td>22.83</td></tr><tr><td>Trojan.tb</td><td>6</td><td>9147</td><td>25.21</td></tr><tr><td>Trojan.tc</td><td>10</td><td>9088</td><td>28.33</td></tr><tr><td>Backdoor.h</td><td>3</td><td>1077</td><td>13.09</td></tr><tr><td>Backdoor.g</td><td>9</td><td>3096</td><td>334.56</td></tr><tr><td>Backdoor.cb</td><td>6</td><td>1043</td><td>85.16</td></tr><tr><td>Backdoor.gy</td><td>8</td><td>4956</td><td>1942.67</td></tr><tr><td>Backdoor.j</td><td>7</td><td>6426</td><td>171.60</td></tr><tr><td>Backdoor.bv</td><td>9</td><td>1090</td><td>366.04</td></tr><tr><td>Backdoor.z</td><td>9</td><td>3824</td><td>595.53</td></tr><tr><td>Yak.a</td><td>32</td><td>2700</td><td>5.74</td></tr><tr><td>Worm.ae</td><td>6</td><td>3207</td><td>10.58</td></tr><tr><td>Worm.cua</td><td>7</td><td>1864</td><td>268.00</td></tr><tr><td>Worm.cra</td><td>7</td><td>6262</td><td>161.88</td></tr><tr><td>Worm.f</td><td>5</td><td>565</td><td>4.61</td></tr><tr><td>Worm.b</td><td>5</td><td>1141</td><td>11.49</td></tr><tr><td>Worm.h</td><td>4</td><td>1538</td><td>27.28</td></tr><tr><td>Worm.g</td><td>10</td><td>2134</td><td>11.18</td></tr></tbody></table>

the same approach as [25, 37] to construct SM-DPNs from the assembly code. Shortly, the control locations of SM-DPDSs are binary addresses and each instruction corresponds to a rule in an SM-DPDS. Instructions that spawn parallel processes correspond to spawning rules, and self-modifying instructions correspond to self-modifying rules in SM-DPDS. After obtaining the SM-DPN, the tool performs model checking of the obtained model against the given CTL formula. Atomic propositions are Windows functions, and each atomic proposition is satisfied when the binary calls the corresponding function. If the formula is satisfied, then the tool returns True, otherwise False.

### 4.2.1 Specifying malicious behaviours using CTL.
We specified malicious behaviours using single indexed CTL formulas. For example, the Trojan behaviour involves injecting the filename of the malware
into the Windows registry (registry key injection) while spawning
the second thread that injects malicious payload into legitimate
processes (code injection). Registry key injection consists in obtain-
ing the filename of the malware and putting the filename into the
registry record that keeps track of the programs launched automat-
ically when the computer turns on. On the other hand, trojans use
code injection to evade anti-virus software by making legitimate
processes execute malicious payloads. Malware writes the mali-
cious code into the process memory of another program. Thus, the
trojan behavior can be described by a single indexed CTL formula
$\psi_{tr} = \psi_{ri}^1 \wedge \psi_{ci}^2$, where $\psi_{ri}$ is a CTL formula specifying the registry
key injection behavior of the first thread, while $\psi_{ci}$ is a CTL formula
specifying the code injection behavior of the second thread. More
precisely, $\psi_{ri} = \mathbf{EF}[\text{GetModuleFilenameA} \wedge \mathbf{EFRegSetValueExA}]$.

This describes that in the future, the program calls function `GetModuleFilenameA` to get the malware's filename. Then, the program calls function `RegSetValueExA` to modify the Windows registry.

And $\psi_{ci} = \mathbf{AG}[\mathbf{EF}[\mathbf{OpenProcess} \wedge \mathbf{EF}(\mathbf{VirtualAllocEx} \wedge \mathbf{EF}\mathbf{WriteProcessMemory})]]$. This formula describes that in the created thread, there is always a loop that obtains a handle to a new process by calling function `OpenProcess`. After that, function `VirtualAllocEx` allocates a block of memory in the new process and the `WriteProcessMemory` function writes some payload into the created block.

We then applied our tool for malware detection. We gathered self-
modifying versions of real malware from public malware databases
such as Malware Bazaar [1] and Virus Share [12]. After that, we
executed our tool, giving it as input the malware samples and single
indexed CTL formulas for malicious behaviours. If the tool returned
True, i.e. if the CTL formula for malicious behaviour is satisfied, we
marked the given binary as malware.

4.2.2 *Results.* We were able to detect several types of malware. The results of our experiments are presented in Table 2. The table shows the type of malware in the **Type** column. The **Thread #** column shows how many different parallel processes can be spawned by the malware, the **# of rules** column shows how many rules are in the largest process, and column **T** shows how long it took to perform model checking.

Our tool successfully detected concurrent and self-modifying
malware by model checking against single-indexed CTL formulas.
For example, the Trojan-Downloader.afl malware with two threads
was detected by checking it over $\psi_{tr}$. To detect this malware, it is
necessary to check both threads and take spawning into account.
Moreover, note that code injection cannot be described by LTL. CTL
is needed to describe this behaviour.

**5 Conclusion**

We present in this paper an efficient approach for CTL model check-
ing concurrent and self-modifying programs. We described a direct
algorithm for model checking Self-Modifying Dynamic Pushdown
Networks. Then, we conducted practical experiments showing that
our direct algorithm is more efficient than the naive approach for
standard DPNs. In particular, our tool was able to detect several
self-modifying concurrent malware.

**References**

[1] abuse.ch. 2025. Malware Bazaar. https://bazaar.abuse.ch/about/.

[2] B. Anckaert, M. Madou, and K. De Bosschere. 2007. A model for self-modifying code. In *Information Hiding 2006*.

[3] K. Apt, F. S De Boer, and E. Olderog. 2010. *Verification of sequential and concurrent programs*. Springer Science & Business Media.

[4] G. Balakrishnan, T. Reps, N. Kidd, et al. 2005. Model checking x86 executables with CodeSurfer/x86 and WPDS++ . In *CAV*.

[5] J. Bergeron, M. Debbabi, J. Desharnais, M. Erhioui, Y. Lavoie, N. Tawbi, et al. 2001. Static detection of malicious code in executable programs. *Req. Eng.*

[6] S. Blazy, V. Laporte, and D. Pichardie. 2016. Verified abstract interpretation techniques for disassembling low-level self-modifying code. *Journal of Automated Reasoning*.

[7] G. Bonfante, J. Marion, and D. Reynaud-Plantey. 2009. A computability perspective on self-modifying programs. In *SEFM*.

[8] A. Bouajjani, J. Esparza, and O. Maler. 1997. Reachability analysis of pushdown automata: application to model-checking. In *Concurrency Theory 1997*.

[9] A. Bouajjani, M. Müller-Olm, and T. Touili. 2005. Regular symbolic analysis of dynamic networks of pushdown systems. In *Concurrency Theory 2005*.

[10] H. Cai, Z. Shao, and A. Vaynberg. 2007. Certified self-modifying code. In *PLDI*.

[11] S. K Coogan, K. P Debray, and G. Townsend. 2008. On the semantics of self-unpacking malware code. *Citeseer, Tech. Rep.*

[12] Corvus Forensics. 2025. Virus Share. https://virusshare.com/about.

[13] J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. 2000. Efficient algorithms for model checking pushdown systems. In *CAV*.

[14] J. Esparza, A. Kučera, and S. Schwoon. 2003. Model checking LTL with regular valuations for pushdown systems. *Information and Computation*.

[15] A. Finkel, B. Willems, and P. Wolper. 1997. A direct symbolic approach to model checking pushdown systems. *Electronic Notes in Theoretical Computer Science*.

[16] G. Holzmann. 2000. Logic verification of ANSI-C code with SPIN. In *SPIN*.

[17] K. Hristova and Y. Liu. 2006. Improved algorithm complexities for linear temporal logic model checking of pushdown systems. In *VMCAL*.

[18] V. Kahlon and A. Gupta. 2006. An automata-theoretic approach for model checking threads for LTL properties. In *LICS'06*.

[19] R. Keller. 1976. Formal verification of parallel programs. *Communications of the ACM*.

[20] N. Kidd, P. Lammich, T. Touili, and T. Reps. 2011. A decision procedure for detecting atomicity violations for communicating processes with locks. *STTT*.

[21] J. Kinder, S. Katzenbeisser, C. Schallhart, and H. Veith. 2005. Detecting malicious code by model checking. In *DIMVA*.

[22] R. Lakenbrink, M. Müller-Olm, C. Ohrem, and J. Gutsfeld. 2023. A navigation logic for recursive programs with dynamic thread creation. In *VMCAL*.

[23] P. Lammich, M. Müller-Olm, and A. Wenner. 2009. Predecessor sets of dynamic pushdown networks with tree-regular constraints. In *CAV*.

[24] L. Lamport. 1999. Specifying concurrent systems with TLA+. *Calculational System Design*.

[25] W. Messahel and T. Touili. 2024. Reachability analysis of concurrent self-modifying code. In *ICECCS*.

[26] H. Nguyen and T. Touili. 2018. CARET analysis of multithreaded programs. In *LOPSTR*.

[27] A. Pommellet and T. Touili. 2020. LTL model checking for communicating concurrent programs. *Innovations in Systems and Software Engineering*.

[28] S. Qadeer and J. Rehof. 2005. Context-bounded model checking of concurrent software. In *TACAS*.

[29] G. Ramalingam. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. *TOPLAS*.

[30] Y. Shoshitaishvili et al. 2016. SoK(state of) the art of war: offensive techniques in binary analysis. In *IEEE Symposium on Security and Privacy*.

[31] P. Singh and A. Lakhotia. 2003. Static verification of worm and virus behavior in binary executables using model checking. In *SMC*.

[32] F. Song and T. Touili. 2012. Efficient malware detection using model-checking. In *International Symposium on Formal Methods*.

[33] F. Song and T. Touili. 2013. LTL model-checking for malware detection. In *TACAS*.

[34] F. Song and T. Touili. 2015. Model checking dynamic pushdown networks. *Formal Aspects of Computing*.

[35] T. Touili and X. Ye. 2022. LTL model checking of self modifying code. *Formal Methods in System Design*.

[36] T. Touili and X. Ye. 2022. SMODIC: a model checker for self-modifying code. In *ARES*.

[37] T. Touili and O. Zhangeldinov. 2025. LTL model checking of concurrent self modifying code. In *ICECCS*.

[38] M. Vardi and P. Wolper. 1984. Automata theoretic techniques for modal logics of programs. In *STOC*.

[39] I. Walukiewicz. 2000. Model checking CTL properties of pushdown systems. In *FSTTCS*.