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

HAL
open science

# How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?

Radu Iosif, Arnaud Sangnier

► To cite this version:

Radu Iosif, Arnaud Sangnier. How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?. 14th International Symposium on Automated Technology for Verification and Analysis, Oct 2016, Chiba, Japan. pp.89-105, 10.1007/978-3-319-46520-3_6. hal-01418881

HAL Id: hal-01418881

https://hal.science/hal-01418881

Submitted on 17 Dec 2016

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.

Public Domain
# How hard is it to verify flat affine counter systems with the finite monoid property ?

Radu Iosif¹ and Arnaud Sangnier²

¹ Verimag, Univ Grenoble Alpes, CNRS

² IRIF, Univ Paris Diderot, CNRS

**Abstract.** We study several decision problems for counter systems with guards defined by convex polyhedra and updates defined by affine transformations. In general, the reachability problem is undecidable for such systems. Decidability can be achieved by imposing two restrictions: (1) the control structure of the counter system is *flat*, meaning that nested loops are forbidden, and (2) the multiplicative monoid generated by the affine update matrices present in the system is finite. We provide complexity bounds for several decision problems of such systems, by proving that reachability and model checking for Past Linear Temporal Logic stands in the second level of the polynomial hierarchy $\Sigma_2^P$, while model checking for First Order Logic is PSPACE-complete.

## 1 Introduction

Counter systems are finite state automata extended with integer variables, also known as counter automata or counter machines. These are Turing-complete models of computation, often used to describe the behavior of complex real-life systems, such as embedded/control hardware and/or software systems. Because many verification problems, of rather complex systems, can be reduced to decision problems for counter systems, it is important to understand the difficulties faced by potential verification algorithms designed to work with the latter.

Due to their succinctness and expressive power, most decision problems, such as reachability, termination and temporal logic model-checking, are undecidable for counter systems, even when the operations on the counters are restricted to increment, decrement and zero-test [24]. This early negative result motivated the search for subclasses with decidable decision problems. Such classes include *one-counter systems* [14], *vector addition systems with states* [22], *reversal-bounded counter machines* [15] and *flat counter systems* [4,12].

Flat counter systems are defined by a natural syntactic restriction, which requires that no state occurs in more than one simple cycle in the control flow graph of the system. Decidability results on the verification of reachability problems for flat counter systems have been obtained by proving that, under certain restrictions on the logic that defines the transition rules, the set of reachable configurations is semilinear and effectively definable in Presburger arithmetic [4,12,6]. Even though flatness is an important restriction (few counter systems
modeling real-life hardware and software artifacts are actually flat), this class
provides the grounds for a useful method that under-approximates the set of be-
haviors of a non-flat counter system by larger and larger sets of paths described
by flat counter systems. This method is currently used by model checking tools,
such as FAST [2] and FLATA [19], and has been applied to improve the results
of static analysis [13], as well as the convergence of counterexample-driven ab-
straction refinement algorithms [17]. Moreover, several works define classes of
flattable counter systems, for which there exist flat unfoldings of the system
with identical reachability sets. Such is the case of timed automata [7] and of
2-dimensional vector addition systems with states [21,3]. For these systems, the
method of under-approximations by flat unfoldings is guaranteed to terminate.

In general, the flatness restriction is shown to reduce the computational com-
plexity of several decision problems, such as reachability or temporal logic model
checking. For instance, in the case of Kripke structures, flatness reduces the com-
plexity of the model-checking of Linear Temporal Logic (LTL) from PSPACE
to NP [20]. When considering flat counter systems whose updates are described
by translations, the complexity of these problems drops from undecidable to
NP-complete [10], while model checking for First Order Logic (FO) is coined to
be PSPACE-complete [8]. For branching time temporal logics, flatness yields
decidable problems, but with less remarkable complexity bounds [9].

In this work, we focus on the model of affine counter systems, in which
each transition is labeled with (i) a guard defined by (a disjunction of) convex
polyhedra, i.e. linear systems of inequalities of the form $C \cdot x \le d$, and (ii) a
deterministic update defined by an affine transformations $f(x) = A \cdot x + b$
where $A, C \in \mathbb{Z}^{n \times n}$ are square matrices with integer entries, $b, d \in \mathbb{Z}^n$ are
vectors of integer constants and $x = [x_1, \dots, x_n]$ is a vector of counters. For
such systems, the set of reachable configurations is semilinear (thus reachability
is decidable), provided that the multiplicative monoid generated by the matrices
used in update functions is finite. This condition is also known as the *finite
monoid property* [4,12]. Moreover, it has been shown that the model-checking
of such systems, for an extended version of the branching time logic CTL* is
decidable, also by reduction to the satisfiability of a Presburger formula, of size
exponential in the size of the counter system [11].

In this work, we show that for flat affine counter systems with the finite
monoid property, reachability and model checking for Past LTL are $\Sigma_2^P$, whereas
model checking for FO is PSPACE-complete. Our result generalizes the results
for flat counter systems with translations [8,10], since these systems are a strict
subclass of flat affine counter systems with the finite monoid property. For in-
stance, a transfer of values between different counters can be done in one step
with an affine counter system, whereas a translating counter system would need
a cycle to implement such operations. Our proof technique is based on an anal-
ysis of the behavior of the sequence of matrix powers in a finite multiplicative
monoid, and adapts several techniques for translating counter systems to this
more general case.

Due to lack of space, omitted proofs can be found in [18].
## 2 Counter Systems and their Decision Problems

We denote by $\mathbb{N}$ and $\mathbb{Z}$ the sets of natural and integer numbers, respectively. We write $[\ell, u]$ for the integer interval $\{\ell, \ell+1, \dots, u\}$, where $\ell \le u$, and $\text{abs}(n)$ for the absolute value of the integer $n \in \mathbb{Z}$. The cardinality of a finite set $S$ is denoted by $\|S\|$.

We denote by $\mathbb{Z}^{n \times m}$ the set of matrices with $n$ rows and $m$ columns, where $\mathbf{A}[i]$ is the $i$-th column and $\mathbf{A}[i][j]$ is the entry on the $i$-th row and $j$-th column of $\mathbf{A} \in \mathbb{Z}^{n \times m}$, for each $i \in [1, n]$ and $j \in [1, m]$. If $n = m$, we call this number the dimension of $\mathbf{A}$, and we denote by $\mathbf{I}_n$ the identity matrix in $\mathbb{Z}^{n \times n}$. For $\mathbf{A} \in \mathbb{Z}^{n \times m}$ and $\mathbf{B} \in \mathbb{Z}^{m \times p}$, we denote by $\mathbf{A} \cdot \mathbf{B} \in \mathbb{Z}^{n \times p}$ the matrix product of $\mathbf{A}$ and $\mathbf{B}$. For a matrix $\mathbf{A} \in \mathbb{Z}^{n \times n}$, we define $\mathbf{A}^0 = \mathbf{I}_n$ and $\mathbf{A}^i = \mathbf{A}^{i-1} \cdot \mathbf{A}$, for all $i > 0$.

We write $\mathbb{Z}^n$ for $\mathbb{Z}^{n \times 1}$ in the following. Each $\mathbf{v} \in \mathbb{Z}^n$ is a column vector, where $\mathbf{v}[i]$ is the entry on its $i$-th row. For a vector $\mathbf{x}$ of variables of length $n$ and a matrix $\mathbf{A} \in \mathbb{Z}^{m \times n}$, the product $\mathbf{A} \cdot \mathbf{x}$ is the vector of terms $(\mathbf{A} \cdot \mathbf{x})[i] = \sum_{j=1}^n \mathbf{A}[i][j] \cdot \mathbf{x}[j]$, for all $i \in [1, m]$. A row vector is denoted by $\mathbf{v} = [v_1, \dots, v_n] \in \mathbb{Z}^{1 \times n}$. For a row vector $\mathbf{v}$, we denote its transpose by $\mathbf{v}^\top$.

For a vector $\mathbf{v} \in \mathbb{Z}^n$, we consider the standard infinity $\|\mathbf{v}\|_\infty = \max_{i=1}^n \text{abs}(\mathbf{v}[i])$ norm. Given $\mathbf{A} \in \mathbb{Z}^{m \times n}$, consider the induced $\|\mathbf{A}\|_\infty = \max_{i=1}^m \sum_{j=1}^n \text{abs}(\mathbf{A}[i][j])$, and the maximum $\|\mathbf{A}\|_{\max} = \max_{i=1}^m \max_{j=1}^n \text{abs}(\mathbf{A}[i][j])$ norms. The size of a matrix is $\text{size}(\mathbf{A}) = \sum_{i=1}^m \sum_{j=1}^n \log_2(\mathbf{A}[i][j]+1)$, with integers encoded in binary.

### 2.1 Counter systems

Let $X_n = \{x_1, x_2, \dots, x_n\}$ be a finite set of integer variables, called *counters*, $\mathbf{x}$ be the vector such that $\mathbf{x}[i] = x_i$, for all $i \in [1, n]$, and $\text{AP} = \{\text{a}, \text{b}, \text{c}, \dots\}$ be a countable set of boolean *atomic propositions*. A *guard* is either true, denoted by $\top$, or a disjunction of systems of inequalities, denoted by $\bigvee_{i=1}^k C_i \cdot \mathbf{x} \le \mathbf{d}_i$ where $C_i \in \mathbb{Z}^{m \times n}$ and $\mathbf{d}_i \in \mathbb{Z}^m$ for all $i \in [1, k]$. A guard is said to be without disjunction if it is either true or it consists of a single system of inequalities.

An integer vector $\mathbf{v} \in \mathbb{Z}^n$ satisfies the guard $\mathbf{g}$, written $\mathbf{v} \models \mathbf{g}$, if either (i) $\mathbf{g} := \top$, or (ii) $\mathbf{g} := \bigvee_{i=1}^k C_i \cdot \mathbf{x} \le \mathbf{d}_i$ and $\mathbf{v}$ is a solution of a system $C_i \cdot \mathbf{x} \le \mathbf{d}_i$, for some $i \in [1, k]$. The set of guards using $X_n$ is denoted by $\text{CG}(X_n)$. An *affine function* $f: \mathbb{Z}^n \to \mathbb{Z}^n$ is a pair $(\mathbf{A}, \mathbf{b}) \in \mathbb{Z}^{n \times n} \times \mathbb{Z}^n$. Given a vector $\mathbf{v} \in \mathbb{Z}^n$, the result of the function $f = (\mathbf{A}, \mathbf{b})$ applied to $\mathbf{v}$ is $f(\mathbf{v}) = \mathbf{A} \cdot \mathbf{v} + \mathbf{b}$. We denote by $\text{Aff}_n$ the set of affine functions over $\mathbb{Z}^n$. An affine function $(\mathbf{A}, \mathbf{b})$ where $\mathbf{A} = \mathbf{I}_n$ is called a *translation*.

**Definition 1.** [*Affine Counter System*] For an integer $n \ge 0$, an affine counter system of dimension $n$ (shortly a *counter system*) is a tuple $S = (\langle Q, X_n, \Delta, \Lambda \rangle)$, where: (i) $Q$ is a finite set of control states, (ii) $\Lambda: Q \to 2^{\text{AP}}$ is a labeling function, and (iii) $\Delta \subseteq Q \times \text{CG}(X_n) \times \text{Aff}_n \times Q$ is a finite set of transition rules labeled by guards and affine functions (updates).

A counter system is said to be *disjunction free* if all its guards are without disjunction. For a transition rule $\delta = (q, g, f, q') \in \Delta$, we use the notations
$source(\delta) = q$, $guard(\delta) = g$, $update(\delta) = f$ and $target(\delta) = q'$. A path $\pi$ of $S$ is a non-empty sequence of transition rules $\delta_1 \dots \delta_m$ such that $source(\delta_{i+1}) = target(\delta_i)$ for all $i \in [1, m-1]$. The path $\pi$ is a simple cycle if $\delta_1 \dots \delta_m$ are pairwise distinct and $source(\delta_1) = target(\delta_m)$. In this case, we denote $source(\pi) = target(\pi) = source(\delta_1)$. A counter system $S$ is flat if for each control state $q \in Q$ there exists at most one simple cycle $\pi$ such that $source(\pi) = q$. In such a system any path leaving a simple cycle cannot revisit it.

**Example 1.** Figure 1 shows a flat counter system whose control states $q_0, q_1, q_2, q_3$ are labeled by the atomic propositions **a**, **b**, **c**, **d**, respectively. From the initial state $q_0$ with all counters equal to 0, this system begins with incrementing $x_1$ a certain number of times by a transition $\delta_0$ then, with $\delta_1$, it transfers the value of the counter $x_1$ to $x_3$ and resets $x_1$; the loop labeled by $\delta_2$ increments both $x_1$ and $x_2$ until they both reach the value of $x_3$ and finally the loop labeled by $\delta_4$ is used to decrement $x_2$ and increment $x_1$ until the value of $x_1$ is twice the value of $x_3$. As a consequence, when the system reaches $q_3$ the value of $x_1$ is twice the value of $x_3$ and the value of $x_2$ is equal to 0. Hence, any run reaching $q_3$ visits the state $q_1$ exactly the same number of times as the state $q_2$. ■

<figure><img src="image_2.png" /><figcaption>**Fig. 1.** A flat affine counter system</figcaption></figure>

The size of a counter system $S$ is $size(S) = \sum_{\delta \in \Delta} size(\delta) + \sum_{q \in Q} \|\Lambda(q)\|$, where $size(\delta) = 1 + size(guard(\delta)) + size/update(\delta)$, for a guard $g := \bigvee_{i=1}^k C_i$. $x \le d_i$ we have $size(g) = \sum_{i=1}^k size(C_i) + size(d_i)$, and for an update $f = (A, b)$, $size(f) = size(A) + size(b)$.

A counter system of dimension $n = 0$ is called a *Kripke structure*. We denote by $KS$ and $KS_f$ the sets of Kripke structures and flat Kripke structures, respectively. A counter system of dimension $n \ge 1$ is *translating* if all updates labeling the transition rules are pairs $(I_n, b)$. Let $TS$ and $TS_f$ denote the sets of translating and flat translating counter systems of any dimension $n \ge 1$.

For a counter system $S$ of dimension $n \ge 1$, we consider $M_S \subseteq \mathbb{Z}^{n \times n}$ to be the smallest set of matrices, closed under product, which contains $I_n$ and each matrix $A$ occurring in an update $(A, b)$ of a transition rule in $S$. Clearly, $M_S$ forms a monoid with the matrix product and identity $I_n$. We say that $S$ has the
finite monoid property if the set $\mathcal{M}_S$ is finite. Let $\mathbf{AS}_{\text{fm}}$ be the set of flat counter systems with the finite monoid property and $\mathbf{AS}_{\text{fm}}^{\text{df}}$ its restriction to disjunction free systems. These latter classes are the main focus of this paper.

A configuration of the counter system $S = \langle Q, \mathcal{X}_n, \Delta, \Lambda \rangle$ is a pair $(q, v) \in Q \times \mathbb{Z}^n$, where $q$ is the current control state and $v[i]$ is the value of the counter $x_i$, for all $i \in [1, n]$. Given two configurations $\gamma = (q, v)$ and $\gamma' = (q', v')$ and a transition rule $\delta$, we write $\gamma \xrightarrow{\delta} \gamma'$ iff $q = \text{source}(\delta)$, $q' = \text{target}(\delta)$, $v = \text{guard}(\delta)$ and $v' = \text{update}(\delta)(v)$. We use the notation $\gamma \to \gamma'$ when there exists a transition rule $\delta$ such that $\gamma \xrightarrow{\delta} \gamma'$. A run of $S$ is then an infinite sequence of the form $\rho: \gamma_0 \xrightarrow{\delta_0} \gamma_1 \xrightarrow{\delta_1} \gamma_2 \xrightarrow{\delta_2} \dots$. We say that such a run starts at configuration $\gamma_0$, furthermore we denote by $\text{trans}(\rho) = \delta_0\delta_1\delta_2\dots$ the infinite sequence of transition rules seen during $\rho$. Without loss of generality we consider deadlock-free counter systems only, where for each configuration $\gamma \in Q \times \mathbb{Z}^n$, there exists a configuration $\gamma'$ such that $\gamma \to \gamma'^3$.

*Example 2.* The sequence below is a run of the counter system from Figure 1:

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

## 2.2 Decision Problems

The reachability problem for a class of counter systems $\mathcal{C}$, denoted by $\text{REACH}(\mathcal{C})$, can then be stated as follows: given a counter system $S$ in $\mathcal{C}$, an initial configuration $\gamma_0$, and a control state $q_f$, does $S$ have a run starting in $\gamma_0$ and containing a configuration $(q_f, v)$, for some $v \in \mathbb{Z}^n$? It is well known that $\text{REACH}(\text{TS})$ is undecidable for non-flat counter systems, even for only 2 counters with zero test guards, and increment/decrement updates [24].

In this work we also consider model checking problems for two specification logics, namely Past Linear Temporal Logic (PLTL) and First Order Logic (FO). The formulae of PLTL are defined by the grammar: $\phi ::= p | \neg\phi | \phi \land \phi | X\phi | \phi U\phi | X^{-1}\phi | \phi S\phi$, where $p \in \text{AP}$. As usual, we consider the derived modal operators $F\phi := \top U\phi$ and $G\phi := \neg F\neg\phi$. Given a run $\rho: \gamma_0 \xrightarrow{\delta_0} \gamma_1 \xrightarrow{\delta_1} \gamma_2 \xrightarrow{\delta_2} \dots$ of a counter system $S$ and a PLTL formula $\phi$, the semantics of PLTL is defined by an inductive forcing relation $\rho, i \models_{\text{PLTL}} \phi$, where for all $i \ge 0: \rho, i \models_{\text{PLTL}} p \Leftrightarrow$

<footnote n="3">³ We ensure deadlock-freedom by adding a sink state $\sigma$ to $S$, with a self-loop $\sigma \xrightarrow{\top} \sigma$, and a transition $q \xrightarrow{\sigma} \sigma$ from each state $q \in Q$.</footnote>
$\gamma_i = (q, v)$ and $p \in \mathcal{A}(q)$; $\rho, i \models_{\text{PLTL}} X\phi \Leftrightarrow \rho, i+1 \models_{\text{PLTL}} \phi$; $\rho, i \models_{\text{PLTL}} \phi U\psi \Leftrightarrow \rho, j \models_{\text{PLTL}} \psi$ for some $j \ge i$ and $\rho, k \models_{\text{PLTL}} \phi$ for all $i \le k < j$; $\rho, i \models_{\text{PLTL}} X^{-1}\phi \Leftrightarrow i > 0$ and $\rho, i-1 \models_{\text{PLTL}} \phi$; $\rho, i \models_{\text{PLTL}} \phi S\psi \Leftrightarrow \rho, j \models_{\text{PLTL}} \psi$ for some $0 \le j \le i$ and $\rho, k \models_{\text{PLTL}} \phi$ for all $j < k \le i$. The semantics of the boolean connectives $\wedge$ and $\neg$ is the usual one. We write $\rho \models_{\text{PLTL}} \phi$ for $\rho, 0 \models_{\text{PLTL}} \phi$. For instance, each run of the counter system from Figure 1 satisfies $G((b \wedge Xb \wedge Fd) \rightarrow F(c \wedge Xc))$, because each run visiting $q_3$ sees the same number of b's and c's.

The formulae of FO are defined by the grammar: $\phi ::= p(z) \mid z < z' \mid \neg\phi \mid \phi \wedge \phi \mid \exists z.\phi$, where $p \in \mathcal{AP}$ and $z$ belongs to a countable set of *logical variables* $\mathcal{Var}$. The semantics is given by a forcing relation $\rho \models_{\mathcal{FO}} \phi$ between runs $\rho$ of $S$ and closed formulae $\phi$, with no free variables, which interprets the quantified variables $z \in \mathcal{Var}$ as positive integers denoting positions in the run. With this convention, the semantics of FO is standard. For instance, each run of the counter system from Figure 1 satisfies the FO property: $\forall x\forall x'.(x < x' \wedge b(x) \wedge b(x') \wedge \exists z.d(z)) \rightarrow \exists y\exists y'.c(y) \wedge c(y')$, which differs from the previous PLTL formula only in that $x$ and $x'$ ($y$ and $y'$) are not necessarily consecutive moments in time. For both of these logics, we consider the size of a formula as its number of subformulae.

The model-checking problem for counter systems in a class $\mathcal{C}$ with specification language $\mathcal{L}$ (in this work either PLTL or FO), denoted by $\text{MC}_{\mathcal{L}}(\mathcal{C})$, is defined as follows: given a counter system $S$ in $\mathcal{C}$, an initial configuration $\gamma_0$, and a formula $\phi$ of $\mathcal{L}$, does there exist a run $\rho$ of $S$ starting in $\gamma_0$ such that $\rho \models_{\mathcal{L}} \phi$.

<table><caption>**Table 1.** Known results</caption><thead><tr><th></th><th>KS</th><th>KS<sub>f</sub></th><th>TS</th><th>TS<sub>f</sub></th><th>AS<sub>fm</sub></th></tr></thead><tbody><tr><td>REACH</td><td>NLOGSPACE</td><td>NLOGSPACE</td><td>Undec. [24]</td><td>NP-c. [10]</td><td>4EXPTIME [12]</td></tr><tr><td>MC<sub>PLTL</sub></td><td>PSPACE-c. [25]</td><td>NP-c. [10,20]</td><td>Undec.</td><td>NP-c. [10]</td><td>4EXPTIME [11]</td></tr><tr><td>MC<sub>FO</sub></td><td>NONELEM. [26]</td><td>PSPACE-c. [8]</td><td>Undec.</td><td>PSPACE-c. [8]</td><td>Decid. [11]</td></tr></tbody></table>

Table 1 gives an overview of the known complexity bounds for the previously mentioned decision problems looking at different classes of counter systems. For flat Kripke structures, it is proved in [10,20] that $\text{MC}_{\text{PLTL}}(\text{KS}_f)$ is NP-complete and in [8] that $\text{MC}_{\text{FO}}(\text{KS}_f)$ is PSPACE-complete, whereas $\text{MC}_{\text{PLTL}}(\text{KS})$ is PSPACE-complete and $\text{MC}_{\text{FO}}(\text{KS})$ is non-elementary. As explained in [8,10], the complexity of these two last problems does not change if one considers flat translating counter systems. For what concerns flat counter systems with the finite monoid property, it has been shown that one can compute a Presburger formula which characterizes the reachability set, which entails the decidability of $\text{REACH}(\text{AS}_{\text{fm}})$ [12]. Later on, in [11], the authors have shown that the model-checking of an extension of the branching time logic CTL* is decidable. Hence we know that $\text{MC}_{\text{PLTL}}(\text{AS}_{\text{fm}})$ and $\text{MC}_{\text{FO}}(\text{AS}_{\text{fm}})$ are decidable, however no precise complexity for these problems is known. We only can deduce from the proofs in [12,5,11] that for $\text{REACH}(\text{AS}_{\text{fm}})$ and $\text{MC}_{\text{PLTL}}(\text{AS}_{\text{fm}})$ there exists a reduction to the satisfiability problem for Presburger arithmetic where the built formula is
exponentially bigger than the size of the model, this leads to an upper bound
in 4EXPTIME (the satisfiability problem for Presburger arithmetic can in fact
be solved in 3EXPTIME, see e.g. [16]).

In this work, we aim at improving the complexity for the problems related
to affine counter systems with the finite monoid property. Note that for the pre-
sented results, the counter systems were manipulating natural numbers instead
of integers, but considering the latter option does not change the stated results.

3 A Hardness Result

In this section we prove that the reachability problem for flat affine counter
systems with the finite monoid property is $\Sigma_2^P$-hard, by reduction from the va-
lidity problem for the $\exists^*\forall^*$ fragment of quantified boolean formulae ($\Sigma_2$-QBF),
which is a well-known $\Sigma_2^P$-complete problem [1, §5.2]. Let us consider a formula
$\Phi := \exists y_1 \dots \exists y_p \forall z_1 \dots \forall z_q . \Psi(y, z)$, where $y = \{y_1, \dots, y_p\}$ and $z = \{z_1, \dots, z_q\}$
are non-empty sets of boolean variables, and $\Psi$ is a quantifier-free boolean for-
mula. We shall build, in polynomial time, a flat counter system $S_\Phi$, with the
finite monoid property, such that $\Phi$ is valid if and only if $S_\Phi$ has a run reaching
$q_f$ which starts in $(q_0, v_0)$ for a certain valuation $v_0$ of its counters.

<figure><img src="image_4.png" /><figcaption>Fig. 2. The counter system $S_{\Phi}$ corresponding to the $
\Sigma_2$-QBF $\Phi$</figcaption></figure>

Let $\pi_n$ denote the $n$-th prime number, i.e. $\pi_1 = 2, \pi_2 = 3, \pi_3 = 5$, etc.
Formally, $S_{\Phi} = \langle Q, X_N, \Delta, \Lambda \rangle$, where $Q = \{q_0, \dots, q_p, q, q_f\}$, $N = p + \sum_{n=1}^q \pi_n$, and $\Lambda$ is the function associating to each state an empty set of propositions. We recall that $\pi_n$ is a polynomial in the size of $n$, hence $N$ is as well polynomial in the size of $n$. The transition rules $\Delta$ are depicted in Figure 2. Intuitively, each existentially quantified boolean variable $y_i$ of $\Phi$ is modeled by the counter $x_i$ in $S_{\Phi}$, each universally quantified variable $z_j$ of $\Phi$ is modeled by the counter $x_{p+\sum_{n=1}^j \pi_n}$, and the rest are working counters. All counters range over the set $\{0, 1\}$, with the obvious meaning (0 stands for false and 1 for true).

The counter system $S_{\Phi}$ works in two phases. The first phase, corresponding
to transitions $q_0 \rightarrow \dots \rightarrow q_p$, initializes the counters $x_1, \dots, x_p$ to some values
from the set $\{0, 1\}$, thus mimicking a choice of boolean values for the existentially
quantified variables $y_1, \dots, y_p$ from $\Phi$. Here $I_N \in \mathbb{Z}^{N \times N}$ is the identity matrix,
and $e_i \in \{0, 1\}^N$ is the unit vector such that $e_i[j] = 0$ if $j \neq i$ and $e_i[i] = 1$.

The second phase checks that $\Phi$ is valid for each choice of $z_1, \dots, z_q$. This
is done by the cycle $q \to q$, which explores all combinations of 0's and 1's for
the counters $x_{p+\sum_{n=1}^j \pi_n}$, corresponding to $z_j$, for all $j \in [1, q]$. To this end, we use the permutation matrix $\mathbf{M}$, which consists of $\mathbf{I}_p$ and $q$ rotation blocks $\mathbf{M}_{\pi_j} \in \{0, 1\}^{\pi_j \times \pi_j}$ (Figure 3). The valuation $v_0$ ensures that the initial value of $x_{p+\sum_{n=1}^j \pi_n}$ is 1, for all $j \in [1, q]$, the other counters being 0 initially (Figure 3).

<figure><img src="image_5.png" /><figcaption>Fig. 3. Matrix $\mathbf{M}$ and initial vector $\mathbf{v}_0$</figcaption></figure>

Intuitively, after $n$ iterations of the affine function $(\mathbf{M}, \mathbf{0})$, labeling the cycle $q \to q$ in $S_\Phi$, we have $x_{p+\sum_{n=1}^j \pi_n} = 1$ iff $n$ is a multiple of $\pi_j$. This fact guarantees that all combinations of 0's and 1's for $z_1, \dots, z_q$ have been visited in $\Pi_{j=1}^q \pi_j$ iterations of the cycle. The guard $g_1$, labeling the cycle, tests that, at each iteration, the formula $\Psi$ is satisfied, using a standard encoding of the formula $\tilde{\Psi}$. Namely, each variable $y_i$ is encoded as the term $x_i \ge 1$ and each $z_j$ is encoded as $x_{p+\sum_{n=1}^j \pi_n} \ge 1$.

For instance, the formula $y_1 \lor \neg z_2$ is encoded as $x_1 \ge 1 \lor \neg(x_{p+\pi_1+\pi_2} \ge 1))$ which is equivalent to $x_1 \ge 1 \lor x_{p+\pi_1+\pi_2} < 1$. Finally, the guard $g_2$ simply checks that $x_{\pi_1} = \dots = x_{\pi_1+\dots+\pi_q} = 1$, ensuring that the loop has been iterated sufficiently many times. This allows us to deduce the following result.

**Lemma 1.** $\text{REACH}(\text{AS}_{\text{fm}})$ is $\sum_2^P$-hard.

# 4 Bounding the Number of Cycle Iterations

In this section we prove a crucial property of counter systems from the $\text{AS}_{\text{fm}}^{\text{df}}$ class, namely that there exists a polynomial function $\text{Poly}(x)$ such that, for each run $\rho$ starting at $\gamma_0$ of the considered counter system, there exists another run $\rho'$ starting at $\gamma_0$, using the same transition rules as $\rho$, in exactly the same order, and which iterates each simple cycle at most $2^{\text{Poly}(size(S)+size(\gamma_0))}$ times.

In the rest of this section, we fix a flat disjunction free affine counter system $S = \langle Q, X_n, \Delta, \Lambda \rangle$ with the finite monoid property. We recall here that the set of
runs of a flat counter system can be captured by a finite (though exponential)
number of *path schemas* [8]. Formally, a path schema is a non-empty finite
sequence $P := u_1 \dots u_N$, where $u_i$ is either a transition rule from $\Delta$ or a simple
cycle, such that (i) $u_1, \dots, u_N$ are pairwise distinct, (ii) $u_N$ is a simple cycle,
called *terminal*, and (iii) $\text{target}(u_i) = \text{source}(u_{i+1})$, for all $i \in [1, N-1]$. All
simple cycles on $P$, except for $u_N$, are called *nonterminal*. We use then the
following notations: $\text{len}(P)$ for $N$, $P[i]$ for $u_i$ with $i \in [1, N]$, and $\text{size}(P)$ is the
sum of the sizes of all transition rules occurring in $P$.

Intuitively a path schema *P* represents a set of infinite paths obtained by iter-
ating the non-terminal cycles a certain number of times. We can hence represent
such a path by an associated path schema and an iteration vector. Formally,
an *iterated path schema* is a pair ⟨*P*, *m*⟩, such that *P* is a path schema, and
*m* ∈ N^[len(*P*)-1] is a vector, where for all *i* ∈ [1, len(*P*) - 1], *m*[*i*] ≥ 1 and
*m*[*i*] > 1 implies that *P*[*i*] is a cycle. An iterated path schema defines a unique
infinite word over Δ, denoted by *trans*(*P*, *m*) = *P*[1]^m[P*[2]^m[2] ... P[len(*P*)-1]^m[len(*P*)-1]*P[len(*P*)]]^ω. We recall the following result:

**Lemma 2.** [10] Let $S$ be a flat affine counter system. Then:

1. the length and the size of a path schema of S are polynomial in size(S);

2. for any run $\rho$ of $S$, there exists an iterated path schema $\langle P, m \rangle$ such that $\text{trans}(\rho) = \text{trans}(P, m)$.

For a run $\rho$, we consider the set $ips(\rho) = \{\langle P, m \rangle \mid \text{trans}(\rho) = \text{trans}(P, m)\}$.
Observe that $ips(\rho) \neq \emptyset$ for any run $\rho$ of $S$, due to Lemma 2 (2). Moreover, as a
consequence of Lemma 2 (1), the number of path schemas is bounded by a simple
exponential in the size of $S$. Note that $ips(\rho)$ is not necessarily a singleton: if a
run enters and exits a loop in different states then, in the path schema, the loop
may begin either from the entering state or from the exiting state.

We fix a run $\rho$ of $S$ starting at $\gamma_0$, and $\langle P, m \rangle \in ips(\rho)$ an iterated path schema corresponding to $\rho$. We consider a simple cycle $c = \delta_0 \dots \delta_{k-1}$ of $P$, whose transition rules are $\delta_i = \langle q_i, C_i \cdot x \le d_i, (A_i, b_i), q_{i+1} \rangle$, for all $i \in [0, k-1]$, and $q_k = q_0$. Let $f_c = (A_c, b_c)$ be the update of the entire cycle $c$, where $A_c = A_{k-1} \dots A_1 \cdot A_0$, denoted $\prod_{i=k-1}^{0} A_i$, and $b_c = \sum_{i=0}^{k-1} \prod_{j=k-1}^{i+1} A_j \cdot b_i$. Since $S$ has the finite monoid property, the set $M_c = \{A_c^i | i \in \mathbb{N}\}$ is finite. Then there exist two integer constants $\alpha, \beta \in \mathbb{N}$, such that $0 \le \alpha + \beta \le \|M_c\| + 1$, and $A_c^\alpha = A_c^{\alpha+\beta}$. Observe that, in this case, we have $M_c = \{A_c^0, \dots, A_c^\alpha, \dots, A_c^{\alpha+\beta-1}\}$.

Our goal is to exhibit another run $\rho'$ of $S$ and an iterated path schema
$\langle P, m' \rangle \in ips(\rho')$, such that $\|m'\|_{\infty} \le 2^{\text{Poly}(size(S)+size(\gamma_0))}$, for a polynomial
function $\text{Poly}(x)$. Because $c = \delta_0 \dots \delta_{k-1}$ is a simple cycle of $P$ and $\langle P, m \rangle \in
ips(\rho)$, there exists a (possibly infinite) contiguous subsequence of $\rho$, let us call
it $\theta = (q_0, v_0) \xrightarrow{\tau_0} (q_1, v_1) \xrightarrow{\tau_1} \dots$ that iterates $c$, i.e. $\tau_i = \delta_{(i \bmod k)}$, for all $i \ge 0$.
In the following, we call any subsequence of a run an *execution*.

The main intuition now is that $\theta$ can be decomposed into a prefix of length
$(\alpha + \beta)k$ and $k$ infinite sequences of translations along some effectively com-
putable vectors $w_0, \dots, w_{k-1}$. More precisely, all valuations $v_i$ of $\theta$, for $i \ge$
$(\alpha + \beta)k$, that are situated at distance $\beta k$ one from another, differ by exactly the same vector. We refer to Figure 4 for an illustration of this idea.

<figure><img src="image_6.png" /><figcaption>Fig. 4. Behavior of an execution which iterates $\alpha + 3\beta$ times the cycle $c = \delta_0 \dots \delta_{k-1}$</figcaption></figure>

**Lemma 3.** Given an execution $(q_0, v_0) \xrightarrow{\delta_0} \dots \xrightarrow{\delta_{k-1}} (q_k, v_k) \xrightarrow{\delta_0} \dots$ of $S$ that iterates a simple cycle $c = \delta_0 \dots \delta_{k-1}$, there exist $w_0, \dots, w_{k-1} \in \mathbb{Z}^n$, such that $v_{(\alpha+p\beta+r)k+q} = v_{(\alpha+r)k+q} + p \cdot w_q$, for all $p \ge 0$, $r \in [0, \beta-1]$ and $q \in [0, k-1]$, where $f_c = (A_c, b_c)$ is the update of $c$ and $\alpha, \beta \ge 0$ are such that $A_c^\alpha = A_c^{\alpha+\beta}$.

We distinguish now the case when $c$ is a nonterminal cycle of $P$, iterated finitely many times, from the case when $c$ is terminal, thus iterated ad infinitum. We consider first the case when $c$ is a nonterminal cycle, taken a finite number of times. Viewing the sequence of counter valuations, that occur during the unfolding of a simple loop, as a set of translations by vectors $w_0, \dots, w_{k-1}$, prefixed by an initial sequence, allows us to reduce the problem of checking the validity of the guards along this sequence to checking the guards only in the beginning and in the end of each translation by $w_q$, for $q \in [0, k-1]$. This is possible because the counter systems is disjunction free and hence each guard in the loop is defined by a convex vector set $\{v \in \mathbb{Z}^n | C \cdot v \le d\}$, for a matrix $C \in \mathbb{Z}^{m \times n}$ and a vector $d \in \mathbb{Z}^m$, thus a sequence of vectors produced by a
translation cannot exit and then re-enter the same guard, later on. This crucial
observation, needed to prove the upper bound, is formalized below.

We consider the relaxed transition relation $\rightsquigarrow \subseteq (Q \times \mathbb{Z}^n) \times \Delta \times (Q \times \mathbb{Z}^n)$,
defined as $(q, \mathbf{v}) \rightsquigarrow (q', \mathbf{v}')$ iff $\text{source}(\delta) = q, \mathbf{v}' = \text{update}(\delta)(\mathbf{v})$ and $\text{target}(\delta) = q'$. Hence, $\rightsquigarrow$ allows to move from one configuration to another as in $\rightarrow$, but
without testing the guards. In the following, we fix a sequence of configurations
$\theta' = (q_0, \mathbf{v}_0) \stackrel{\tau_0}{\rightsquigarrow} (q_1, \mathbf{v}_1) \stackrel{\tau_1}{\rightsquigarrow} \dots$ called a *pseudo-execution*. We assume, moreover,
that $\theta'$ iterates the simple cycle $c = \delta_0, \dots, \delta_{k-1}$ a finite number of times, i.e.
$\tau_i := \delta_i \bmod k$, for all $i \ge 0$. To check whether $\theta'$ is a real execution, it is enough
to check the guards in the first $\alpha + \beta + 1$ and the last $\beta$ iterations of the cycle,
as shown by the following lemma:

**Lemma 4.** For any $m > (\alpha+\beta+1)k$, given a finite pseudo-execution $(q_0, \mathbf{v}_0) \rightsquigarrow \dots \rightsquigarrow (q_m, \mathbf{v}_m)$ of $S$, that iterates a nonterminal simple cycle $c = \delta_0 \dots \delta_{k-1}$, $(q_0, \mathbf{v}_0) \xrightarrow{\tau_0} \dots \xrightarrow{\tau_{m-1}} (q_m, \mathbf{v}_m)$ is an execution of $S$ iff $\mathbf{v}_i \models \text{guard}(\tau_i)$, for all $i \in [0, (\alpha + \beta + 1)k - 1] \cup [m - \beta k, m - 1]$.

The next step is to show that if a cycle is iterated $\ell$ times with $\ell = \alpha + \beta + p\beta + r$ for some $p > 0$ and $r \in [0, \beta - 1]$, starting with values $\mathbf{v} \in \mathbb{Z}^n$, then $[\mathbf{v}[1], \dots, \mathbf{v}[n], p]^\top$ is the solution of a system of inequations $\mathbf{M}_c \cdot [\mathbf{y}; z]^\top \le \mathbf{n}_c$, where $[\mathbf{y}; z] = [y_1, \dots, y_n, z]$ is a vector of $n + 1$ variables. The bound on the number of iterations follows from the theorem below, by proving that the sizes of the entries of $\mathbf{M}_c$ and $\mathbf{n}_c$ (in binary) are bounded by a polynomial in $\text{size}(S)$.

**Theorem 1.** Given $\mathbf{A} \in \mathbb{Z}^{m \times n}$ and $\mathbf{b} \in \mathbb{Z}^m$, for $n \ge 2$, the system $\mathbf{A} \cdot \mathbf{x} \le \mathbf{b}$ has a solution in $\mathbb{N}^n$ iff it has a solution such that $\|\mathbf{x}\|_{\infty} \le m^{2n} \cdot \|\mathbf{A}\|_{\max}^n \cdot \|\mathbf{b}\|_{\infty}$.

We recall that $c = \delta_0, \dots, \delta_{k-1}$, where $\text{guard}(\delta_i) := \mathbf{C}_i \cdot \mathbf{x} \le \mathbf{d}_i$, $\text{update}(\delta_i) := (\mathbf{A}_i, \mathbf{b}_i)$, and that $f_c = (\mathbf{A}_c, \mathbf{b}_c)$ is the affine function defining the update of the entire cycle. For any $j > 0$, we define $\mathbf{b}_c^j = \sum_{i=0}^{j-1} \mathbf{A}_c^i \cdot \mathbf{b}_c$, hence $f_c^\ell = (\mathbf{A}_c^\ell, \mathbf{b}_c^\ell)$ is the update corresponding to $\ell$ iterations of the cycle for a fixed integer constant $\ell > 0$. The following set of inequalities expresses the fact that all guards are satisfied within the $\ell$-th iteration of the cycle starting at $\mathbf{v} \in \mathbb{Z}^n$:

$$
C_p \left( \prod_{i=p-1}^{0} \mathbf{A}_i \cdot (\mathbf{A}_c^{\ell-1} \cdot \mathbf{v} + \mathbf{b}_c^{\ell-1}) + \sum_{i=0}^{p-1} \mathbf{A}_{p-1} \cdots \mathbf{A}_{i+1} \cdot \mathbf{b}_i \right) \le \mathbf{d}_p, \text{ for all } p=0, \dots, k-1
$$

In the sequel, we define $\mathbf{M}_\ell$ as the matrix obtained by vertically stacking the
matrices $\mathbf{C}_j \cdot \prod_{i=j-1}^0 \mathbf{A}_i \cdot \mathbf{A}_c^{\ell-1}$ for $j = 0, \dots, k-1$, with $\mathbf{C}_0 \cdot \mathbf{A}_c^{\ell-1}$ on top. Also,
$\mathbf{n}_\ell$ is the column vector with rows $\mathbf{n}_\ell[j] = \mathbf{d}_j - (\mathbf{C}_j \cdot \prod_{i=j-1}^0 \mathbf{A}_i \cdot \mathbf{b}_c^{\ell-1} + \mathbf{C}_j \cdot (\sum_{i=0}^{j-1} \mathbf{A}_{j-1} \cdots \mathbf{A}_{i+1} \cdot \mathbf{b}_i))$, for $j = 0, \dots, k-1$. For technical reasons that will be
made clear next, we do not need to consider the case when the loop is iterated
less than $\alpha + 2\beta + 1$ times. We know, from Lemma 4, that checking whether a
given cycle $c$ can be iterated $\ell > \alpha + 2\beta + 1$ times from $\mathbf{v}$, reduces to checking
the validity of the guards during the first $\alpha+\beta+1$ and the last $\beta$ iterations only.
This condition is encoded by the union of the linear inequality systems below:

$$ \begin{bmatrix} M_1 \\ \vdots \\ M_{\alpha+\beta+1} \end{bmatrix} \cdot \mathbf{v} \le \begin{bmatrix} n_1 \\ \vdots \\ n_{\alpha+\beta+1} \end{bmatrix} \qquad \begin{bmatrix} M_1 \\ \vdots \\ \dot{M}_\beta \end{bmatrix} \cdot f_c^{\ell-\beta}(\mathbf{v}) \le \begin{bmatrix} n_1 \\ \vdots \\ n_\beta \end{bmatrix} $$

Since we assumed that $\ell > \alpha+2\beta+1$, it follows that $\ell-\beta = \alpha+p\beta+r$ for some $p>0$ and $r \in [0, \beta-1]$, thus $f_c^{\ell-\beta}(\mathbf{v}) = f_c^{\alpha+r}(\mathbf{v})+p \cdot \mathbf{w}_0 = A_c^{\alpha+r} \cdot \mathbf{v} + b_c^{\alpha+r} + p \cdot \mathbf{w}_0$, by Lemma 3. Then, for any finite execution starting with $\mathbf{v}$, and consisting of $\alpha+p\beta+r$ iterations of $c$, we have that the column vector $[\mathbf{v}[1], \dots, \mathbf{v}[n], p]^\top$ is a solution of the linear system $M_{c,r} \cdot [\mathbf{y}; z]^\top \le n_{c,r}$, where:

$$ M_{c,r} = \begin{bmatrix} M_1 & 0 \\ M_{\alpha+\beta+1} & \cdots \\ M_1 \cdot A_c^{\alpha+r} & M_1 \cdot w_0 \\ M_\beta \cdot A_c^{\alpha+r} & \cdots \\ M_\beta \cdot w_0 \end{bmatrix} \qquad n_{c,r} = \begin{bmatrix} n_1 \\ \vdots \\ n_{\alpha+\beta+1} \\ n_1 - M_1 \cdot b_c^{\alpha+r} \\ n_\beta - \dot{M}_\beta \cdot b_c^{\alpha+r} \end{bmatrix} $$

We now consider the case when the simple cycle $c = \delta_0 \dots \delta_{k-1}$ is terminal and let $w_0, \dots, w_{k-1} \in \mathbb{Z}^n$ be the vectors from Lemma 3. We say that $c$ is *infinitely iterable* iff for all $i \in [0, k-1]$, we have $C_i \cdot w_i \le 0$. Since $w_0, \dots, w_{k-1}$ are effectively computable vectors$^4$, this condition is effective. The next lemma reduces the existence of an infinite iteration of the cycle to the existence of an integer solution of a linear inequation system.

**Lemma 5.** Given an infinite pseudo-execution $(q_0, v_0) \stackrel{\tau_0}{\rightleftharpoons} (q_1, v_1) \stackrel{\tau_1}{\rightleftharpoons} \dots$ of $S$, that iterates a terminal simple cycle $c = \delta_0 \dots \delta_{k-1}$, $(q_0, v_0) \stackrel{\tau_0}{\longrightarrow} (q_1, v_1) \stackrel{\tau_1}{\longrightarrow} \dots$ is an infinite execution of $S$ iff $c$ is infinitely iterable and $v_i \models \text{guard}(\tau_i)$, for all $i \in [0, (\alpha + \beta + 1)k - 1]$.

As a consequence, for an infinitely iterable cycle $c$, the existence of an execution that iterates $c$ infinitely often is captured by the linear system $M_{c,\omega} \cdot \mathbf{y} \le n_{c,\omega}$, where $M_{c,\omega}$ and $n_{c,\omega}$ are obtained by stacking the matrices $M_1, \dots, M_{\alpha+\beta+1}$ and vectors $n_1, \dots, n_{\alpha+\beta+1}$, respectively.

We have now all the ingredients needed to bound the number of cycle iterations within the runs of a flat disjunction free affine counter system having the finite monoid property. The argument used in the proof relies on the result of Theorem 1, namely that the size of a minimal solution of a linear system of inequalities is polynomially bounded in the maximum absolute value of its coefficients, and the number of rows, and exponentially bounded in the number of columns. Since the number of rows depends on the maximum size of the monoids of the update matrices in the counter system, we use the result from [18, Lemma 13, §B.1], namely that the size of a finite monoid of a square matrix is simply exponential in the dimension of that matrix.

<footnote>$^4$ They are defined in the proof of Lemma 3.</footnote>
**Theorem 2.** Given a flat disjunction free affine counter system $S = (Q, X_n, \Delta, \Lambda)$, with the finite monoid property, for any run $\rho$ of $S$, starting in $(q_0, v_0)$, and any iterated path schema $\langle P, m \rangle \in \text{ips}(\rho)$, there exists a run $\rho'$, starting in $(q_0, v_0)$, and an iterated path schema $\langle P, m' \rangle \in \text{ips}(\rho')$, such that $\|m'\|_{\infty} \le 2^{\text{Poly}(\text{size}(S)+\text{size}(v_0))}$, for a polynomial function $\text{Poly}(x)$.

# 5 The Complexities of Decision Problems for $\mathbf{AS}_{\text{fm}}^{\text{df}}$

In this section, we will prove that the previous reasoning on iterated path schemas allows us to deduce complexity bounds of the reachability problems and of model-checking with PLTL and FO formulae for disjunction free flat counter systems with the finite monoid property.

## 5.1 Reachability is $\Sigma_2^P$

In this section we give the first upper bound, for the reachability problem and show that $\text{REACH}(\mathbf{AS}_{\text{fm}}^{\text{df}})$ is $\Sigma_2^P$. Even if this upper bound holds only for disjunction free counter system, we believe we could extend it to all the class $\mathbf{AS}_{\text{fm}}$ by adapting the method presented in [10] to eliminate the disjunctions. This would allow us to match the lower bound from Section 3. However we did not wish to enter into the heavy details of eliminating disjunctions in this work, in order to focus more on the specific aspects of affine counter systems. Anyway the provided result improves the 4EXPTIME upper bound from Table 1. The crux of the proof is based on the result provided by Theorem 2 and it follows the following reasoning: we use a polynomial-time bounded nondeterministic Turing machine that guesses an iterated path schema and then a NP oracle to check whether a guard has been violated. This gives us an $\text{NP}^{\text{NP}}$ algorithm for $\text{REACH}(\mathbf{AS}_{\text{fm}}^{\text{df}})$, which then lies in $\Sigma_2^P$. Theorem 2 ensures us the soundness of the Algorithm and the correctness is provided by the fact that if, in an iterated path schema, no guard is violated then it corresponds necessarily to a run.

Let us now explain how our NP oracle works. The next lemma is based on the fact that any power $A^k$ of a finite monoid matrix $A$ can be computed in time polynomial in $\text{size}(A)$ and $\log_2 k$, using matrix exponentiation by squaring. The reason is that the value of an entry of any power of a finite monoid matrix $A$ is bounded by an exponential in $\text{size}(A)$, thus the size of its binary representation is polynomially bounded by $\text{size}(A)$, and each step of the squaring algorithm takes polynomial time [18, Lemma 14, §B.1].

**Lemma 6.** Given an iterated path schema $\langle P, m \rangle$ of a counter system with the finite monoid property $S$ and an initial configuration $\gamma_0$, checking whether there is no run $\rho$ starting at $\gamma_0$ such that $\langle P, m \rangle \in \text{ips}(\rho)$ is in NP.

The next theorem gives the main result of this section.

**Theorem 3.** $\text{REACH}(\mathbf{AS}_{\text{fm}}^{\text{df}})$ is $\Sigma_2^P$.
## 5.2 PLTL Model Checking is $\Sigma_2^P$

For a PLTL formula $\phi$, its temporal depth $td(\phi)$ is defined as the maximal nesting depth of temporal operators in $\phi$, and the size of $\phi$ is its number of subformulae. In [10, Theorem 4.1], the authors have proved a stuttering theorem for PLTL stating that if an $\omega$-word $w = w_1w_2^Mw_3$ over the alphabet $2^{AP}$ with $w_2 \neq \epsilon$ satisfies a PLTL formula $\phi$ (i.e. $w, 0 \models_{PLTL} \phi$) and if $M \ge 2td(\phi) + 5$ then all $\omega$-words $w' = w_1w_2^{M'}w_3$ with $M' \ge 2td(\phi) + 5$ are such that $w', 0 \models_{PLTL} \phi$. In other words, to verify if an $\omega$-word with some repeated infix words satisfies a PLTL formula it is enough to verify the property for the $\omega$-words where each infix is repeated at most $2td(\phi) + 5$ times. This allows to deduce that the model-checking of PLTL for flat translating counter systems is NP-complete. We rewrite now in our terminology the main proposition which leads to this result.

In the sequel we consider a flat disjunction free counter system $S = (Q, X_n, \Delta, \Lambda)$ with the finite monoid property. For a finite sequence of transitions $\delta_1 \dots \delta_k$, we denote by $\Lambda(\delta_1 \dots \delta_k) = \Lambda(source(\delta_1)) \dots \Lambda(source(\delta_k))$ the finite word labeling the sequence with sets of atomic propositions. We lift this definition to iterated path schemas $(P, m)$ as $\Lambda(P, m) = \Lambda(P[1])^{m[1]} \Lambda(P[2])^{m[2]} \dots \Lambda(P[\text{len}(P) - 1])^{m[\text{len}(P)-1]} \Lambda(P[\text{len}(P)])^\omega$. Observe that, for a run $\rho$ of a counter system, if $(P, m) \in \text{ips}(\rho)$ is an iterated path schema, we have by definition of the semantics of PLTL that $\rho \models_{PLTL} \phi$ iff $\Lambda(P, m), 0 \models_{PLTL} \phi$ for all PLTL formulae $\phi$. Moreover, for each $m \in \mathbb{N}$, we define the function $\xi_m$ mapping each vector $v \in \mathbb{N}^k$ to $\xi_m(v) \in \mathbb{N}^k$, where, for all $i \in [1, k]: \xi_m(v)[i] = v[i]$ if $v[i] < m$ and $\xi_m(v)[i] = m$ otherwise. Let us now recall the main technical propositions established in [10], which are a consequence of the stuttering theorem for PLTL and of the result on the complexity of model-checking ultimately periodic path with PLTL given in [23].

**Lemma 7.** Let $(P, m)$ be an iterated path schema and $\phi$ a PLTL formula, then:

1. [10, Proposition 5.1] $\Lambda(P, m), 0 \models_{PLTL} \phi$ iff $\Lambda(P, \xi_{2\text{td}(\phi)+5}(m)), 0 \models_{PLTL} \phi$,

2. [23, Theorem 3.2] Given finite words $u$ and $v$, checking $uv^\omega, 0 \models_{PLTL} \phi$ can be done in time polynomial in the sizes of $uv$ and $\phi$.

We need furthermore a version of Theorem 2 above, which ensures that given an iterated path schema and a PLTL formula $\phi$, we do not change the number of times a loop is iterated if this one is less than $2.td(\phi) + 5$. The proof of the next result can in fact be deduced by adapting the proof of Theorem 2 by unfolding the loop which are iterated less than $2.td(\phi) + 5$ for a given formula $\phi$. As a consequence of Lemma 7, the new run $\rho'$, obtained in the next lemma, is such that $\rho \models_{PLTL} \phi$ iff $\rho' \models_{PLTL} \phi$ for the considered PLTL formula $\phi$.

**Lemma 8.** For a run $\rho$ of $S$ starting in $(q_0, v_0)$, an iterated path schema $(P, m) \in \text{ips}(\rho)$ and a PLTL formula $\phi$, there exists a run $\rho'$ starting in $(q_0, v_0)$, and an iterated path schema $(P, m') \in \text{ips}(\rho')$, such that $\|m'\|_\infty \le 2^{\text{Poly}(\text{size}(S)+\text{size}(v_0)+\text{td}(\phi))}$ for a polynomial $\text{Poly}(x)$ and $\xi_{2\text{td}(\phi)+5}(m) = \xi_{2\text{td}(\phi)+5}(m')$.

<footnote n="5">⁵ We take here the classical semantics of PLTL over infinite words.</footnote>
We can now explain why the model-checking of flat counter systems with the finite monoid property with PLTL formulae is in $\Sigma_2^P$. Given a flat counter system $S$ with the finite monoid property, an initial configuration $\gamma_0$, and a PLTL formula $\phi$, we guess an iterated path schema $\langle P, m \rangle$ of polynomial size in the size of $S$, $\gamma_0$ and $\phi$ and we check whether $\Lambda(P, \xi_{2\mathrm{td}(\phi)+5}(m)), 0 \models_{\mathrm{PLTL}} \phi$. This check can be done in polynomial time in the size of $P$ and $\phi$ thanks to Lemma 7. Finally, we use the NP algorithm of Lemma 6 to verify that there exists a run $\rho$ starting at $\gamma_0$, such that $\langle P, m \rangle \in \mathrm{ips}(\rho)$. This gives us a $\Sigma_2^P$ algorithm whose correctness is ensured by Lemma 8 and Lemma 2.

**Theorem 4.** $MC_{\mathrm{PLTL}}(\mathrm{AS}_{\mathrm{fm}}^{\mathrm{df}})$ is $\Sigma_2^P$.

## 5.3 FO Model Checking is PSPACE-complete

For a FO formula $\phi$, its quantifier height $qh(\phi)$ is the maximal nesting depth of its quantifiers, and the size of $\phi$ is its number of subformulae. Similarly, as for the PLTL case, in [8, Theorem 6], a stuttering theorem for FO is provided, which says that two $\omega$-words $w = w_1w_2^Mw_3$ and $w = w_1w_2^{M'}w_3$ with $w \neq \epsilon$ are indistinguishable by a FO formula $\phi$ if $M$ and $M'$ are strictly bigger than $2^{qh(\phi)+2}$. The main difference with PLTL is that this provides an exponential bound in the maximum number of times an infix of an $\omega$-word needs to be repeated to satisfy a FO formula. In the sequel we consider a flat counter system $S = \langle Q, X_n, \Delta, \Lambda \rangle$ with the finite monoid property and we reuse the notations introduced in the previous section. The results of [8] can be restated as follows.

**Lemma 9.** Given an iterated path schema $\langle P, m \rangle$ and a FO formula $\phi$, then:

1. [8, Lemma 7] $\Lambda(P, m) \models_{\mathrm{FO}} \phi$ iff $\Lambda(P, \xi_{2qh(\phi)+2}(m)) \models_{\mathrm{FO}} \phi$,

2. [8, Theorem 9] Checking $\Lambda(P, m), 0 \models_{\mathrm{FO}} \phi$ can be done in space polynomial in the sizes of $\langle P, m \rangle$ and $\phi$.

As for the PLTL case, this allows us to deduce a NPSPACE algorithm for the model-checking problem of flat counter system with the finite monoid property with FO formulae. Since the problem is already PSPACE-hard for flat translating counter systems [8, Theorem 9], we conclude by the following theorem.

**Theorem 5.** $MC_{\mathrm{FO}}(\mathrm{AS}_{\mathrm{fm}}^{\mathrm{df}})$ is PSPACE-complete.

## References

1. Arora, S., Barak, B.: Computational complexity: a modern approach. Cambridge University Press (2009)

2. Bardin, S., Finkel, A., Petrucci, J.L.L.: Fast: Fast acceleration of symbolic transition systems. http://tapas.labri.fr/trac/wiki/FASTer

3. Blondin, M., Finkel, A., Göller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is pspace-complete. CoRR abs/1412.4259 (2014), http://arxiv.org/abs/1412.4259
4. Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD, Univ. de Liège (1999)

5. Bozga, M., Iosif, R., Konečný, F.: Deciding conditional termination. Logical Methods in Computer Science 10(3) (2014)

6. Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: CAV. LNCS, vol. 6174, pp. 227–242 (2010)

7. Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: CONCUR '99, Proceedings. pp. 242–257 (1999)

8. Demri, S., Dhar, A.K., Sangnier, A.: On the complexity of verifying regular properties on flat counter systems. In: ICALP'13. LNCS, vol. 7966, pp. 162–173 (2013)

9. Demri, S., Dhar, A.K., Sangnier, A.: Equivalence between model-checking flat counter systems and presburger arithmetic. In: RP'14. LNCS, vol. 8762, pp. 85–97. Springer (2014)

10. Demri, S., Dhar, A.K., Sangnier, A.: Taming past LTL and flat counter systems. Inf. Comput. 242, 306–339 (2015)

11. Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking CTL* over flat presburger counter systems. Journal of Applied Non-Classical Logics 20(4), 313–344 (2010)

12. Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: FST TCS '02. pp. 145–156 (2002)

13. Gawlitza, T.M., Monniaux, D.: Invariant generation through strategy iteration in succinctly represented control flow graphs. LMCS 8(3) (2012)

14. Göller, S., Haase, C., Ouaknine, J., Worrell, J.: Model checking succinct and parametric one-counter automata. In: ICALP'10. LNCS, vol. 6199, pp. 575–586. Springer (2010)

15. Gurari, E.M., Ibarra, O.H.: The complexity of decision problems for finite-turn multicounter machines. J. Computer and System Sciences 22, 220–229 (1981)

16. Haase, C.: Subclasses of Presburger arithmetic and the weak EXP hierarchy. In: CSL-LICS '14. pp. 47:1–47:10. ACM (2014)

17. Hojjat, H., Iosif, R., Konečný, F., Kuncak, V., Rümmer, P.: Accelerating Interpolants, pp. 187–202. Springer Berlin Heidelberg (2012)

18. Iosif, R., Sangnier, A.: How hard is it to verify flat affine counter systems with the finite monoid property? CoRR abs/1605.05836 (2016), http://arxiv.org/abs/1605.05836

19. Konečny, F., Iosif, R., Bozga, M.: Flata: a verification toolset for counter machines. http://nts.imag.fr/index.php/Flata (2009)

20. Kuhtz, L., Finkbeiner, B.: Weak Kripke structures and LTL. In: CONCUR'11. LNCS, vol. 6901, pp. 419–433. Springer (2011)

21. Leroux, J., Sutre, G.: On Flatness for 2-Dimensional Vector Addition Systems with States, pp. 402–416 (2004)

22. Lipton, R.J.: The reachability problem is exponential-space-hard. Tech. Rep. 62, Yale University, Department of Computer Science (1976)

23. Markey, N., Schnoebelen, P.: Model checking a path. In: CONCUR'03. LNCS, vol. 2761, pp. 248–262 (2003)

24. Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall (1967)

25. Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. J. ACM 32(3), 733–749 (1985)

26. Stockmeyer, L.J.: The complexity of decision problems in automata and logic. Ph.D. thesis, MIT (1974)