Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic

TL;DR

This paper introduces a method for approximate verification of counter systems against expressive counting temporal logic properties using flat model checking and Presburger arithmetic, enabling scalable analysis.

Contribution

It presents a novel approximation approach employing flat under-approximations and Presburger arithmetic for verifying counting LTL properties, extending recent frequency property techniques.

Findings

Prototype implementation with z3 SMT solver shows effectiveness.

Approach handles expressive counting properties in counter systems.

Trade-off between analysis completeness and computational effort.

Abstract

This paper presents an approximation approach to verifying counter systems with respect to properties formulated in an expressive counting extension of linear temporal logic. It can express, e.g., that the number of acknowledgements never exceeds the number of requests to a service, by counting specific positions along a run and imposing arithmetic constraints. The addressed problem is undecidable and therefore solved on flat under-approximations of a system. This provides a flexibly adjustable trade-off between exhaustiveness and computational effort, similar to bounded model checking. Recent techniques and results for model-checking frequency properties over flat Kripke structures are lifted and employed to construct a parametrised encoding of the (approximated) problem in quantifier-free Presburger arithmetic. A prototype implementation based on the z3 SMT solver demonstrates the effectiveness of the approach based on problems from the RERS Challange.

Equations

$$G(\neg \text{reset}{U}_{[2e_1-e_2\ge -10]}\text{reset})$$

$$\phi$$

$$\tau$$

$$\begin{array}[]{l@{\hspace{1.4ex}}c@{\hspace{1.4ex}}l}(\mathcal{S},\rho,i)\models\gamma\hfil\hskip 6.02773pt&:\Leftrightarrow\hfil\hskip 6.02773pt&\theta_{i}\models\gamma\\ (\mathcal{S},\rho,i)\models\varphi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi\hfil\hskip 6.02773pt&:\Leftrightarrow\hfil\hskip 6.02773pt&\exists_{j\geq i}:(\mathcal{S},\rho,j)\models\psi\text{ and }\llbracket\tau\rrbracket(\#^{\mathcal{S},\rho}_{i,j-1})\geq b\\ \hfil\hskip 6.02773pt&\hfil\hskip 6.02773pt&\text{ and }\forall_{i\leq k<j}:(\mathcal{S},\rho,k)\models\varphi\end{array}$$

$${\#}_{i,j}^{\mathcal{S},\rho }(\chi ):=|\{k\mid i\le k\le j,(\mathcal{S},\rho ,k)\models \chi \}|$$

$$\rho \in \mathsf{FA}(\mathcal{S},n)\iff$$

$$\wedge {\exists }_{k_0,\dots ,k_{m-1}\in \mathbb{N}}:s_0{s}_1\dots =u_0{v}_0^{k_0}\dots u_{m-1}{v}_{m-1}^{k_{m-1}}{u}_m{v}_m^{\omega }.$$

$$\mu (c_{\tau ,q})=\{\begin{array}{ll}0& \text{if q1∈sucP∗(q)}\\ [[\tau ]]({\lambda }_{\mathcal{P}}^{\#}(q_1))& \text{otherwise}.\end{array}$$

$$\mathrm{fmc}(\mathcal{S},\Phi ,n):=\mathrm{aps}(\mathcal{S},n)\wedge \mathrm{run}(\mathcal{S},n)\wedge \mathrm{consistency}(n,\Phi )\wedge \Phi \in {\mathsf{lbl}}_0$$

$$\begin{gathered} {\bigwedge }_{i=1}^{n-1}{\bigwedge }_{(s,\mu ,\Gamma ,s^{\prime })\in \Delta }{\mathsf{org}}_{i-1}=s\wedge {\mathsf{org}}_i=s^{\prime } \\ \to {\bigwedge }_{(\tau \ge b)\in \Gamma }\tau [{\mathsf{valFst}}_i]\ge b\wedge (\neg {▹}_i\to \tau [{\mathsf{valLst}}_i]\ge b) \end{gathered}$$

$${\mathsf{valLst}}_i={\mathsf{valFst}}_i+({\mathsf{valSec}}_i-{\mathsf{valFst}}_i)\cdot ({\mathsf{itr}}_i-1).$$

$$\bigwedge_{i\in[1,n-2]\atop(s,\mu,\Gamma,s^{\prime})\in\Delta}\left(\begin{array}[]{rcll}&(\triangleleft_{i}&\land\ \mathsf{org}_{i-1}{=}s\land\mathsf{org}_{i}{=}s^{\prime}&\to\mathsf{lUpd}_{i}{=}\mu\cdot\mathsf{itr}_{i}-\mu)\\ \land&({\raisebox{-0.3pt}{\scalebox{0.8}{$\boxplus$}}}_{i}&\land\ \mathsf{org}_{i-1}{=}s\land\mathsf{org}_{i}{=}s^{\prime}&\to\mathsf{lUpd}_{i}{=}\mu\cdot\mathsf{itr}_{i}-\mu+\mathsf{lUpd}_{i+1})\\ \land&(\triangleright_{i}&\land\ \mathsf{orgAtEnd}_{i}{=}s\land\mathsf{org}_{i}{=}s^{\prime}&\to\mathsf{lUpd}_{i}{=}\mu\cdot\mathsf{itr}_{i}-\mu+\mathsf{lUpd}_{i+1})\end{array}\right)\begin{array}[]{@{\hspace{-1.25ex}}l}\\ \\[6.88889pt] .\end{array}$$

$$\underset{c\in C_{\mathcal{S}}}{\bigwedge }\begin{array}{rl}& ({\mathsf{valFst}}_i(c)={\mathsf{valSec}}_i(c)={\mathsf{valLst}}_i(c))\\ & \vee ({\mathsf{valFst}}_i(c)>{\mathsf{valSec}}_i(c)\wedge {\mathsf{valLst}}_i(c)=-\infty )\\ & \vee ({\mathsf{valFst}}_i(c)<{\mathsf{valSec}}_i(c)\wedge {\mathsf{valLst}}_i(c)=\infty ).\end{array}$$

$$(\tau \ge b)\in {\mathsf{lbl}}_i\leftrightarrow \tau [{\mathsf{valFst}}_i]\ge b\wedge \tau [{\mathsf{valLst}}_i]\ge b$$

$$\displaystyle\mathsf{ite}\big{(}\operatorname{\mathrm{\mathbf{X}}}\varphi{\in}\mathsf{lbl}_{i},\,\varphi{\in}\mathsf{lbl}_{i+1}\land(\triangleleft_{i}\to\varphi{\in}\mathsf{lblAtBeg}_{i}),\,\varphi{\not\in}\mathsf{lbl}_{i+1}\land(\triangleleft_{i}\to\varphi{\not\in}\mathsf{lblAtBeg}_{i})\big{)}.$$

$$({\mathsf{acc}}_{n-1}^{\tau }=\tau [{\mathsf{lbl}}_{n-1}])\wedge {\bigwedge }_{i=0}^{n-2}\mathrm{ite}({\mathsf{itr}}_i=0,{\mathsf{acc}}_i^{\tau }={\mathsf{acc}}_{i+1}^{\tau }+\tau [{\mathsf{lbl}}_i],{\mathsf{acc}}_i^{\tau }={\mathsf{acc}}_{i+1}^{\tau }).$$

$$\begin{gathered} \mathrm{glob}(n,\chi ):=({\mathsf{prpg}}_{n-1}^{\chi }\leftrightarrow \chi \in {\mathsf{lbl}}_{n-1})\wedge \left({\bigwedge }_{i=0}^{n-2}{\mathsf{prpg}}_i^{\chi }\leftrightarrow {\mathsf{prpg}}_{i+1}^{\chi }\wedge \chi \in {\mathsf{lbl}}_i\right) \\ \wedge ({\mathsf{glob}}_0^{\chi }\leftrightarrow {\mathsf{prpg}}_0^{\chi })\wedge {\bigwedge }_{i=1}^{n-1}{\mathsf{glob}}_i^{\chi }\leftrightarrow \mathrm{ite}({\text{scalebox}0.8\boxminus }_i\vee {▹}_i,{\mathsf{prpg}}_i^{\chi },{\mathsf{glob}}_{i-1}^{\chi }) \end{gathered}$$

$$\mathrm{fin}(n,\psi ):={\mathsf{onLast}}^{\psi }\leftrightarrow {\bigvee }_{i=0}^{n-1}{\mathsf{itr}}_i=0\wedge \psi \in {\mathsf{lbl}}_i.$$

$$\mathrm{con}\text{ref}\mathrm{itm}:\mathrm{consistency}-\mathrm{U}-\mathrm{goodlast}(\phi ,i):=\phi \in {\mathsf{lbl}}_i\wedge {\mathsf{acc}}_0^{\tau }>0\wedge {\mathsf{onLast}}^{\psi }\wedge {\mathsf{glob}}_i^{\chi }.$$

$$(\phi \in {\mathsf{lbl}}_i\leftrightarrow {\mathsf{maxFst}}_i^{\phi }\ge b)\wedge ((\phi \in {\mathsf{lbl}}_i\leftrightarrow {\mathsf{maxLst}}_i^{\phi }\ge b)\vee {\mathsf{itr}}_i=0).$$

$$\begin{gathered} \left({\bigwedge }_{i=1}^{n-2}\mathrm{ite}({▹}_i,{\mathsf{sumEff}}_i^{\tau }={\mathsf{eff}}_i^{\tau },{\mathsf{sumEff}}_i^{\tau }={\mathsf{sumEff}}_{i-1}+{\mathsf{eff}}_i^{\tau })\right) \\ \wedge {\bigwedge }_{i=0}^{n-1}\mathrm{ite}({\chi }_0\in {\mathsf{lbl}}_i,{\mathsf{eff}}_i^{t,0}=a_0\cdot {\mathsf{itr}}_i-3a_0,{\mathsf{eff}}_i^{t,0}=0) \\ \wedge {\bigwedge }_{k=1}^m\mathrm{ite}({\chi }_k\in {\mathsf{lbl}}_i,{\mathsf{eff}}_i^{t,k}={\mathsf{eff}}_i^{t,k-1}+a_k\cdot {\mathsf{itr}}_i-3a_k,{\mathsf{eff}}_i^{t,k}={\mathsf{eff}}_i^{t,k-1}) \end{gathered}$$

$$({\raisebox{-0.3pt}{\scalebox{0.8}{$\boxminus$}}}_{i}\to\mathsf{updFst}^{\varphi}_{i}{=}\mathsf{updLst}^{\varphi}_{i}{=}\mathsf{maxFst}^{\varphi}_{i+1}+\tau[\mathsf{lbl}_{i}])\\ \land\big{(}\triangleleft_{i}\to\mathsf{updLst}^{\varphi}_{i}{=}\mathsf{maxFst}^{\varphi}_{i+1}+\tau[\mathsf{lbl}_{i}]\land\mathsf{updFst}^{\varphi}_{i}{=}\mathsf{maxAuxAtBeg}^{\varphi}_{i}+\tau[\mathsf{lbl}_{i}]\\ \land\mathsf{updAux}^{\varphi}_{i}{=}\mathsf{maxLst}^{\varphi}_{i}+\mathsf{sumEff}^{\tau}_{i}\big{)}\\ \land\big{(}\triangleright_{i}\lor\ {\raisebox{-0.3pt}{\scalebox{0.8}{$\boxplus$}}}_{i}\to\mathsf{updLst}^{\varphi}_{i}{=}\mathsf{maxLst}^{\varphi}_{i+1}+\tau[\mathsf{lbl}_{i}]\land\mathsf{updFst}^{\varphi}_{i}{=}\mathsf{maxFst}^{\varphi}_{i+1}+\tau[\mathsf{lbl}_{i}]\\ \land\mathsf{updAux}^{\varphi}_{i}{=}\mathsf{maxAux}^{\varphi}_{i+1}+\tau[\mathsf{lbl}_{i}]\big{)}.$$

$$\begin{gathered} \mathrm{glob}(n,\chi )\wedge \mathrm{accu}(n,t)\wedge \mathrm{fin}(n,\psi )\wedge \mathrm{witnessMax}(n,\chi U_{[\tau \ge b]}\psi ) \\ \wedge {\bigwedge }_{i=0}^{n-1}\mathrm{con}\text{ref}\mathrm{itm}:\mathrm{consistency}-\mathrm{U}-\mathrm{goodlast}(\chi U_{[\tau \ge b]}\psi ,i)\vee \mathrm{con}\text{ref}\mathrm{itm}:\mathrm{consistency}-\mathrm{U}-\mathrm{counter}(\chi U_{[\tau \ge b]}\psi ,i). \end{gathered}$$

$$\mathrm{fmc}(\mathcal{S},\Phi ,n):=\mathrm{aps}(\mathcal{S},n)\wedge \mathrm{run}(\mathcal{S},n)\wedge \mathrm{consistency}(n,\Phi )\wedge \Phi \in {\mathsf{lbl}}_0$$

$$\mathrm{aps}(\mathcal{S},n):={\mathsf{org}}_0=s_I\wedge \mathrm{typ}(n)\wedge \mathrm{labels}(\mathcal{S},n)\wedge \mathrm{transitions}(\mathcal{S},n).$$

$$\mathrm{typ}(n):=\underset{i\in [1,n-1]}{\bigwedge }\mathrm{ite}({◃}_{i-1}\vee {\text{scalebox}0.8\boxminus }_{i-1},{\text{scalebox}0.8\boxminus }_i\vee {▹}_i,{\text{scalebox}0.8⊞}_i\vee {◃}_i).$$

$$\mathrm{labels}(\mathcal{S},n):=\underset{\genfrac{}{}{0ex}{}{p\in AP,}{i\in [0,n-1]}}{\bigwedge }p\in {\mathsf{lbl}}_i\leftrightarrow \underset{s\in {\lambda }^{-1}(p)}{\bigvee }{\mathsf{org}}_i=s$$

$$\mathrm{orgAtEnd}(n):=$$

$$\wedge \underset{i\in [0,n-2]}{\bigwedge }\mathrm{ite}({◃}_i,{\mathsf{orgAtEnd}}_i={\mathsf{org}}_i,{\mathsf{orgAtEnd}}_i={\mathsf{orgAtEnd}}_{i+1}).$$

$$\mathrm{transitionsBwd}(\mathcal{S},n):=\underset{i\in [0,n-1]}{\bigwedge }{▹}_i\to \underset{(s,\mu ,\Gamma ,s^{\prime })\in \Delta }{\bigvee }{\mathsf{orgAtEnd}}_i=s\wedge {\mathsf{org}}_i=s^{\prime }$$

$$\mathrm{transitionsFwd}(\mathcal{S},n):=\underset{i\in [1,n-1]}{\bigwedge }\underset{(s,\mu ,\Gamma ,s^{\prime })\in \Delta }{\bigvee }{\mathsf{org}}_{i-1}=s\wedge {\mathsf{org}}_i=s^{\prime }.$$

$$\mathrm{transitions}(\mathcal{S},n):=\mathrm{orgAtEnd}(n)\wedge \mathrm{transitionsBwd}(\mathcal{S},n)\wedge \mathrm{transitionsFwd}(\mathcal{S},n)$$

Full text

1 Introduction

Counting is a fundamental principle in the theory of computation and well-established in the study and verification of infinite-state systems. The concept is ubiquitous in programming, and counting mechanisms are a natural notion of quantitative measurement in specification formalisms. For example, they are useful for expressing constraints such as “the number of acknowledgements never exceeds the number of requests” or “the relative error frequency stays below some threshold”. An established and well-studied framework for correctness specification is linear temporal logic ($\mathsf{LTL}$) [29]. Therefore, various counting extensions were proposed [8, 24, 6, 13] that allow for imposing constraints on the number of positions along a run that satisfy some property. These extensions target different kinds of system models, and vary in the type of events that can be counted and the constraints that can be expressed.

This paper is concerned with verifying properties expressed in the counting temporal logic $\mathsf{CLTL}$. This extension of $\mathsf{LTL}$ features a generalised temporal until operator $\operatorname{\mathbf{U}}_{[.]}$ for evaluating a counting constraint within its scope. For example, consider the property that between two system resets, two events $e_{1}$ and $e_{2}$ (say, related sensor events) should be correlated linearly. The $\mathsf{CLTL}$ formula

[TABLE]

would specify that there are not more than twice as many occurrences of $e_{1}$ than there are of $e_{2}$, with an absolute margin of $10$. Notice that this property is not regular. The events $e_{1}$ and $e_{2}$ may be atomic or again characterised by some temporal (counting) property. The definition used111To avoid cluttered notation when respecting various existing naming schemes, the denotation $\mathsf{CLTL}$ is reused, despite semantic differences. here extends that of [24] by admitting not only natural but arbitrary integer coefficients in constraints. Without this extension, the logic was shown to be more concise but not more expressive than $\mathsf{LTL}$. Moreover, in the present work, $\mathsf{CLTL}$ is interpreted over counter systems instead of Kripke structures and allows for imposing arithmetic constraints also on (linear combinations of) the counter values, similar to the formalisms considered in [32, 11, 16].

Towards making the extended features of this specification language available for program verification, we propose an approach to the existential model-checking problem of $\mathsf{CLTL}$ over counter systems, i.e. deciding for some counter system whether it admits a run satisfying a given formula. Both system model and logic are very powerful, and the problem is undecidable. However, we avoid the often made compromise of recovering decidability by means of essential restrictions to the specification language. Instead, we use an approximation scheme based on an extension of recent work [13] that has laid the theoretical basis for a decision procedure in the special case of structures that are flat. Flatness demands, essentially, that cycles of the system cannot be alternated during an execution. It is thus a strong restriction but decreases the computational complexity of verification tasks significantly. To benefit from the improved complexity while being generally applicable, our approach verifies flat under-approximations of a specific depth given as parameter. Similarly to bounded model checking [5, 4], the parameter allows the user to flexibly adjust the trade-off between exhaustiveness and computational effort. An essential advantage of flat under-approximations is that they represent sets of complete (infinite) runs instead of only a finite number of bounded prefixes. They can be understood as a bounded unfolding of loop alternations, represented symbolically. When increasing the approximation depth to include one more alternation, an infinite number of additional runs is represented, and verified at once. Considering first a small depth and increasing it only if no witness was found allows for finding “simple” witnesses quickly where they exist, even for complex path properties that cannot be evaluated on prefixes. The underlying theory provides a bound on the maximal depth that needs to be considered in the case of a flat system. The method is (necessarily) incomplete in the general case but can nevertheless be directly applied.

1.0.1 Contributions.

As conceptual basis, we first extend the theory of model-checking counting logics on flat structures developed in [13], where only frequency constraints and Kripke structures were considered. Symbolic models called augmented path schemas were introduced to represent sets of runs. We extend the definitions and techniques to apply to more general counting constraints and flat counter systems while preserving the previous complexity bounds. This is a consequent continuation of the development of the theory. From the user perspective, it is a valuable extension, since $\mathsf{CLTL}$ provides a much more flexible specification language and counter systems an extended application domain. It is particularly important for the practical application of the method.

Subsequently, based on the lifted theory, we describe an explicit formulation of the (approximated) model-checking problem in quantifier-free Presburger arithmetic (QPA). Recall that Presburger arithmetic is first-order logic over the integer numbers with addition. Its satisfiability problem is decidable [30] and in the case of the quantifier-free fragment in NP [7]. Importantly, the theory of QPA is well-supported by a number of competitive SMT-solvers (cf. [10]). Our construction is parametrised by the depth of the flat approximation that is to be verified, and the resulting QPA formula is linear in the problem size and the chosen depth.

We have implemented the incremental model-checking procedure based on the QPA encoding and the z3 SMT solver [28]. Verification tasks of the RERS Challenge [21] and counting variations were used to evaluate the effectiveness of our approach.

1.0.2 Related work.

In [6] an $\mathsf{LTL}$ extension to express relative frequencies, called $\mathsf{fLTL}$, was studied. It features a generalised until operator that can be understood as a variant of the $\operatorname{\mathbf{U}}_{[.]}$ operator restricted to a specific class of counting constraints. Various other classes were studied in the context of $\mathsf{CTL}$ [25]. One of the corresponding $\mathsf{CTL}$ variants, denoted $\mathsf{CCTL_{\pm}}$, admits integer coefficients and thus represents the branching-time analog to $\mathsf{CLTL}$, although interpreted over finite Kripke structures. The difference between linear and branching time is crucial, however. Satisfiability, and hence model checking Kripke structures, is undecidable for $\mathsf{fLTL}$ [6] (and hence for $\mathsf{CLTL}$) but decidable for its branching-time analog $\mathsf{fCTL}$ and even $\mathsf{CCTL_{\pm}}$ [25, 13]. Counting extensions were also studied for regular expressions in [19, 1]. The notion of flat (or weak) systems was investigated as a sensible restriction to reduce the computational complexity of various verification problems. Considering (finite) Kripke structures, model-checking $\mathsf{LTL}$ properties, which is PSpace-complete [31], becomes NP-complete under the flatness condition [23]. It follows from [6] that model-checking $\mathsf{fLTL}$, and thus all more expressive counting logics, is undecidable. Over flat Kripke structures, the problem is in NExp and even an extremely powerful counting extension of CTL​* was shown to become decidable [13]. A similar impact is observable for (infinite state) counter systems. While reachability is already undecidable for two-counter systems [27], results from [12] provide that flatness recovers decidability with an arbitrary number of counters (see also [11]). Later, it was shown in [15] that $\mathsf{LTL}$ properties (including past) can generally be evaluated in NP (see also [17]). The authors also make the suggestion to consider flat systems as under-approximations, which is addressed here. Increasing the depth of a flat under-approximation is similar to so-called loop acceleration in symbolic verification. It aims at stepping over an arbitrary number of consecutive iterations of a loop during state space exploration, by symbolically representing its effect. Since this is particularly effective for simple loops, flatness is a desired property [2] also in this setting. Unfortunately, acceleration typically concerns the computation of reachability sets [2, 3, 9, 22, 20] and is thus insufficient when analysing path properties as expressible in (extensions of) $\mathsf{LTL}$. For accelerating the latter, flat systems, and path schemas in particular, provide a suitable symbolic model since they represent entire runs.

1.0.3 Outline.

First, Section 2 provides basic definitions. In Section 3, a generalised notion of augmented path schemas is introduced and employed to lift the decidability results of [13]. It provides the basis for Section 4 describing the parametrised encoding of the model-checking problem into QPA. Section 5 reports on our implementation of the approach and Section 6 concludes.

2 Counting in Linear Temporal Logic

2.0.1 Constraints and counter systems.

For $x,y\in\mathbb{Z}$ let $[x,y]$ denote the (potentially empty) interval $\{x,x+1,\ldots,y\}\subset\mathbb{Z}$. A constraint over a set $X$ is a linear arithmetic inequation $\tau\geq b$ where $\tau=\sum_{i=0}^{n}a_{i}x_{i}$, $n\in\mathbb{N}$, $b,a_{i}\in\mathbb{Z}$, and $x_{i}\in X$ for $i\in[0,n]$. For convenience, we may use relation symbols $\leq$, $<$, and $>$, denoting arithmetically equivalent constraints, e.g. $2x_{1}+x_{2}<3$ denotes $-2x_{1}-x_{2}\geq-2$. The dual of a constraint $\tau\geq b$ is denoted by $\overline{\tau\geq b}$ and defined as the equivalent of $\tau<b$. For a valuation $\theta:X\to\mathbb{Z}$, we denote by $\llbracket\tau\rrbracket(\theta):=\sum_{i=0}^{n}a_{i}\theta(x_{i})$ the arithmetic evaluation of $\tau$. Satisfaction is defined as $\theta\models\tau\geq b$ if and only if $\llbracket\tau\rrbracket(\theta)\geq b$. Constraint sets are interpreted as conjunction and satisfaction is defined accordingly. The set of all constraints over $X$ is denoted $\mathfrak{C}(X)$. For convenience, arithmetic operations are lifted point-wise to integer-valued functions of equal domain.

Let $\Lambda$ be a set of labels and $C_{\mathcal{S}}$ a finite set of system counters. A counter system (CS) over $\Lambda$ and $C_{\mathcal{S}}$ is a tuple $\mathcal{S}=(S,\Delta,s_{I},\lambda)$ where $S$ is a finite set of control states, $s_{I}\in S$ is the initial state, $\lambda:S\to 2^{\Lambda}$ is a labelling function, and $\Delta\subseteq S\times\mathbb{Z}^{C_{\mathcal{S}}}\times 2^{\mathfrak{C}(C_{\mathcal{S}})}\times S$ is a finite set of transitions carrying an update $\mu:C_{\mathcal{S}}\to\mathbb{Z}$ to the system counters and a finite set of guards $\Gamma\subseteq\mathfrak{C}(C_{\mathcal{S}})$ over them. A configuration of $\mathcal{S}$ is a pair $(s,\theta)$ comprised of a state $s\in S$ and a valuation $\theta:C_{\mathcal{S}}\to\mathbb{Z}$. A run of $\mathcal{S}$ is an infinite sequence $\rho=(s_{0},\theta_{0})(s_{1},\theta_{1})\ldots\in(S\times\mathbb{Z}^{C_{\mathcal{S}}})^{\omega}$ such that $(s_{0},\theta_{0})=(s_{I},\mathbf{0})$ and for all positions $i\in\mathbb{N}$ there is a transition $(s_{i},\mu_{i},\Gamma_{i},s_{i+1})\in\Delta$ such that $\theta_{i+1}=\theta_{i}+\mu_{i}$ and $\theta_{i+1}\models\Gamma_{i}$. The set of all runs of $\mathcal{S}$ is denoted $\mathrm{runs}(\mathcal{S})$.

Let $\lambda^{\#}:S^{*}\to\mathbb{N}^{\Lambda}$ denote the accumulation of labels in a multi-set fashion, counting the number of occurrences of each label on a finite state sequence $w\in S^{*}$ by $\lambda^{\#}_{\mathcal{P}}(w):\ell\mapsto|\{i\in[0,|w|-1]\mid\ell\in\lambda(w(i))\}|$ for all $\ell\in\Lambda$. The set of successors of a state $s\in S$ in $\mathcal{S}$ be denoted by $\mathrm{suc}_{\mathcal{\mathcal{S}}}(s):=\{s^{\prime}\in S\mid\exists_{\mu,\Gamma}:(s,\mu,\Gamma,s^{\prime})\in\Delta\}$, and the corresponding transitive and reflexive closure by $\mathrm{suc}_{\mathcal{\mathcal{S}}}^{*}(s)$. A (finite) path in $\mathcal{S}$ is a (finite) state sequence $w=s_{0}s_{1}\ldots$ with $s_{i+1}\in\mathrm{suc}_{\mathcal{\mathcal{S}}}(s_{i})$ for all $0\leq i<|w|$. A finite path $w=s_{0}\ldots s_{n}$ is simple if no state occurs twice, it is a loop if $s_{0}\in\mathrm{suc}_{\mathcal{\mathcal{S}}}(s_{n})$, and a row if no state is part of any loop in $\mathcal{S}$. The counter system $\mathcal{S}$ is flat if for every state $s\in S$ there is at most one simple loop $s_{0}\ldots s_{n}$ with $s_{0}=s$. Let the size of $\mathcal{S}$ be denoted by $|\mathcal{S}|$ and defined as the length of its syntactic representation with numbers encoded binary.

2.0.2 Counting LTL.

We consider linear temporal logic extended by counting constraints in the style of [24]. In contrast, however, we admit arbitrary integer coefficients. Moreover, the semantics is defined in terms of runs of counter systems and the logic provides access to the counter valuation by means of Presburger constraints. Let $AP$ and $C$ be fixed, finite sets of atomic propositions and counter names, respectively. The set of $\mathsf{CLTL}$ formulae (denoted simply by $\mathsf{CLTL}$) is defined by the grammar

[TABLE]

for atomic propositions $p\in AP$, guards over counter names $\gamma\in\mathfrak{C}(C)$ and integer constants $a,b\in\mathbb{Z}$. Additional abbreviations may be used with expected semantics, in particular $\mathsf{false}:=\neg\mathsf{true}$, $\varphi\operatorname{\mathrm{\mathbf{U}}}\psi:=\varphi\operatorname{\mathbf{U}}_{[1\cdot\mathsf{true}\geq 0]}\psi$ and $\operatorname{\mathbf{F}}_{[\tau\geq b]}\varphi:=\mathsf{true}\operatorname{\mathbf{U}}_{[\tau\geq b]}\varphi$. We may write $\mathsf{CLTL}(C^{\prime})$ for the restriction to formulae that only use counter names from some specific set $C^{\prime}\subseteq C$. By $\mathrm{sub}(\varphi)$ we denote the set of subformulae of $\varphi$ (including itself).

Let $\mathcal{S}=(S,\Delta,s_{I},\lambda)$ be a counter system over counters $C_{\mathcal{S}}$ with a run $\rho=(s_{0},\theta_{0})(s_{1},\theta_{1})\ldots$ and $i\geq 0$ a position on $\rho$. Observe that expressions of the form $\tau\geq b$ are in fact arithmetic constraints from the set $\mathfrak{C}(\mathsf{CLTL})$. The satisfaction relation $\models$ is defined inductively as follows. For plain $\mathsf{LTL}$ formulae, the usual definition applies. Additionally, for $(\tau\geq b)\in\mathfrak{C}(\mathsf{CLTL}(C_{\mathcal{S}}))$, $\gamma\in\mathfrak{C}(C_{\mathcal{S}})$, and $\varphi,\psi\in\mathsf{CLTL}(C_{\mathcal{S}})$ let

[TABLE]

where $\#_{i,j}^{\mathcal{S},\rho}:\mathsf{CLTL}\to\mathbb{N}$ denotes the function mapping a $\mathsf{CLTL}$ formula $\chi$ to the number

[TABLE]

of positions on $\rho$ between $i$ and $j$ satisfying it. Notice that this is well-defined because the mutual recursion descends towards strict subformulae. We write $(\mathcal{S},\rho)\models\chi$ if $(\mathcal{S},\rho,0)\models\chi$ and $\mathcal{S}\models\chi$ if there is $\rho\in\mathrm{runs}(\mathcal{S})$ with $(\mathcal{S},\rho)\models\chi$.

The logic $\mathsf{fLTL}$ [6] features a dedicated frequency-until operator $\operatorname{\mathrm{\mathbf{U}}}^{\frac{a}{b}}$ for $a,b\in\mathbb{N}$ and $a\leq b>0$ that can be considered as restricted variant of $\operatorname{\mathbf{U}}_{[.]}$. An $\mathsf{fLTL}$ formula $\varphi\operatorname{\mathrm{\mathbf{U}}}^{\frac{a}{b}}\psi$ specifies that a formula $\varphi$ holds at least at a fraction $0\leq\frac{a}{b}\leq 1$ of all positions before some position satisfying $\psi$. This is equivalently expressed in $\mathsf{CLTL}$ by $\mathsf{true}\operatorname{\mathbf{U}}_{[b\cdot\varphi-a\cdot\mathsf{true}\geq 0]}\psi$.

2.0.3 Model checking.

We target the existential model-checking problem for $\mathsf{CLTL}$. Given a counter system $\mathcal{S}$ and a $\mathsf{CLTL}$ formula $\Phi$ the task is to decide whether $\mathcal{S}\models\Phi$, i.e., to compute if $\mathcal{S}$ contains a run satisfying $\Phi$. The problem is undecidable for two reasons: First, counter systems extend Minsky machines [27] and even $\mathsf{LTL}$ can express their undecidable (control-state) reachability problem. Second, $\mathsf{CLTL}$ extends $\mathsf{fLTL}$ and checking a universal Kripke structure encodes its undecidable satisfiability problem [6]. We therefore approach a parametrised approximation of the problem that considers only runs with a specific shape, namely those represented by so-called path schemas. A path schema [26, 15] is characterised by a (connected) sequence $u_{0}v_{0}u_{1}v_{1}\ldots u_{n}v_{n}$ of paths $u_{i}$ and cycles $v_{i}$ of $\mathcal{S}$. It represents all those runs $\rho$ of $\mathcal{S}$ that traverse a state sequence of the form $u_{0}v_{0}^{\ell_{0}}\ldots u_{n-1}v_{n-1}^{\ell_{n-1}}u_{n}v_{n}^{\omega}$. Restricting the length of such a schema effectively controls how complicated the shape of the considered runs can be. In particular, it bounds the cycle alternation performed by a run.

Definition 1 (Flat model checking)

Let $\mathcal{S}=(S,\Delta,s_{I},\lambda)$ be a counter system and $n\in\mathbb{N}$. The flat approximation of depth $n$ of $\mathcal{S}$ is the set $\mathsf{FA}(\mathcal{S},n)\subseteq\mathrm{runs}(\mathcal{S})$ such that, for all $\rho=(s_{0},\theta_{0})(s_{1},\theta_{1})\ldots\in\mathrm{runs}(\mathcal{S})$,

[TABLE]

The flat model-checking problem is to decide for a given $\mathsf{CLTL}$ formula $\varphi$, whether there is a run $\rho\in\mathsf{FA}(\mathcal{S},n)$ with $(\mathcal{S},\rho)\models\varphi$, denoted $\mathsf{FA}(\mathcal{S},n)\models\varphi$.

A flat approximation $\mathsf{FA}(\mathcal{S},n)$ induces a flat counter system $\mathcal{F}$ such that $\mathsf{FA}(\mathcal{S},n)=\mathrm{runs}(\mathcal{F})$ and thus a series $(\mathcal{F}_{n})_{n\in\mathbb{N}}$ of flat counter systems representing an increasing number of runs of $\mathcal{S}$. Flat model checking can hence be understood as verifying the $n$th system in this series providing the computational benefits of flatness in the concrete case. As mentioned earlier, this is similar to bounded model checking, where the approximation is prefix-based and represents only a finite number of runs.

3 Model Checking $\mathsf{CLTL}$ over Flat Counter Systems

This section is dedicated to lifting the technique for model-checking $\mathsf{fLTL}$ over flat Kripke structures [13] to $\mathsf{CLTL}$ and flat counter systems. The central aspect is the definition of augmented path schemas (APS) and the notion of consistency. We observe that consistent APS are suitable witnesses for runs because they are of bounded size and exist if a formula is satisfied. The QPA encoding of the flat-model-checking problem presented in Section 4 builds on these definitions. To simplify notation, we fix in this section a counter system $\mathcal{S}=(S_{\mathcal{S}},\Delta_{\mathcal{S}},s_{I},\lambda)$ and a $\mathsf{CLTL}$ formula $\Phi$, both over counters $C_{\mathcal{S}}$. Augmented path schemas [13] extend path schemas by a labelling that provides additional information, as well as counters and guards to constrain the set of runs of an APS beyond a specific shape. The following definition extends that of [13] to take the counters and guards of $\mathcal{S}$ into account. See Fig. 1 for an example.

Definition 2 (APS)

An augmented path schema (APS) in $\mathcal{S}$ is a structure $\mathcal{P}=(Q,\Delta_{\mathcal{P}},\lambda_{\mathcal{P}},\mathrm{org})$ where

• •

$(Q,\Delta_{\mathcal{P}},q_{0},\lambda_{\mathcal{P}})$ is a flat counter system over $Q=\{q_{0},\ldots,q_{n}\}$, for some $n\in\mathbb{N}$, with labelling $\lambda_{\mathcal{P}}:Q\to 2^{\mathrm{sub}(\Phi)\cup AP}$ and simple path $q_{0}\ldots q_{n}$;

• •

$\mathrm{org}:Q\to S_{\mathcal{S}}$ maps every state to an origin such that $\lambda_{\mathcal{P}}(q)\cap AP=\lambda_{\mathcal{S}}(\mathrm{org}(q))\cap AP$ and $\mathrm{org}(q_{0})=s_{I}$;

• •

for each transition $(q,\mu,\Gamma,q^{\prime})\in\Delta_{\mathcal{P}}$ there is $(\mathrm{org}(q),\hat{\mu},\hat{\Gamma},\mathrm{org}(q^{\prime}))\in\Delta_{\mathcal{S}}$ with $\hat{\Gamma}\subseteq\Gamma$ and $\hat{\mu}(c)=\mu(c)$ for all $c\in C_{\mathcal{S}}$;

• •

$\Delta_{\mathcal{P}}=\Delta_{\text{fwd}}\operatorname{\dot{\cup}}\Delta_{\text{bwd}}$ is comprised of forward- and backward transitions where

• –

$\Delta_{\text{fwd}}=\{(q_{0},\mu_{0},\Gamma_{0},q_{1}),\ldots,(q_{n-1},\mu_{n-1},\Gamma_{n-1},q_{n})\}$,

• –

there is $(q_{n},\mu_{n},\Gamma_{n},q_{n^{\prime}})\in\Delta_{\text{bwd}}$, for $n^{\prime}\leq n$, closing the last loop, and

• –

for all $(q_{j},\mu,\Gamma,q_{i}),(q_{k},\mu^{\prime},\Gamma^{\prime},q_{h})\in\Delta_{\text{bwd}}$ we have $i\leq j$, $h\leq k$, and the corresponding loops $q_{h}q_{h+1}\ldots q_{k}$ and $q_{i}q_{i+1}\ldots q_{j}$ are disjoint; and

• •

for each loop $L=q_{i}q_{i+1}\ldots q_{i+\ell}$ there is a front row $F=q_{i-\ell-1}\ldots q_{i-1}$ and, if $i+\ell<n$, a rear row $R=q_{i+\ell+1}\ldots q_{i+2\ell+1}$ with identical labelling $\lambda_{\mathcal{P}}(q_{i-\ell-1})\ldots\lambda_{\mathcal{P}}(q_{i-1})=\lambda_{\mathcal{P}}(q_{i})\ldots\lambda_{\mathcal{P}}(q_{i+\ell})=\lambda_{\mathcal{P}}(q_{i+\ell+1})\ldots\lambda_{\mathcal{P}}(q_{i+2\ell+1})$.

The paths, loops, rows, and runs of $\mathcal{P}$ are those of the underlying counter system where the latter are restricted to those visiting the last state $q_{n}$ of $\mathcal{P}$. The mapping $\mathrm{org}$ is lifted from states to paths and runs as expected, restricting the valuations to the counters $C_{\mathcal{S}}$ of $\mathcal{S}$. Then, for every run $\rho$ of $\mathcal{P}$, the sequence $\mathrm{org}(\rho)$ is a run of $\mathcal{S}$ starting in $\mathrm{org}(q_{I})=s_{I}$. We denote by $\mathrm{lastl}(\mathcal{P}):=q_{n^{\prime}}\ldots q_{n}$ the last loop of $\mathcal{P}$. Observe that the definition requires each loop to be preceded and (except for $\mathrm{lastl}(\mathcal{P})$) succeeded by state sequences that may be considered as an unfolding regarding the labelling sequence. These front and rear rows are needed for technical reasons to cover edge-cases in reasoning on the first and last loop iteration, respectively.

We are interested in APS that provide a semantically correct labelling because they allow us to reason syntactically on where a particular formula is satisfied.

Definition 3 (Correctness)

A state $q\in Q$ of an APS $\mathcal{P}$ is correctly labelled with respect to a $\mathsf{CLTL}$ formula $\varphi\in\mathrm{sub}(\Phi)$ if for all runs $\rho=(q_{0},\theta_{0})(q_{1},\theta_{1})\ldots\in\mathrm{runs}(\mathcal{P})$ and all positions $x\in\mathbb{N}$ with $q_{x}=q$ we have $(\mathcal{S},\mathrm{org}(\rho),x)\models\varphi\Leftrightarrow\varphi\in\lambda_{\mathcal{P}}(q)$.

This notion is very strict in the sense that the annotation must always be in line with the $\mathsf{CLTL}$ semantics. Observe that there may not even exist a correct labelling for a particular state: if the latter resides on a loop it may occur more than once on some run and a formula $\Phi$ may hold at one of them but not at the other (e.g., because $\Phi$ imposes a minimal number of iterations to follow). However, an APS in $\mathcal{S}$ that is actually correctly labelled witnesses the existence of a run satisfying $\Phi$ in case it is non-empty and its initial state is labelled by $\Phi$. In [13], the syntactic criterion called consistency was introduced in order to characterise APS that are labelled correctly with respect to $\mathsf{fLTL}$ formulae. We generalise the definition and the results to $\mathsf{CLTL}$, i.e., from relative frequencies to arbitrary linear constraints and from Kripke structures to counter systems.

Consider an APS $\mathcal{P}=(Q,\Delta_{\mathcal{P}},\lambda_{\mathcal{P}},\mathrm{org})$ using counters $C_{\mathcal{P}}\supseteq C_{\mathcal{S}}$ where $q_{0}\ldots q_{n}$ is the unique simple path traversing all states of $\mathcal{P}$. The criterion distinguishes the syntactical forms of a $\mathsf{CLTL}$ formula based on the top most operator and identifies for each case syntactical conditions that certify satisfaction or violation of a corresponding formula. Further subordinate cases formulate individual conditions to matching the various situations that may apply to a control state, e.g., whether it is on a loop or not. Before presenting the formal definition, let us discuss the rationale of the individual conditions.

3.0.1 Consistency for non-until formulae.

The simplest case is that of propositions, because these labels are correct by definition. Recall that constraints $\gamma\in\mathfrak{C}(C_{\mathcal{S}})$ over system counters, e.g. $c_{1}-2c_{2}\geq 0$, are not only valid atomic $\mathsf{CLTL}$ formulae but also valid transition guards. Therefore, the reasoning on their satisfaction can directly be moved to the level of the counter system. If all incoming transitions of a state $q\in Q$ are guarded by some constraint $\gamma$, then every valid run necessarily satisfies it whenever visiting $q$. Similarly, if these transitions are guarded by the dual constraint $\overline{\gamma}$, then $\gamma$ can not hold at any occurrence of $q$ on any run.

If $\Phi$ is a Boolean combination, correctness can be established locally for any state $q$ when inductively assuming that $q$ is labelled correctly by all the strict subformulae. For example, a negation $\neg\varphi$ holds on all runs at all positions of a state $q$ if and only if on all runs $\varphi$ does not hold at $q$. With the assumption that the labelling with respect to $\varphi$ is correct, labelling $q$ by $\neg\varphi$ is correct if and only if $q$ is not labelled by $\varphi$, and vice versa. Similar reasoning applies to conjunctions and the temporal operator $\operatorname{\mathrm{\mathbf{X}}}$.

3.0.2 Consistency for until formulae using balance counters.

For counted until formulae, we also make use of the counting capabilities of the system model, although the reasoning is more involved. Consider $\Phi$ to have the form $\varphi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi$, and let $q,q^{\prime}\in Q$ be row states such that $q^{\prime}\in\mathrm{suc}_{\mathcal{\mathcal{P}}}^{*}(q)$ is a successor of $q$ and (correctly) labelled by $\psi$. Assume that the states in-between $q$ and $q^{\prime}$ are correctly labelled by $\varphi$. In order to establish that $\Phi$ holds at state $q$ on any run, it remains to enforce the counting constraint on the intermediate segment. To this end, also assume that $\mathcal{P}$ features a counter $c_{\tau,q}$ that tracks the value of the term $\tau$ as a balance that starts with zero at $q$ and is updated according to the effect that each individual state would have on the value of $\tau$. For example, if $\tau=p_{1}-2p_{2}$, then the counter is updated by $+1$ on every outgoing transition of a state labelled by $p_{1}$, because this is what each such state contributes to the term value. The counter would be update by $-2$ on the outgoing transitions, if the state is labelled by $p_{2}$, and consequently by $1-2=-1$ if it carries both labels. Then, upon reaching $q^{\prime}$ along some run, the counter $c_{\tau,q}$ would hold precisely the value of the counting term $\tau$ evaluated on the intermediate path taken from $q$ to $q^{\prime}$. If the incoming (forward) transition of $q^{\prime}$ is now labelled by the guard $c_{t,q}\geq b$, then $\Phi$ can be assumed to hold whenever a valid run visits $q$ because $q^{\prime}$ is certainly visited and will then serve as witness. Dually, if all such potential witness states $q^{\prime}$ are guarded instead by the dual constraint $c_{t,q}<b$, then there is no way a valid run could satisfy $\Phi$ when visiting $q$.

Definition 4 (Balance counter)

Let $\mathcal{P}=(Q,\Delta_{\mathcal{P}},\lambda_{\mathcal{P}},\mathrm{org})$ be an APS in $\mathcal{S}$ with counters $C_{\mathcal{P}}$. Let $\tau$ be a constraint term over $\mathrm{sub}(\Phi)$, and $q\in Q$ a row state in $\mathcal{P}$. A balance counter for $\tau$ and $q$ in $\mathcal{P}$ is a counter $c_{\tau,q}\in C_{\mathcal{P}}$ that is updated, on all transitions $(q_{1},\mu,\Gamma,q_{2})\in\Delta_{\mathcal{P}}$, by

[TABLE]

In combination with appropriately guarded states, balance counters allow us to reason syntactically about the satisfaction of $\Phi$. Such counters are particularly useful to track the value of a term across an entire loop, even if some runs of $\mathcal{P}$ iterate it more often than others.

3.0.3 Static consistency conditions for until formulae.

If there is no entire loop between two states $q$ and $q^{\prime}$, using a counter is still possible but not necessary. Each run passes precisely once the (unique) path between $q$ and $q^{\prime}$, so whether or not $q^{\prime}$ witnesses satisfaction of $\Phi$ at $q$ can be determined statically, independently of the precise course of the run in other parts. While the existence of a balance counter and appropriate guards imply that a formula is satisfied, it would be too restrictive to consider this as only option. There are situations where satisfaction of a formula can not be witnessed by a balance counter. For example, if a witness state $q^{\prime}$ is part of a loop, a corresponding guard may be satisfied at one of its occurrences on a run but not at all of them. While the consistency criterion is intended to be strong enough to imply correctness, it shall also admit a sufficiently large class of APS to represent all reasons for satisfaction (and violation). Therefore, the definition admits also the static reasoning.

A further case treated explicitly concerns the effect of the last loop. If traversing it once exhibits a positive effect on the evaluation of $\tau$, then it dominates the effects of all other loops, since it is traversed infinitely often. Therefore, if it can be reached from $q$ and traversed once without violating $\varphi$, and contains some witness state labelled by $\psi$, then $\Phi$ is necessarily satisfied when a run reaches $q$.

Finally, the last case considered by the consistency criterion is concerned with the satisfaction of $\Phi$ when visiting states that are situated directly on a loops: If $\Phi$ holds at the first occurrence of a state $q$ on a run and at the last, then the formula holds also at all occurrences of $q$ in-between. The reason is, essentially, that the effect of one iteration of a loop on the value of the term $\tau$ is always the same (at least, if the labelling by all subformulae is correct, as we have assumed). Therefore, the worst (i.e., smallest) value of $\tau$ is encountered either in the first or the last iteration. Augmented path schemas are defined to feature for each loop a preceding and a succeeding row that are exact copies and can be considered as unfoldings. Hence, if these are correctly labelled with respect to $\Phi$, then the loop labelling inherits their correctness.

Using the above reasoning, it can be shown that the following definition of consistency is a sufficient criterion for correctness. It extends that of [13] to the present context and accounts for the various subtleties arising from the different cases.

Definition 5 (Consistency)

Let $\mathcal{P}=(Q,\Delta_{\mathcal{P}},\lambda_{\mathcal{P}},\mathrm{org})$ be an APS in $\mathcal{S}$ with $|Q|=n$, simple path $q_{0}\ldots q_{n-1}$, and $\varphi$ a $\mathsf{CLTL}$ formula. A state $q_{i}\in Q$ is $\varphi$-consistent if $\varphi\in AP$ is an atomic proposition or

1. (A)

$\varphi=(\tau\geq b)\in\mathfrak{C}(C)$, all incoming transitions $(q,\mu,\Gamma,q_{i})\in\Delta_{\mathcal{P}}$ are guarded by $\varphi\in\Gamma$ if $\varphi\in\lambda_{\mathcal{P}}(q_{i})$ and by $\overline{\varphi}\in\Gamma$ otherwise, and if $i=0$, then $\varphi\in\lambda_{\mathcal{P}}(q_{i})\Leftrightarrow 0\geq b$.

For non-atomic formulae $\varphi$, the state $q_{i}$ is $\varphi$-consistent if for all $\psi\in\mathrm{sub}(\varphi)\setminus\{\varphi\}$ all states $q\in Q$ are $\psi$-consistent and one of the following Items B, C and D applies.

1. (B)

$\varphi=\chi\land\psi$ and $\varphi\in\lambda_{\mathcal{P}}(q_{i})\Leftrightarrow\chi,\psi\in\lambda_{\mathcal{P}}(q_{i})$; or $\varphi=\neg\psi$ and $\neg\psi\in\lambda_{\mathcal{P}}(q_{i})\Leftrightarrow\psi\not\in\lambda_{\mathcal{P}}(q_{i})$. 2. (C)

$\varphi=\operatorname{\mathrm{\mathbf{X}}}\psi$ and $\operatorname{\mathrm{\mathbf{X}}}\psi\in\lambda_{\mathcal{P}}(q_{i})\Leftrightarrow\psi\in\lambda_{\mathcal{P}}(q)$, for all $q\in\mathrm{suc}_{\mathcal{\mathcal{P}}}(q_{i})$. 3. (D)

$\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi$ and one of the following holds:

$\varphi\in\lambda_{\mathcal{P}}(q_{i})$, $\llbracket\tau\rrbracket(\lambda_{\mathcal{P}}^{\#}(\mathrm{lastl}(\mathcal{P}))>0$, $\psi\in\lambda_{\mathcal{P}}(q)$ for some $q\in\mathrm{lastl}(\mathcal{P})$, and $\chi\in\lambda_{\mathcal{P}}(q^{\prime})$ for all $q^{\prime}\in\mathrm{suc}_{\mathcal{\mathcal{P}}}^{*}(q_{i})$. 2. 2.

The state $q_{i}$ is not part of a loop. If $\varphi\not\in\lambda_{\mathcal{P}}(q_{i})$, then $\psi\not\in\lambda_{\mathcal{P}}(q_{i})$ or $0<b$. Further, if $\varphi\not\in\lambda_{\mathcal{P}}(q_{i})$, then

1. (i)

there is some $k\geq i$ such that $\chi\not\in\lambda_{\mathcal{P}}(q_{k})$ and, for each $j\in[i,k]$, $|\mathrm{suc}_{\mathcal{\mathcal{P}}}(q_{j})|=1$ and $\psi\in\lambda_{\mathcal{P}}(q_{j})\Rightarrow\llbracket\tau\rrbracket(\lambda_{\mathcal{P}}^{\#}(q_{i}\ldots q_{j-1}))<b$ or 2. (ii)

$\mathcal{P}$ contains a balance counter $c_{\tau,i}\in C_{\mathcal{P}}$ for $\tau$ and $q_{i}$, and the guard $(c_{\tau,i}<b)\in\Gamma$ for all $(q,\mu,\Gamma,q_{j})\in\Delta_{\mathcal{P}}$ where $j>i$, $\psi\in\lambda_{\mathcal{P}}(q_{j})$, and $\forall_{k\in[i,j-1]}:\chi\in\lambda_{\mathcal{P}}(q_{k})$.

If $\varphi\in\lambda_{\mathcal{P}}(q_{i})$, then there is $k\geq i$ with $\psi\in\lambda_{\mathcal{P}}(q_{k})$, $\forall_{j\in[i,k-1]}:\chi\in\lambda_{\mathcal{P}}(q_{j})$, and

1. (iii)

$\llbracket\tau\rrbracket(\lambda_{\mathcal{P}}^{\#}(q_{i}\ldots q_{k-1}))\geq b$ and $\forall_{j\in[i,k-1]}:|\mathrm{suc}_{\mathcal{\mathcal{P}}}(q_{j})|=1$, or 2. (iv)

$k>i$ and $\mathcal{P}$ contains a balance counter $c_{\tau,i}\in C_{\mathcal{P}}$ for $\tau$ and $q_{i}$, and the unique transition from $q_{k-1}$ to $q_{k}$ has the form $(q_{k-1},\mu,\Gamma\cup\{c_{\tau,i}\geq b\},q_{k})\in\Delta_{\mathcal{P}}$. 3. 3.

$q_{i}$ is on some loop $L$ of $\mathcal{P}$, and $q_{i-|L|}$ and $q_{i+|L|}$ (if $L\neq\mathrm{lastl}(\mathcal{P})$) are $\varphi$-consistent.

The APS $\mathcal{P}$, a loop, or a row in $\mathcal{P}$ are $\varphi$-consistent if all their states are $\varphi$-consistent, respectively.

Using a structural induction on a $\mathsf{CLTL}$ formula $\varphi$ we can show that if some state of an APS is $\varphi$-consistent, then the state is correctly labelled by that formula. The base cases those of atomic propositions and guards, concerning Item A of Definition 5. The remaining conditions cover the inductive cases for the potential shape of $\varphi$ and rely on the fact that the definition demands all states to be consistent with respect to each strict subformula of $\varphi$. The proof relies on a thorough investigation of each syntactic case in combination with various specific situations that states can be found in, as discussed above. It has to deal with the sometimes quite subtle interplay between temporal counting constraints and iterated loops and we omit the technicalities of the proof here in favour of conciseness.

Theorem 3.1 (Correctness)

If a state $q$ of an APS $\mathcal{P}$ in $\mathcal{S}$ is $\varphi$-consistent, then it is labelled correctly with respect to $\varphi$.

Consequently, a non-empty APS in $\mathcal{S}$ of which the initial state is $\Phi$-consistent and labelled by $\Phi$ witnesses that $\mathcal{S}\models\Phi$.

3.0.4 Existence of consistent APS in flat systems.

Although consistency imposes a very specific shape, it can be shown that for a significant class of systems there is always a $\Phi$-consistent APS (of bounded size) if the formula $\Phi$ is satisified. The construction for $\mathsf{fLTL}$ over flat Kripke structures [13] extends with Definition 5 to $\mathsf{CLTL}$.

Assume $\mathcal{S}$ is flat and let $\sigma\in\mathrm{runs}(\mathcal{S})$ be a run that satisfies $\Phi$. In the following we sketch how to construct a $\Phi$-consistent APS in $\mathcal{S}$ that contains (a representation of) $\sigma$ and is thus labelled by $\Phi$ at its initial state. It is known that each path in a flat structure can be represented by some path schema of linear size [2, 15]. Hence, let $\mathcal{P}$ be an APS containing a run $\rho\in\mathrm{runs}(\mathcal{P})$ with $\mathrm{org}_{\mathcal{P}}(\rho)=\sigma$ and thus satisfying $\Phi$. The states of this APS can now recursively be labelled by the subformulae of $\Phi$ as semantically determined by $\rho$.

The conditions of Definition 5 can be realised for $\Phi$ under the assumption, that the labelling has been completed for each strict subformula. The construction distinguishes which case applies to $\Phi$. If $\Phi$ is an atomic proposition, nothing needs to be done since the labelling is consistent by definition. Boolean combinations can be realised by simply adjusting the labelling locally for each state of $\mathcal{P}$, e.g., including $\Phi=\neg\varphi$ in the labelling of a state if and only if it is not labelled by $\varphi$. Assume $\Phi$ has the form $\operatorname{\mathrm{\mathbf{X}}}\varphi$. Depending on whether the successor states of a state $q$ are labelled by $\varphi$ or not, $q$ is labelled by $\operatorname{\mathrm{\mathbf{X}}}\varphi$ or not. Notice that all successors of a state have the same labelling because either there is only one or the state is the last state of some loop. In the latter case, the successors are the first states of the loop and its rear copy and thus share the same labelling (cf. Definition 2).

For the remaining types of formulae, i.e., until formulae and constraints over system counters, the structure of $\mathcal{P}$ may have to be altered, in order to provide a consistent labelling and to retain a valid run $\rho$ (as representation of $\sigma$). The essential difficulties concern loop states because these may occur at more than one position on $\rho$. A subformula $\varphi$ may then be satisfied at some, but not all of these positions. For example, consistency for a constraint formula $\gamma=\tau\geq b$ and a state $q$ demands to add $\gamma$ or its dual to every incoming transition of $q$, depending on whether we want to label it by $\gamma$ or not. Clearly, the guards can simply be added and this would settle consistency. However, if $\gamma$ is satisfied at one occurrence of $q$ on $\rho$ but not at another, the guards would be violated at one of these positions and $\rho$ would not be valid anymore. To establish consistency for until formulae, we may have to add a fresh balance counter to the system and similar issues may arise. It may therefore be necessary to introduce copies of a state in order to distinguish the positions of the state and label them differently in the APS. The important observation is that during the iteration of a loop the validity of a formula $\varphi$ at some state switches at most once, assuming the APS is labelled consistently by all subformulae already. Therefore, loops may have to be duplicated once for each subformula, one copy where on all iterations $\varphi$ holds and one where it does not. The recursive labelling procedure may therefore increase the size of $\mathcal{P}$ exponentially.

Theorem 3.2 (Existence)

If $\mathcal{S}$ is flat and $\mathcal{S}\models\Phi$ then there is a non-empty and $\Phi$-consistent APS in $\mathcal{S}$ with initial state labelled by $\Phi$ and of at most exponential size in $\mathcal{S}$ and $\Phi$.

Notice that, even if $\mathcal{S}$ is not flat, each run contained in the flat approximation $\mathsf{FA}(\mathcal{S},n)$ of $\mathcal{S}$ can by definition be represented by an APS in $\mathcal{S}$ of size $n$. Therefore, the construction applied to $\mathsf{FA}(\mathcal{S},n)$ also yields an exponential witness.

Corollary 1

If $\mathsf{FA}(\mathcal{S},n)\models\Phi$ then there is a non-empty and $\Phi$-consistent APS in $\mathcal{S}$ with initial state labelled by $\Phi$ and of at most exponential size in $n$ and $\Phi$.

4 From Flat Model Checking to Presburger Arithmetic

For solving the flat model-checking problem of a counter system $\mathcal{S}=(S,\Delta,s_{I},\lambda)$ over counters $C_{\mathcal{S}}$ and a $\mathsf{CLTL}(C_{\mathcal{S}})$ formula $\Phi$, the developments in the previous section devise the search for an augmented path schema $\mathcal{P}$ in $\mathcal{S}$ that is $\Phi$-consistent, labelled initially by $\Phi$ and non-empty. In the following we sketch 222Details are presented in Appendix 0.A. a formulation of this search in quantifier-free Presburger arithmetic, aiming at an SMT-based implementation.

The idea is to encode an APS of size $n\in\mathbb{N}$ and a run of it as valuation of a set of first-order variables. We construct a formula $\mathrm{fmc}(\mathcal{S},\Phi,n)$ that is satisfiable if there is a run $\rho\in\mathsf{FA}(\mathcal{S},n)$ satisfying $\Phi$ and such that any solution represents a valid witness that $\mathcal{S}\models\Phi$. Without restriction, we need only to represent APS $\mathcal{P}=(Q,\Delta_{\mathcal{P}},\lambda_{\mathcal{P}},\mathrm{org})$ where the states are natural numbers $Q=[0,n-1]$. The natural ordering implicitly determines the unique maximal simple path in $\mathcal{P}$. It hence suffices to encode explicitly the beginning and end of loops, the origin and labelling of each state, as well as a valid run. Further, the formula expresses the satisfaction of all encountered guards and the consistency criterion.

For convenience, we use not only first-order variables for integer numbers but also boolean, enumeration and natural number types (sorts). They can, theoretically, be encoded into integers but are more readable and directly supported by, e.g., the z3 SMT solver. We use notation of the form $\mathsf{var}:X$ to denote that some variable symbol $\mathsf{var}$ is of some sort $X$. Mappings with some finite domain $Y$ can be represented by variable vectors of length $|Y|$ that we denote concisely by single variable symbols $\mathsf{var}:X^{Y}$. The shorthand $\mathrm{ite}(\mathrm{cond},\mathrm{prop},\mathrm{alt})$ represents the if-then-else construct. Figure 2 depicts an example of an APS $\mathcal{P}$ and its representation in terms of first-order variables and their valuation. For every state $i\in Q$, we encode the positions of loops in terms of a variable \mathsf{typ}_{i}:\{{\raisebox{-0.3pt}{\scalebox{0.8}{\boxminus}}},\triangleright,{\raisebox{-0.3pt}{\scalebox{0.8}{\boxplus}}},\triangleleft\} that indicates whether it is outside (

$\boxminus$

), inside (

$\boxplus$

), the beginning ($\triangleright$), or the end ($\triangleleft$) of a loop. We use $\diamond_{i}$ to abbreviate $\mathsf{typ}_{i}=\diamond$ for \diamond\in\{{\raisebox{-0.3pt}{\scalebox{0.8}{\boxminus}}},\triangleright,{\raisebox{-0.3pt}{\scalebox{0.8}{\boxplus}}},\triangleleft\}. The origin is represented by a variable $\mathsf{org}_{i}:S$ and the labelling by $\mathsf{lbl}_{i}:\{0,1\}^{\mathrm{sub}(\Phi)}$, describing the set $\lambda_{\mathcal{P}}(i)\subseteq\mathrm{sub}(\Phi)$. The formula

[TABLE]

specifies the shape of $\mathcal{P}$, a run and that the initial state is labelled by $\Phi$. The formula components are discussed next.

4.0.1 Basic structure of APS.

The basic structure is easily specified as QPA formula $\mathrm{aps}(\mathcal{S},n)$. It states that $s_{I}$ is the origin of the first state ($\mathsf{org}_{0}=s_{I}$), that loops are delimited by $\triangleright$ and $\triangleleft$, and that the labelling of states by propositions coincides with that of $\mathcal{S}$.

A way to express that the backward transitions from the last to the first state of the loops has a correspondence in $\mathcal{S}$ is to build a constraint over all pairs of states from $Q$. This is, however, quadratic in $n$ and we therefore use a propagation scheme introducing $n$ additional variables $\mathsf{orgAtEnd}_{i}:S$. We let them equal $\mathsf{org}_{i}$ where $\mathsf{typ}_{i}=\triangleleft$ and otherwise be copied from $\mathsf{orgAtEnd}_{i+1}$, thus propagating backward the origin of the last state of every loop. The formula $\bigwedge_{i=0}^{n-1}\,\triangleright_{i}\to\bigvee_{(s,\mu,\Gamma,s^{\prime})\in\Delta}\mathsf{orgAtEnd}_{i}{=}s\land\mathsf{org}_{i}{=}s^{\prime}$ then guarantees that all backward transitions exist in $\mathcal{S}$. Forward transitions are specified similarly. We assume a minimal loop length of $2$ due to distinct positions for the first ($\triangleright$) and the last ($\triangleleft$) state of each loop but single-state loops can still be represented (cf. Fig. 2) while increasing the upper bound for the size of path schemas only by one state per loop. Definition 2 demands that loops be surrounded by identical rows which are not represented explicitly in the encoding. Instead, runs are required to traverse each representation of a loop at least three times, the first representing the front, the last representing the rear and the remaining representing the actual loop traversals. The construction distinguishes between the first, second, and last iteration where necessary.

To allow for a simplified presentation, let us assume that there is at most one transition between every two states of $\mathcal{S}$, thus being uniquely identified by $\mathsf{org}_{i}$ and $\mathsf{org}_{i+1}$. The assumption could be eliminated by adding $2n$ additional variables determining explicitly which transition is selected for the represented APS.

4.0.2 Runs.

The formula $\mathrm{run}(\mathcal{S},n)$ specifies the shape and constraints of a run in the encoded schema. Variables $\mathsf{itr}_{i}:\mathbb{N}$ indicate how often state $i\in Q$ is visited and are thus constraint to equal $1$ outside loops and to stay constant inside each loop. Infinite iteration of the last loop is represented by the otherwise unused value [math].

To ensure that the represented run is valid it has to satisfy all the guards at any time. The variables $\mathsf{valFst}_{i},\mathsf{valSec}_{i},\mathsf{valLst}_{i}:\mathbb{Z}_{\infty}^{C_{\mathcal{S}}}$ hold the counter valuations at state $i\in Q$ when the represented run visits it for the first, the second and the last time, respectively. Due to flatness each loop is entered and left only once. Since the guards of the counter system are linear inequalities and the updates are constant, it suffices to check them in the first and last iteration of a loop. For a term $\tau=\sum_{j=0}^{\ell}a_{j}c_{j}$ and a variable symbol $\mathsf{var}:\mathbb{Z}^{C_{\mathcal{S}}}$ let $\tau[\mathsf{var}]:=\sum_{j=0}^{\ell}a_{j}\cdot\mathsf{var}(c_{j})$ denote the substitution of the counter names by the variable symbol (representing the value of) $\mathsf{var}(c_{j})$. The formula

[TABLE]

then specifies that the encoded run satisfies the guards whenever taking a forward transition. Notice that the (forward) transition from state $i-1$ to state $i$ is not taken at the beginning of the last iteration of a loop and thus, its guard must not be checked for the corresponding valuation. Instead, the guards of the backward transition pointing to $i$ must be satisfied from the second iteration on, and are expressed similarly.

It remains to actually specify the counter valuations along the run. By definition, $\mathsf{valFst}_{0}=\mathbf{0}$. Outside of loops (

$\boxminus$

) we impose $\mathsf{valFst}_{i}=\mathsf{valSec}_{i}=\mathsf{valLst}_{i}=\mathsf{valLst}_{i-1}+\mu$ where $\mu$ is the update of the transition from $i-1$ to $i$. Inside ({\raisebox{-0.3pt}{\scalebox{0.8}{\boxplus}}},\triangleleft) we let $\mathsf{valFst}_{i}=\mathsf{valFst}_{i-1}+\mu$, $\mathsf{valSec}_{i}=\mathsf{valSec}_{i-1}+\mu$ and $\mathsf{valLst}_{i}=\mathsf{valLst}_{i-1}+\mu$. At the beginning ($\triangleright$) of a loop the value in the first iteration is propagated as outside ($\mathsf{valFst}_{i}=\mathsf{valLst}_{i-1}+\mu$), but for the second iteration we impose $\mathsf{valSec}_{i}=\mathsf{valFstAtEnd}_{i}+\mu$ where $\mu$ comes from the incoming backward transition and is applied to the last value of the previous iteration propagated as above using variables $\mathsf{valFstAtEnd}_{i}$.

Having a direct handle on the valuations in the first and second iteration (in terms of the variables $\mathsf{valFst}_{i}$ and $\mathsf{valSec}_{i}$) as well as the total number of loop iterations ($\mathsf{itr}_{i}$), it is tempting to specify the valuations in the last iteration simply by

[TABLE]

Unfortunately, this formula uses multiplication of variables and hence exceeds Presburger arithmetic. Instead, the updates over the second to last loop iteration are accumulated in an explicit variable $\mathsf{lUpd}_{i}$ such that $\mathsf{valLst}_{i}$ can be set to $\mathsf{valFst}_{i}+\mathsf{lUpd}_{i}$. We express this accumulation by the formula

[TABLE]

Essentially, the multiplication by $\mathsf{itr}_{i}$ is distributed over the individual transition updates along the loop. This is admissible because the individual updates $\mu$ appear in the formula not as variables but as constants. In the formulation above, $\mathsf{lUpd}_{i}$ is always zero for states $i$ on the last loop but this is no problem because this particular situation can be handled using $\mathsf{valFst}_{i}$ and $\mathsf{valSec}_{i}$. Observe also that the variable $\mathsf{lUpd}_{i}$ holds only intermediate results inside and at the end of loops and is undefined outside. Only for states $i$ that are the beginning of a loop, it holds the precise accumulated loop effect and this value is used for propagation as above.

Using $\mathsf{lUpd}_{i}$, the calculation of the valuations in the last iteration of a loop is now specified by $\mathsf{valLst}_{i}=\mathsf{valFst}_{i}+\mathsf{lUpd}_{i}$. In the infinitely repeated last loop of the schema, there is no actual last iteration, but the variables are nevertheless used to indicate the limit behaviour by specifying

[TABLE]

4.0.3 Consistency.

The formulae constructed above describe a non-empty augmented path schema in $\mathcal{S}$ of which the first state is labelled by $\Phi$. In the following, we develop the components of the formula $\mathrm{consistency}(\mathcal{S},n,\Phi)$ expressing the different cases of Definition 5. Consistency for Boolean combinations (Item B) can almost literally be translated to QPA. Concerning Item A, constraints of the form $\tau\geq b$ are not modelled explicitly. Rather, the formula

[TABLE]

imposes for each $i$ that the represented run satisfies the constraints as if they were guards on all incoming transitions on any state labelled by an atomic constraint. To express Item C, variables $\mathsf{lblAtBeg}_{i}:2^{\mathrm{sub}(\Phi)}$ propagate labelling information from the start of a loop towards the end. The condition for formulae $\operatorname{\mathrm{\mathbf{X}}}\varphi\in\mathrm{sub}(\Phi)$ is then specified by $(\operatorname{\mathrm{\mathbf{X}}}\varphi\in\mathsf{lbl}_{n-1}\leftrightarrow\varphi\in\mathsf{lblAtBeg}_{n-1})$ and for $0\leq i\leq n-2$ by

[TABLE]

Until Item D1.

Consider a formula $\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi\in\mathrm{sub}(\Phi)$. We first set up some propagations to be able to express Item D1. To access the accumulated value of $\tau$ on a single iteration of the last loop we introduce variables $\mathsf{acc}_{i}^{\tau}$ for $i\in Q$. Let the formula $\mathrm{accu}(n,\tau)$ be defined as

[TABLE]

It implies that $\mathsf{acc}_{0}^{\tau}$ holds the effect of the last loop on the value of $\tau$. Item D1 requires that $\chi$ holds globally at all reachable states. For loop states this concerns not only larger states (with respect to $\geq$). The whole loop must be labelled by $\chi$. Using variables $\mathsf{prpg}_{i}^{\chi}$ and $\mathsf{glob}_{i}^{\chi}$ for $i\in Q$ the formula

[TABLE]

propagates this information through the structure by implying that $\mathsf{glob}_{i}^{\chi}$ is true if and only if $\chi$ is labelled at all states reachable from $i$. The information whether $\psi$ holds somewhere on the last loop is made available in terms of the variable $\mathsf{onLast}^{\psi}$ by

[TABLE]

Then, condition (D1) is expressed by

[TABLE]

Until Item D2.

Item D2 demands the existence or absence of a witness state proving that $\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi$ holds. As before, it would be inefficient to model balance counters and the guards required by the criterion explicitly. Instead, a formulation is developed that assures that the encoded APS can be assumed to have the necessary counters and guards. For example, assume some state $i$ is to be labelled by $\varphi$ and consider the best (maximal) value of the term $\tau$ on a path starting at state $i$ and leading to some state satisfying $\psi$, without violating $\chi$ in between. If that value is at least $b$, then there is a state at which a balance counter $c_{\tau,i}$ for $i$ and $\tau$ would have precisely that value and checking the constraint $c_{\tau,i}\geq b$ would succeed. On the other hand, if the best value is below $b$, then there is no such state. Even, the dual constraint could be added to any potential witness state and the encoded run would still be valid.

We introduce variables $\mathsf{maxFst}_{i}^{\varphi}:\mathbb{Z}_{\infty}$ and $\mathsf{maxLst}_{i}^{\varphi}:\mathbb{Z}_{\infty}$ for each $i\in Q$. For the first and last occurrence of state $i$, respectively, they are supposed to hold the maximal value possibly witnessing satisfaction of the constraint, the symbolic value $-\infty$ expressing non-existence. Recall that these positions represent only rows as the first and last iteration of loops represent their front and rear, respectively. Notice also that the latter value is not defined for positions belonging to the last loop. Then, Item D2 can be expressed for state $i$ in terms of the formula $\mathrm{con\ref{itm:consistency-U-counter}}(\varphi,i)$ defined as

[TABLE]

Maximal witness.

The optimal witness value is obtained by a suffix optimum backward propagation from the end to the start of the represented schema. Its QPA formulation $\mathrm{witnessMax}(n,\varphi)$ is comprised of three parts: the computation of the potentially propagated value, the calculation of the accumulated loop effect on the value of $\tau$ as necessary part of that, and the actual selection. Concerning the selection, the best value is propagated backwards, as long as $\chi$ holds. When the chain breaks, no witness position is properly reachable and the best value is set to $-\infty$. Each state of the schema where $\psi$ holds is a potential witness for preceding states. Thus, if the propagated value is less than [math], this state will generally provide a better value for $\tau$ than any of its successors. For example, for the case $\chi,\psi\in\mathsf{lbl}_{i}$ the formula specifies that $\mathsf{maxLst}_{i}^{\varphi}=\max(\mathsf{updLst}^{\varphi}_{i},0)$ where variables $\mathsf{updLst}^{\varphi}_{i}$ are assumed to hold the value propagated from state $i+1$.

The overall effect of (all iterations of) a loop on the value of $\tau$ is made accessible in terms of variables $\mathsf{sumEff}^{\tau}_{i}$ where $i$ is the first state of a loop. It is obtained by summing up the individual contribution $\tau[\mathsf{lbl}_{i}]\cdot(\mathsf{itr}_{i}-3)$ of each loop state $i$ bound to variables $\mathsf{eff}^{\tau}_{i}$. The effect is multiplied only by $\mathsf{itr}_{i}-3$ since the first (front), second (auxiliary), and last (rear) iteration is already accounted for explicitly. In order to circumvent multiplication of variables in the formula, the variables $\mathsf{eff}^{\tau}_{i}$ are themselves defined by distributing the factor ($\mathsf{itr}_{i}-3$) over the sum of monomials of the term $\tau$. Assuming $\tau$ to have the form $\tau=\sum_{k=0}^{m}a_{k}\chi_{k}$ the loop effect is hence specified by

[TABLE]

where the variables $\mathsf{eff}_{i}^{\tau}=\mathsf{eff}_{i}^{t,m}$ are to be considered identical. Then, we can formulate the actual computation of the (potentially) propagated optimum using

[TABLE]

To evaluate Items D(2)iii and D(2)i an additional set of auxiliary variables $\mathsf{maxAux}_{i}^{\varphi}$ and $\mathsf{updAux}_{i}^{\varphi}$ is used that represents, intuitively, the first real iteration of a loop. The maximal value is, effectively, propagated through the rear of the loop, then extrapolated over all iterations to the last position on the auxiliary iteration (by adding the accumulated loop effect) and finally through the front row. Since the value at the last state at the auxiliary iteration depends on that at the first state in the last iteration, the latter is propagated from the beginning to the end of the loop using variables $\mathsf{maxAuxAtBeg}^{\varphi}_{i}$, similar to the origin above.

Finally, the discussed parts can be combined to express consistency for a formula $\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi$ by

[TABLE]

The structure of the encoding assures that the actual loops are always identically labelled to their front and rear rows. Thus, by assuring those are consistent, all loops automatically satisfy Item D3. This completes the construction of the formula $\mathrm{consistency}(\mathcal{S},n,\Phi)$ and thereby that of $\mathrm{fmc}(\mathcal{S},n,\Phi)$.

4.0.4 Properties of the encoding.

A solution to $\mathrm{fmc}(\mathcal{S},\Phi,n)$ yields a $\Phi$-consistent APS in $\mathcal{S}$ and a run, implying by Theorem 3.1 that $\mathcal{S}\models\Phi$. Corollary 1 implies that if the flat approximation $\mathsf{FA}(\mathcal{S},n)$ contains any run satisfying $\Phi$, then $\mathrm{fmc}(\mathcal{S},\Phi,2^{p(n)})$ is satisfiable (for a fixed polynomial $p$) at latest.

Theorem 4.1

(i) *If $\mathrm{fmc}(\mathcal{S},\Phi,n)$ is satisfiable, then $\mathcal{S}\models\Phi$. * (ii) *If $\mathsf{FA}(\mathcal{S},n)\models\Phi$, then $\mathrm{fmc}(\mathcal{S},\Phi,2^{p(n)})$ is satisfiable. *

The encoding hence provides an effective means to solve the flat model-checking problem based on QPA satisfiability checking. A major concern of our construction is to keep the formula as small as possible. Examining the indexing scheme of variables, we observe that their number is linear in $|\Phi|+|\mathcal{S}|$ and $n$. The length of most parts of the formula $\textrm{fmc}(\mathcal{S},\Phi,n)$ only depends linearly on $n$ or $n\cdot|\Delta|\leq n\cdot|\mathcal{S}|$. The parts encoding the guards in $\mathcal{S}$ further depend (linearly) on the size of the guard sets associated to the transitions, more precisely, linearly on the total length of all guards. The components of $\mathrm{consistency}(\mathcal{S},n,\Phi)$ are of linear size in $n\cdot|\mathcal{S}|$ or $n\cdot|\mathrm{sub}(\Phi)|$. Those concerning atomic constraints and until formulae depend on the length of the constraint terms present in $\Phi$.

Theorem 4.2 (Formula size)

The length of $\mathrm{fmc}(\mathcal{S},\Phi,n)$ is in $\mathcal{O}(n(|\mathcal{S}|+|\Phi|))$.

5 Evaluation

In order to evaluate whether flat model checking and the QPA-based encoding can be used to perform verification tasks, we have implemented the procedure and applied it to a set of problems provided by the RERS Challenge [21].

The tool flat-checker333https://github.com/apirogov/flat-checker takes a $\mathsf{CLTL}$ specification, a counter system to be verified in DOT format [18] and the approximation depth (schema size) and performs the translation of the verification problem to a linear arithmetic formula. The SMT solver z3 [28] is used to compute a solution of the formula, if possible, that is subsequently interpreted as satisfying run and presented adequately to the user. The tool is developed in Haskell and provides a search mode that automatically increases the depth up to a given a bound, in order to potentially find a small witness quickly, before investing computation time in large depths. A successful search can be continued to find a witness of smallest depth.

The RERS Challenge 2017444http://www.rers-challenge.org/2017/ poses problems as C99 and Java programs that provide output depending on read input symbols and internal state. The programs have a regular structure but are inconceivable with reasonable effort. It features a track comprising 100 $\mathsf{LTL}$ formulas to be checked on a program (Problem 1) that is representable as a counter system by treating integer variables as counters. The counting mechanism of $\mathsf{CLTL}$ admits a more specific formulation of a correctness property, making it more restrictive or permissive than a plain $\mathsf{LTL}$ formula. For example, a typical pattern in the RERS problem set has the form $\neg p\operatorname{\mathrm{\mathbf{U}}}q$, stating $q$ occurs before $p$. It can be relaxed to state, e.g., $p$ occurs at most 5 times ($\operatorname{\mathbf{F}}_{[p\leq 5]}q$) or less often than $r$ ($\operatorname{\mathbf{F}}_{[p-r<0]}q$). A stronger formulation would be that $q$ must occur more often before $p$ ($\neg p\operatorname{\mathbf{U}}_{[q\geq 5]}q$ or $\neg p\operatorname{\mathbf{U}}_{[r-q\geq 5]}q$). To evaluate our procedure on counting properties, we constructed variations of formulae from the $\mathsf{LTL}$ track that express relaxed or strengthened versions of the properties.

By checking negated properties, counterexamples were found at an approximation depth of at most $128$ for all violated formulae, while most formulae could be falsified quickly. From the original 52 falsifiable $\mathsf{LTL}$ formulae, 43 were falsified after less than 200 seconds per formula at depth at most 64, the remaining 9 took at most 32 minutes per formula and depth 128. A batch analysis of the whole set of 100 formulae at depth 200 took a total of four days running time (Desktop PC, Intel i5-750 CPU, 4GB RAM). Some derived $\mathsf{CLTL}$ formulae took significantly longer to be evaluated than the original $\mathsf{LTL}$ formulation. However, in most cases, the introduction of counting constraints did not increase the evaluation effort significantly.

6 Conclusion

The concise representation of runs in terms of augmented path schemas allows for an accelerated evaluation of complex path properties expressed in a powerful specification framework with counting as first-class feature. We therefore believe that flat approximation provides a promising technique that deserves further investigation. The underlying theory provides that the procedure is complete on flat systems and, practically, an existing witness will be found eventually unless all of them have an infinitely aperiodic shape. It can also be used as (incomplete) approach to the satisfiability and synthesis problems of $\mathsf{CLTL}$.

Although it may eventually hinder problem-specific optimisations, the SMT-based implementation benefits from the engineering effort put into solvers. The configurability of, e.g., z3 using specific tactics, provides potential for future improvements. It remains to develop and compare different encoding variants. Especially, formulations that admit incremental solving could speed up the verification process. The primary ambition of our approach is to verify the expressive class of $\mathsf{CLTL}$ properties. Our evaluation suggests that this is feasible and, moreover, that flat model checking is well applicable in a general verification context such as the RERS Challenge.

Lifting the theoretical foundation to linear constraints and counter systems as a class of infinite-state models is a consequent advancement of the theory of path schemas. Characterising $\mathsf{CLTL}$ model-checking over flat systems in Presburger arithmetic fills a gap between corresponding results for temporal logics with and without counting [15, 14, 13].

6.0.1 Acknowledgement.

We thank Daniel Thoma for valuable technical discussions.

Appendix 0.A Complete Encoding

This section presents the details on the formula

[TABLE]

introduced in Section 4.

0.A.1 Basic Structure

The basic structure of APS is specified as QPA formula

[TABLE]

It states that $s_{I}$ is the origin of the first state and that loops are delimited by $\triangleright$ and $\triangleleft$ in terms of the formula

[TABLE]

To express that the labelling of states by propositions coincides with that of $\mathcal{S}$, the formula

[TABLE]

is used.

Transitions.

One way to express that each backward transition from the last to the first state of a loop has a correspondence in $\mathcal{S}$ is to build a constraint over all pairs of states from $Q$. This is, however, quadratic in $n$ and we therefore use a propagation scheme introducing $n$ additional variables $\mathsf{orgAtEnd}_{i}:S$. We let them equal $\mathsf{org}_{i}$ where $\mathsf{typ}_{i}=\triangleleft$ and otherwise be copied from $\mathsf{orgAtEnd}_{i+1}$, thus propagating backward the origin of the last state of every loop. The corresponding formula is

[TABLE]

The formula

[TABLE]

then guarantees that all backward transitions exist in $\mathcal{S}$. Similar propagation chains will be used at other occasions to avoid a quadratic blow-up of the formula size due to information non-locality. Forward transitions are specified similarly, but without the need for propagation, by

[TABLE]

The combination of the formulae now defines the formula

[TABLE]

used as part of $\mathrm{aps}(\mathcal{S},n)$ above. Notice that this encoding assumes a minimal loop length of $2$ due to distinct positions for the first ($\triangleright$) and the last ($\triangleleft$) state of each loop. Single-state loops can still be represented as longer (e.g. two-state) loops by combining multiple iterations as one loop that is iterated less often (cf. Fig. 2). Excluding single-state loops increases the upper bound for the size of path schemas only by one state per loop.

To allow for a simplified presentation, let us assume that there is at most one transition between every two states of $\mathcal{S}$, thus being uniquely identified by $\mathsf{org}_{i}$ and $\mathsf{org}_{i+1}$. The assumption could be eliminated by adding $2n$ additional variables determining explicitly which transition is selected for the represented APS.

Front and Rear Rows.

The definition of augmented path schemas demands that loops be surrounded by identical rows. Being identical, these rows are not represented explicitly in the encoding. Instead, runs will be assumed to traverse each representation of a loop at least three times, the first representing the front, the last representing the rear and the remaining representing the actual loop traversals. The construction will distinguish between the first, second and last iteration, where necessary. This is equivalent to representing the states of the front and rear rows individually but allows for a more compact encoding and also provides an efficient way to correlate every loop state to its correspondents on the front and rear.

0.A.2 Runs

The formula $\mathrm{run}(\mathcal{S},n)$ specifies the shape and constraints of a run in the encoded schema. It has the form

[TABLE]

Variables $\mathsf{itr}_{i}:\mathbb{N}$ are used to indicate how often state $i\in Q$ is visited and are thus constraint to equal $1$ outside loops and to stay constant inside each loop. Since every loop state is used to also represent its counterpart on the front and rear, they are to be repeated at least three times. Infinite iteration of the last loop is represented by the otherwise unused value [math]. This is formulated by

[TABLE]

The other components of the formula concern the valuation of counters and evaluation of transition guards. They are described in the following.

0.A.2.1 Counter valuations.

The valuation of any counter at any position on a run $\rho$ of an encoded APS $\mathcal{P}$ is determined unambiguously by the shape of $\mathcal{P}$ (in terms of the sequence of states and their origins) and the number of repetitions of every loop. Yet, in order to formulate that guards need to be satisfied, the counter values will be made explicit in terms of variables $\mathsf{valFst}_{i},\mathsf{valSec}_{i}:\mathbb{Z}^{C_{\mathcal{S}}}$ and $\mathsf{valLst}_{i}:\mathbb{Z}_{\infty}^{C_{\mathcal{S}}}$ for every state $i\in Q$. They are supposed to hold the counter valuations at the first, second, and last occurrence, respectively, of state $i$ on the represented run. Naturally, outside loops the first and last valuations are equal and the second does technically not exist, so $\mathsf{valSec}_{i}$ does not have a semantically meaningful value. Nevertheless, all variables are introduced for each state as loops may occur anywhere. Recall that the states of a loop also represent those of its front and rear rows, so the first and last iteration corresponds to those. The formula

[TABLE]

encodes the semantics of counter updates in terms of the valuations in the represented run. By definition, runs start with the valuation $\mathbf{0}$, assigning [math] to the whole domain. For row states $i$ (of type

$\boxminus$

) the valuation at its (first and only) occurrence is computed from the valuation at the last occurrence of the previous state $i-1$ by adding (elementwise) the update function $\mu$ of the transition $(\mathrm{org}(i-1),\mu,\Gamma,\mathrm{org}(i))\in\Delta$ from $i-1$ to $i$. As mentioned earlier, the first and last occurrence are the same and the variable $\mathsf{valSec}_{i}$ is deliberately set to equal them as well but could as well be left unconstrained. Hence, let

[TABLE]

Recall that we assume that there is at most one transition between every two states in $\mathcal{S}$. Inside (

$\boxplus$

) and at the end of loops ($\triangleleft$), the counter values are propagated individually for the first, second, and last iteration, expressed by

[TABLE]

At the beginning ($\triangleright$) of a loop the value in the first iteration is computed from the preceding position. The first value in the second iteration is to be computed from the last value of the first iteration. However, given a state $i$, it cannot be determined a priori which state exactly constitutes the end of the loop. To obtain the value of the state that happens to be the last on the loop, variables $\mathsf{valFstAtEnd}_{i}$ are introduced to hold the valuation at the last state during the first iteration throughout the loop and make it thus directly accessible at the beginning. They are defined using a propagation scheme as above expressed by

[TABLE]

Then, $\mathsf{valSec}_{i}$ can be set to $\mathsf{valFstAtEnd}_{i}+\mu$ where $\mu$ comes from the incoming backward transition of state $i$. This is specified by

[TABLE]

Having a direct handle on the valuations in the first and second iteration (in terms of the variables $\mathsf{valFst}_{i}$ and $\mathsf{valSec}_{i}$) as well as the total number of loop iterations ($\mathsf{itr}_{i}$), it is tempting to specify the valuations in the last iteration simply by

[TABLE]

Unfortunately, this formula uses multiplication of variables and hence exceeds Presburger arithmetic. Therefore, we need to specify the value of $(\mathsf{valSec}_{i}-\mathsf{valFst}_{i})\cdot(\mathsf{itr}_{i}-1)$ differently. Instead, the updates over the second to last loop iteration are accumulated in an explicit variable $\mathsf{lUpd}_{i}$ such that $\mathsf{valLst}_{i}$ can be set to $\mathsf{valFst}_{i}+\mathsf{lUpd}_{i}$. We express this accumulation by the formula

[TABLE]

Essentially, the multiplication by $\mathsf{itr}_{i}$ is distributed over the individual transition updates along the loop. This is admissible because the individual updates $\mu$ appear in the formula not as variables but as constants. Notice that this formulation deliberately multiplies functions with integers, which is to be understood as point-wise application. Further, the choice of using 0 to mark the infinite iteration of the last loop (as opposed to, e.g., $\infty$) is useful here because otherwise the equation would not be well defined, a negative and a positive update could result in having to add $-\infty$ and $\infty$. In the formulation above, $\mathsf{lUpd}_{i}$ is always zero for states $i$ on the last loop but this is no problem because this particular situation can be handled using $\mathsf{valFst}_{i}$ and $\mathsf{valSec}_{i}$. Observe also that the variable $\mathsf{lUpd}_{i}$ holds only intermediate results inside and at the end of loops and is undefined outside. Only for states $i$ that are the beginning of a loop, it holds the precise accumulated loop effect but this suffices since this value is propagated as specified by the formula $\mathrm{valLoop}(\mathcal{S},n)$ above.

Using $\mathsf{lUpd}_{i}$, the calculation of the valuations in the last iteration of a loop is now formulated as

[TABLE]

0.A.2.2 Guards.

To ensure that the represented run is valid it must satisfy all the guards at any time. The formula $\mathrm{valuations}(\mathcal{S},n)$ developed above ensures that the variables $\mathsf{valFst}_{i}$, $\mathsf{valSec}_{i}$, and $\mathsf{valLst}_{i}$ faithfully provide the counter valuations when reaching the state $i\in Q$ for the first, the second and the last time, respectively. Recall that, due to flatness, each loop is entered and left only once. Since every guard of the counter system is a linear inequality and the effect of the updates of any specific loop is constant, it suffices to check the guard in the first and last traversal in order to guarantee that it is satisfied throughout all repetitions of a particular loop state.

For a constraint term over $C_{\mathcal{S}}$ of the form $\tau=\sum_{j=0}^{\ell}a_{j}c_{j}$ and a variable symbol $\mathsf{var}:\mathbb{Z}^{C_{\mathcal{S}}}$, let $\tau[\mathsf{var}]:=\sum_{j=0}^{\ell}a_{j}\cdot\mathsf{var}(c_{j})$ denote the syntactic substitution of the counter names by the variable symbol (representing the value of) $\mathsf{var}(c_{j})$, in analogy to the evaluation of constraint terms using valuations (cf. Section 2). The formula

[TABLE]

then specifies that the encoded run satisfies the guards whenever taking a forward transition. Recall that for some counter $c\in C_{\mathcal{S}}$ the variable $\mathsf{valLst}_{i}(c)$ may be assigned a symbolic value. Thus, a proper interpretation (or expansion) of $\geq$ is assumed such that $\infty\geq b$ holds for every $b\in\mathbb{Z}$ while $-\infty\geq b$ holds for none. Notice that the (forward) transition from state $i-1$ to state $i$ is not taken at the beginning of the last iteration of a loop and thus, its guard must not be checked for the corresponding valuation. Instead, the guard of the backward transition pointing to $i$ must be verified. This transition is taken by the encoded run for the first time when entering the second loop iteration. The guards of backward transitions are thus reflected exhaustively by

[TABLE]

Thereby we complete the definition of the formula

[TABLE]

and the specification of proper runs in terms of the formula $\mathrm{run}(\mathcal{S},n)$.

0.A.3 Consistency

The formulae constructed above describe the fact that there is some non-empty augmented path schema in the counter system $\mathcal{S}$ of which the first state is labelled by $\Phi$. In the following, we develop the components of the formula

[TABLE]

stating that this APS is consistent. Recall that $\Phi$-consistency requires all states of an APS to be consistent with respect to all subformulae of $\Phi$. Definition 5 discriminates the structural cases of a $\mathsf{CLTL}$ formula and therefore the components of the QPA formulation cover one case each and impose consistency of all states for one subformula of $\Phi$ at a time.

0.A.3.1 Propositions and Boolean combinations.

Item B of Definition 5 can almost literally be translated to QPA formulae

[TABLE]

0.A.3.2 Atomic constraints.

Concerning Item A, counter guard formulae of the form $\tau\geq b$ are not modelled explicitly. Rather, the formula

[TABLE]

imposes that the represented run satisfies the constraints as if they were guards on all incoming transitions on any state labelled by an atomic constraint. Recall that it suffices to assert that the constraint is satisfied at the first and last occurrence of a state.

0.A.3.3 Temporal Next.

To express Item C of the consistency definition, concerning temporal next formulae, variables $\mathsf{lblAtBeg}_{i}:2^{\mathrm{sub}(\Phi)}$ are used to propagate labelling information from the first state of a loop forward towards its end. Similar to the backward propagation of the origin, let

[TABLE]

Notice that it is not necessary to determine the propagation value at the first ($i=0$) state because it is never part of a loop. The condition is now specified by

[TABLE]

0.A.3.4 Temporal Until: Item D1.

Consider a formula $\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi\in\mathrm{sub}(\Phi)$. The consistency criterion considers three conditions for until formulae of that form. Towards defining the corresponding QPA formula $\mathrm{consistencyU}(n,\chi,\psi,\tau,b)$ consider first Item D1 stating, essentially, that the last loop exhibits a positive effect that eventually proves the formula to hold. To express the requirements of that condition, the following information is required. Given a state $i\in[0,n-1]$, first of all, it must be labelled by $\varphi$ and that information is available in terms of the value of the variable $\mathsf{lbl}_{i}$. Second, assume a variable $\mathsf{acc}_{0}^{\tau}:\mathbb{Z}$ holding the accumulated effect of the last loop on the value of $\tau$. Third, let $\mathsf{onLast}^{\psi}:\mathbb{B}$ be set to true if and only if $\psi$ occurs as label on some state of the last loop and $\mathsf{glob}_{i}^{\chi}:\mathbb{B}$ hold if and only if $\chi$ holds globally from state $i$ on. Then, Item D1 is expressed by

[TABLE]

It remains to formulate the side conditions guaranteeing that the variables actually hold the assumed value.

Accumulated effect of the last loop.

To describe the accumulated value of $\tau$ on a single iteration of the last loop we introduce $\mathsf{acc}_{i}^{\tau}$ not only for $i=0$ but for each $i\in[0,n-1]$. The idea is now to accumulate backwards from $\mathsf{acc}_{n-1}^{\tau}$ to $\mathsf{acc}_{0}^{\tau}$ the effects $\tau[\mathsf{lbl}_{i}]$ as long as $i$ is part of the last loop (identified by $\mathsf{itr}_{i}$ being equal [math]). Let

[TABLE]

It implies, as intended, that $\mathsf{acc}_{0}^{\tau}$ holds the effect of the last loop on the value of $\tau$.

Reachability of defect- and witness states.

Consider the evaluation of whether $\chi$ holds globally at all reachable states. For loop states $i\in Q$, this means that not only the successors $j\geq i$ must be labelled by $\chi$ but the whole loop. Therefore, we employ a propagation scheme with two passes. First, a backward propagation imposes that variables $\mathsf{prpg}_{i}^{\chi}$ hold if and only if all states $j\geq i$ are labelled by $\chi$. Based on this information, the intended valuation for $\mathsf{glob}_{i}^{\chi}$ is enforced by a forward propagation. The formula

[TABLE]

implies that each variable $\mathsf{glob}_{i}^{\chi}$ is true if and only if $\chi$ is labelled at all states reachable from $i$. The information whether $\psi$ holds somewhere on the last loop is made available in terms of the variable $\mathsf{onLast}^{\psi}$ by

[TABLE]

0.A.3.5 Temporal Until: Item D2.

Item D2 demands the existence or absence of a witness state proving that a formula $\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi\in\mathrm{sub}(\Phi)$ holds. As before, it would be inefficient to model balance counters and the guards required by the criterion explicitly. Instead, a formulation is developed that assures that the encoded APS can be assumed to have the necessary counters and guards.

For example, assume some state $i$ is to be labelled by $\varphi$ and consider the best (maximal) value of the term $\tau$ on a path starting at state $i$ and leading to some state satisfying $\psi$, without violating $\chi$ in between. If that value is at least $b$, then there is a state at which a balance counter $c_{\tau,i}$ for $\tau$ and $i$ would have precisely this value and checking the constraint $c_{\tau,i}\geq b$ would succeed. On the other hand, if the best value is below $b$, then there is no such state. Even, the dual constraint could be added to any potential witness state and the encoded run would still be valid.

Consider an APS $\mathcal{P}$ in $\mathcal{S}$ with states $Q=[0,n-1]$ and assume it is consistent with respect to all strict subformulae of $\varphi$ and admits a run $\sigma\in\mathrm{runs}(\mathcal{P})$. Let $x_{\mathrm{last}}\in\mathbb{N}$ be the first position of state $n-1$ on $\sigma$ and let $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}:\mathbb{N}\to\mathbb{Z}_{\infty}$ denote the discussed function defined for $x\in\mathbb{N}$ by

[TABLE]

We make three essential observations regarding $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}$.

First, consider the positions $x\leq x_{\mathrm{last}}-|\mathrm{lastl}(\mathcal{P})|$ preceding the last loop. For those, $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x)$ accurately determines the maximal value for $\tau$ (the symbolic value $-\infty$ expressing non-existence of a witness position) unless Item D1 applies to the state at position $x$ on $\sigma$. Assuming that there is a witness position $z\geq x_{\mathrm{last}}$, the last loop must be entirely labelled by $\chi$ and if $\llbracket\tau\rrbracket(\#^{\mathcal{P},\sigma}_{x,z-1})>\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x)$, the effect of the final loop on $\tau$ must be positive.

Second, if one of Items D(2)i and D(2)ii applies to a (row) state $i\in Q$, then there cannot be a witness position for $\varphi$ holding at $i$, especially not before $x_{\mathrm{last}}$, and thus $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x_{i})<b$ for the (unique) position $x_{i}\in\mathbb{N}$ of state $i$ on $\sigma$. On the other hand, if $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x_{i})<b$, then one of Items D1 and D(2)i applies or any balance counter $c_{\tau,i}$ for $i$ and $\tau$ would satisfy the guard $c_{\tau,i}<b$ at any witness position $j\geq i$ for $\varphi$. In the latter case it can thus be assumed that state $i$ obeys Item D(2)ii in $\mathcal{P}$.

Third, a similar point can be made for Items D(2)iii and D(2)iv given that $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x_{i})\geq b$. These conditions imply that there, in fact, is a witness position for $\varphi$ before the end of the second iteration of the last loop. Vice versa, the definition of $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x_{i})$ demands for some witness position $y\geq x_{i}$. Then, one of Items D1 and D(2)iii holds or Item D(2)iv can be established without adding extra states. Hence, $i$ can be assumed to obey one of the conditions in $\mathcal{P}$.

Based on these considerations, we introduce variables $\mathsf{maxFst}_{i}^{\varphi}$ and $\mathsf{maxLst}_{i}^{\varphi}$ for each state $i\in[0,n-1]$ and until formula $\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi\in\mathrm{sub}(\Phi)$ that are supposed represent the value $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x_{i})$ at the first position $x_{i}$ of state $i$ and the value $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x_{i}^{\prime})$ at the last position $x_{i}^{\prime}$ of $i$, respectively. Recall that these positions cover only rows as the first and last iteration of loops represent their front and rear, respectively. Notice also that the latter value is not defined for positions belonging to the last loop. Then, Item D2 is formulated for a state $i$ as

[TABLE]

0.A.3.6 Temporal Until: maximal value to witness.

The intended value for these variables is specified using a suffix-optimum backward propagation scheme initiated at the end of the represented schema. We can characterise the values $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x)$ by

[TABLE]

and for $x\in[0,x_{\mathrm{last}}-1]$ by

[TABLE]

As long as $\chi$ holds, the maximal value is propagated backwards. When the chain breaks at some defect state, no witness position is properly reachable, and the maximal value is set to $-\infty$. Each state of the schema where $\psi$ holds is a potential witness for preceding states. Thus, if the propagated value at this point is less than [math], this state will generally provide a better value for $\tau$ than any of its successors. In the QPA formulation, the above definition is split into the computation of the updated value $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}(x+1)+\llbracket\tau\rrbracket(\lambda^{\#}(\sigma(x)))$ potentially propagated to its predecessor and the actual selection of the appropriate value depending on the case. To express the update across a loop, it is further necessary to express its effect. These aspects are reflected in the components of the formula

[TABLE]

Selection and auxiliary iteration.

Recall that the encoding does not represent every position of the run and not even every state of the path schema explicitly, namely those situated on loops. However, the values at the front and rear row of a loop are represented and the propagation scheme hence needs to “jump” from the rear to the front, that is, extrapolate the calculated value over the iterations of the loop. For that purpose, an additional set of auxiliary variables $\mathsf{maxAux}_{i}^{\varphi}$ are introduced representing, intuitively, the first actual iteration of a loop—similarly to the variables $\mathsf{valSec}_{i}$ above. Thus, the axillary variables complement the variables $\mathsf{maxFst}_{i}^{\varphi}$ and $\mathsf{maxLst}_{i}^{\varphi}$ representing the front and rear rows, respectively.

The case selection is expressed for all three variants by the formula

[TABLE]

where the variables $\mathsf{updFst}_{i}^{\varphi}$, $\mathsf{updLst}_{i}^{\varphi}$, and $\mathsf{updAux}_{i}^{\varphi}$ are assumed to hold the value from the state $i+1$ updated according to the labelling (or the respective initialisation). For easier reading, expressions of the form $\mathsf{var1}=\max(\mathsf{var2},a)$ are used to abbreviate $\mathrm{ite}(\mathsf{var2}>a,\mathsf{var1}=\mathsf{var2},\mathsf{var1}=a)$.

Modelling loop effects.

The overall effect of (all iterations of) a loop on the value of $\tau$ is made accessible in terms of variables $\mathsf{sumEff}^{\tau}_{i}$ where $i$ is the first state of a loop. It is obtained by summing up the individual contribution $\tau[\mathsf{lbl}_{i}]\cdot(\mathsf{itr}_{i}-3)$ of each loop state $i$ bound to variables $\mathsf{eff}^{\tau}_{i}$. The effect is multiplied only by $\mathsf{itr}_{i}-3$ since the first (front), second (auxiliary), and last (rear) iteration is already accounted for explicitly. To circumvent multiplication of variables in the formula, the variables $\mathsf{eff}^{\tau}_{i}$ are themselves defined by distributing the factor ($\mathsf{itr}_{i}-3$) over the sum of monomials of the term $\tau$, as was necessary also for the accumulation of counter updates. The term is assumed to have the form $\tau=\sum_{k=0}^{m}a_{k}\chi_{k}$ and the effect is hence specified by

[TABLE]

where the variables $\mathsf{eff}_{i}^{\tau}=\mathsf{eff}_{i}^{\tau,m}$ are to be considered identical.

Calculating values to propagate.

Using the summed-up loop effect, we can now formulate the actual computation of the (potentially) propagated optimum by

[TABLE]

where $\varphi=\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi$ is assumed.

The formula $\mathrm{calcUpdated}(n,\varphi)$ consists of three parts: the first specifies the updated value, depending on the type of state, the second sets the starting value for the propagation at state $n-1$ for the auxiliary track on which all others depend, and the third makes the value of the auxiliary variables at the begin of each loop available at the corresponding end.

Consider the first part. Outside of loops (type

$\boxminus$

), the first and last encounter of any state fall together, and the updated value is simply calculated from the succeeding position, being the first occurrence of the succeeding state. A state of type $\triangleleft$ marks the end of a loop where the variable $\mathsf{maxLst}_{i}^{\varphi}$ represent the very last state of its rear row and is hence treated just as other row states. As mentioned earlier, the auxiliary track can be considered as the first actual iteration of the loop, thus immediately following the front row. The value of its last state is determined by extrapolating the value at the start of the rear over all iterations by adding the effect of all loop iterations in between. This may in fact be the correct value of $\mathrm{maxWit}^{\mathcal{P},\sigma}_{\varphi}$ at this point. However, in case there is a defect on the loop or the effect of the loop is negative, the witness assumed by the extrapolation is not reachable without violating $\chi$ in between or may not provide the maximal value for $\tau$, respectively. Nevertheless, as the value is passed along it traverses all positions of the loop. Then, if the loop does have a defect, the selection determined by the formula $\mathrm{selectMax}$ would necessarily reset that value to either [math] or $-\infty$ and provide a correct value from that point on. Similarly, if the overall effect of the loop is negative and there is a witness providing a higher value of $\tau$, this witness would be found on the first iteration and the selection would again promote this one as soon as it is encountered. Hence, upon reaching the first state of the loop, the propagated value on the auxiliary track is in fact correct. It is transferred back to the end of the loop by the last part of the formula (by variables $\mathsf{maxAuxAtBeg}_{i}^{\varphi}$) and then used to correctly determine the value of $\mathsf{maxFst}_{i}^{\varphi}$.

Therefore, assessing consistency Item D2 as stated by the formula $\mathrm{con\ref{itm:consistency-U-counter}}$ is appropriate, at least for those states to which Item D1 does not apply. Note that, if the latter does apply to some state, the evaluation of the other criterion is irrelevant.

0.A.3.7 Temporal Until: consistency.

Based on the developments above, the cases for the consistency criterion are combined to express consistency for temporal until formulae $\chi\operatorname{\mathbf{U}}_{[\tau\geq b]}\psi$ by

[TABLE]

The structure of the encoding assures that the actual loops are always identically labelled to their front and rear rows. Thus, assuring those are consistent, all loops automatically satisfy Item D3.

This completes the construction of the formula $\mathrm{consistency}(\mathcal{S},n,\Phi)$ and thereby that of $\mathrm{fmc}(\mathcal{S},n,\Phi)$.