Abstract Interpretation of CTL Properties

Abstract

CTL is a temporal logic commonly used to express program properties. Most of the existing approaches for proving CTL properties only support certain classes of programs, limit their scope to a subset of CTL, or do not directly support certain existential CTL formulas. This paper presents an abstract interpretation framework for proving CTL properties that does not suffer from these limitations. Our approach automatically infers sufficient preconditions, and thus provides useful information even when a program satisfies a property only for some inputs. We systematically derive a program semantics that precisely captures CTL properties by abstraction of the operational trace semantics of a program. We then leverage existing abstract domains based on piecewise-defined functions to derive decidable abstractions that are suitable for static program analysis. To handle existential CTL properties, we augment these abstract domains with under-approximating operators. We implemented our approach in a prototype static analyzer. Our experimental evaluation demonstrates that the analysis is effective, even for CTL formulas with non-trivial nesting of universal and existential path quantifiers, and performs well on a wide variety of benchmarks.

1 Introduction

Computation tree logic (CTL) [6] is a temporal logic introduced by Clarke and Emerson to overcome certain limitations of linear temporal logic (LTL) [33] for program specification purposes. Most of the existing approaches for proving program properties expressed in CTL have limitations that restrict their applicability: they are limited to finite-state programs [7] or to certain classes of infinite-state programs (e.g., pushdown systems [36]), they limit their scope to a subset of CTL (e.g., the universal fragment of CTL [11]), or support existential path quantifiers only indirectly by considering their universal dual [8].

Fig. 1.

Standard lock acquire/release-style program [12], where rand() is a random number generation function. Assignments $\text {x} := 1$ and $\text {x} := 0$ are acting as acquire and release, respectively. We want to prove the CTL property $\mathsf {A} \mathsf {G} (\text {x} = 1 \Rightarrow \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0))$ expressing that whenever a lock is acquired ($\text {x} = 1$) it is eventually released ($\text {x} = 0$). We assume that initially $\text {x} =0$.

In this paper, we propose a new static analysis method for proving CTL properties that does not suffer from any of these limitations. We set our work in the framework of abstract interpretation [16], a general theory of semantic approximation that provides a basis for various successful industrial-scale tools (e.g., Astrée [3]). We generalize an existing abstract interpretation framework for proving termination [18] and other liveness properties [41].

Following the theory of abstract interpretation [14], we abstract away from irrelevant details about the execution of a program and systematically derive a program semantics that is sound and complete for proving a CTL property. The semantics is a function defined over the programs states that satisfy the CTL formula. The value of the semantics for a CTL formula that expresses a liveness property (e.g., $\mathsf {A} (true \mathrel {\mathsf {U}} \phi )$) gives an upper bound on the number of program execution steps needed to reach a desirable state (i.e., a state satisfying $\phi$ for $\mathsf {A} (true \mathrel {\mathsf {U}} \phi )$). The semantics for any other CTL formula is the constant function equal to zero over its domain. We define the semantics inductively on the structure of a CTL formula, and we express it in a constructive fixpoint form starting from the functions defined for its sub-formulas.

Further sound abstractions suitable for static program analysis are derived by fixpoint approximation [14]. We leverage existing numerical abstract domains based on piecewise-defined functions [39], which we augment with novel under-approximating operators to directly handle existential CTL formulas. The piecewise-defined function for a CTL formula is automatically inferred through backward analysis by building upon the piecewise-defined functions for its sub-formulas. It over-approximates the value of the corresponding concrete semantics and, by under-approximating its domain of definition, yields a sufficient precondition for the CTL property. We prove the soundness of the analysis, meaning that all program executions respecting the inferred precondition indeed satisfy the CTL property. A program execution that does not respect the precondition might or might not satisfy the property.

To briefly illustrate our approach, let us consider the acquire/release-style program shown in Fig. 1, and the CTL formula $\mathsf {A} \mathsf {G} (\text {x} = 1 \Rightarrow \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0))$. The analysis begins from the atomic propositions $\text {x} = 1$ and $\text {x} = 0$ and, for each program control point, it infers a piecewise-defined function that is only defined when $\text {x}$ is one or zero, respectively. It then continues to the sub-formula $\mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0)$ for which, building upon the function obtained for $\text {x} = 0$, it infers the following interesting function at program point :

$$\begin{aligned} \lambda \text {x}. \lambda \text {n}. {\left\{ \begin{array}{ll} 0 &{} \text {x} = 0 \\ 2 &{} \text {x} \ne 0 \wedge \text {n} \le 0 \\ 2\text {n} + 2 &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

(1.1)

The function indicates that the sub-formula $\text {x} = 0$ is either satisfied trivially (when $\text {x}$ is already zero), or in at most 2 program execution steps when $\text {n} \le 0$ (and thus the loop at program point is not entered) and $2\text {n} + 2$ steps when $\text {n} > 0$ (and thus the loop is entered). The analysis then proceeds to $\text {x} = 1 \Rightarrow \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0)$, i.e., $\text {x} \ne 1 \vee \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0)$. The inferred function for the sub-formula $\text {x} \ne 1$ is only defined over the complement of the domain of the one obtained for $\text {x} = 1$. The disjunction combines this function with the one obtained for $\mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0)$ by taking the union over the function domains and the maximum over the function values. The result at program point is the same function obtained for $\mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0)$. Finally, the analysis can proceed to the initial formula $\mathsf {A} \mathsf {G} (\text {x} = 1 \Rightarrow \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0))$. The function at program point remains the same but its value now indicates the maximum number of steps needed until the next state that satisfies $\text {x} = 0$. The function inferred at the beginning of the program proves that the program satisfies the CTL formula $\mathsf {A} \mathsf {G} (\text {x} = 1 \Rightarrow \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0))$ unless $\text {x}$ has initial value one. Indeed, in such a case, the program does not satisfy the formula since the loop at program point might never execute. Thus, the inferred precondition is the weakest precondition for the CTL property $\mathsf {A} \mathsf {G} (\text {x} = 1 \Rightarrow \mathsf {A} (true \mathrel {\mathsf {U}} \text {x} = 0))$.

We implemented our approach in the prototype static analyzer $\textsc {FuncTion}$ [13]. Our experimental evaluation demonstrates that the analysis is effective, even for CTL formulas with non-trivial nesting of universal and existential path quantifiers, and performs well on a wide variety of benchmarks.

2 Trace Semantics

We model the operational semantics of a program as a transition system $\langle \varSigma ,\tau \rangle$ where $\varSigma$ is a (potentially infinite) set of program states, and the transition relation $\tau \subseteq \varSigma \times \varSigma$ describes the possible transitions between states. The set of final states of the program is $\varOmega {\mathop {\,=\,}\limits ^{{\tiny def}}} \{s \in \varSigma \mid \forall s' \in \varSigma :\langle s, s' \rangle \not \in \tau \}$.

Given a transition system $\langle \varSigma ,\tau \rangle$, the function $\mathrm {pre} :\mathcal {P}\left( \varSigma \right) \rightarrow \mathcal {P}\left( \varSigma \right)$ maps a given set of states X to the set of their predecessors with respect to $\tau {:} \mathrm {pre} (X) {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ s \in \varSigma \mid \exists s' \in X: \langle s, s' \rangle \in \tau \right\}$, and the function $\widetilde{\mathrm {pre}} :\mathcal {P}\left( \varSigma \right) \rightarrow \mathcal {P}\left( \varSigma \right)$ maps a given set of states X to the set of states whose successors with respect to $\tau$ are all in X: $\widetilde{\mathrm {pre}} (X) {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ s \in \varSigma \mid \forall s' \in \varSigma : \langle s, s' \rangle \in \tau \Rightarrow s' \in X \right\}$.

In the following, given a set S, let $S^n {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ s_0 \cdots s_{n-1} \mid \forall i < n: s_i \in S \right\}$ be the set of all sequences of exactly n elements from S. We write $\varepsilon$ to denote the empty sequence, i.e., $S^0 {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \varepsilon \right\}$. Let $S^* {\mathop {\,=\,}\limits ^{{\tiny def}}} \bigcup _{n \in \mathbb {N}} S^n$ be the set of all finite sequences, $S^+ {\mathop {\,=\,}\limits ^{{\tiny def}}} S^* \setminus S^0$ be the set of all non-empty finite sequences, $S^\omega$ be the set of all infinite sequences, $S^{+\infty } {\mathop {\,=\,}\limits ^{{\tiny def}}} S^+ \mathrel {\cup } S^\omega$ be the set of all non-empty finite or infinite sequences and $S^{*\infty } {\mathop {\,=\,}\limits ^{{\tiny def}}} S^* \mathrel {\cup } S^\omega$ be the set of all finite or infinite sequences of elements from S. We write $\sigma \sigma '$ for the concatenation of two sequences $\sigma , \sigma ' \in S^{*\infty }$ (with $\sigma \varepsilon = \varepsilon \sigma = \sigma$, and $\sigma \sigma ' = \sigma$ if $\sigma \in S^\omega$), $T^+ {\mathop {\,=\,}\limits ^{{\tiny def}}} T \mathrel {\cap } S^+$ for the selection of the non-empty finite sequences of $T \subseteq S^{*\infty }$, $T^\omega {\mathop {\,=\,}\limits ^{{\tiny def}}} T \mathrel {\cap } S^\omega$ for the selection of the infinite sequences of $T \subseteq S^{*\infty }$, and $T \mathrel {;} T' {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma s \sigma ' \mid s \in S, \sigma s \in T, s \sigma '\in T'\right\}$ for the merging of sets of sequences $T \subseteq S^+$ and $T' \subseteq S^{+\infty }$, when a finite sequence in T terminates with the initial state of a sequence in $T'$.

Given a transition system $\langle \varSigma ,\tau \rangle$, a trace is a non-empty sequence of program states described by the transition relation $\tau$, that is, $\langle s, s' \rangle \in \tau$ for each pair of consecutive states $s, s' \in \varSigma$ in the sequence. The set of final states $\varOmega$ and the transition relation $\tau$ can be understood as sets of traces of length one and two, respectively. The maximal trace semantics $\varLambda \in \mathcal {P}\left( \varSigma ^{+\infty } \right)$ generated by a transition system is the union of all non-empty finite traces that are terminating with a final state in $\varOmega$, and all infinite traces. It can be expressed as a least fixpoint in the complete lattice $\langle \mathcal {P}\left( \varSigma ^{+\infty } \right) , \sqsubseteq , \sqcup , \sqcap , \varSigma ^\omega , \varSigma ^+ \rangle$ [14]:

$$\begin{aligned} \varLambda = \mathrm {lfp} ^\sqsubseteq ~\lambda T. \varOmega \mathrel {\cup } (\tau \mathrel {;} T) \end{aligned}$$

(2.1)

where the computational order is $T_1 \sqsubseteq T_2 {\mathop {\,=\,}\limits ^{{\tiny def}}} T_1^+ \subseteq T_2^+ \wedge T_1^\omega \supseteq T_2^\omega$.

The maximal trace semantics carries all information about a program and fully describes its behavior. However, reasoning about a particular property of a program is facilitated by the design of a semantics that abstracts away from irrelevant details about program executions. In the paper, we use abstract interpretation [16] to systematically derive, by abstraction of the maximal trace semantics, a sound and complete semantics that precisely captures exactly and only the needed information to reason about CTL properties.

3 Computation Tree Logic

CTL is also known as branching temporal logic; its semantics is based on a branching notion of time: at each moment there may be several possible successor program states and thus each moment of time might have several different possible futures. Accordingly, the interpretation of CTL formulas is defined in terms of program states, as opposed to the interpretation of LTL formulas in terms of traces. This section gives a brief introduction into the syntax and semantics of CTL. We refer to [1] for further details.

We assume a set of atomic propositions describing properties of program states. Formulas in CTL are formed according to the following grammar:

$$\begin{aligned} \begin{aligned} \phi&::= a \mid \lnot \phi \mid \phi \wedge \phi \mid \phi \vee \phi \mid \mathsf {A} \mathsf {X} \phi \mid \mathsf {A} \mathsf {G} \phi \mid \mathsf {A} (\phi \mathrel {\mathsf {U}} \phi ) \mid \mathsf {E} \mathsf {X} \phi \mid \mathsf {E} \mathsf {G} \phi \mid \mathsf {E} (\phi \mathrel {\mathsf {U}} \phi ) \end{aligned} \end{aligned}$$

where a is an atomic proposition. The universal quantifier (denoted $\mathsf {A}$) and the existential quantifier (denoted $\mathsf {E}$) allow expressing properties of all or some traces that start in a state. In the following, we often use $\mathsf {Q}$ to mean either $\mathsf {A}$ or $\mathsf {E}$. The next temporal operator (denoted $\mathsf {X}$) allows expressing properties about the next program state in a trace. The globally operator (denoted $\mathsf {G}$) allow expressing properties that should hold always (i.e., for all states) on a trace. The until temporal operator (denoted $\mathrel {\mathsf {U}}$) allows expressing properties that should hold eventually on a trace, and always until then. We omit the finally temporal operator (denoted $\mathsf {F}$) since a formula of the form $\mathsf {Q} \mathsf {F} \phi$ can be equivalently expressed as $\mathsf {Q} (true\mathrel {\mathsf {U}} \phi )$.

The semantics of formulas in CTL is formally given by a satisfaction relation $\models$ between program states and CTL formulas. In the following, we write $s\,\models \,\phi$ if and only if the formula $\phi$ holds in the program state $s \in \varSigma$. We assume that the satisfaction relation for atomic propositions is given. The satisfaction relation for other CTL formulas is formally defined as follows:

(3.1)

where $T(s) \in \mathcal {P}\left( \varSigma ^{+\infty } \right)$ denotes the set of all program traces starting in the state $s \in \varSigma$. The semantics of trace formulas $\varphi$ is defined below:

(3.2)

where $\sigma [i]$ denotes the program state at position i on the trace $\sigma \in \varSigma ^{+\infty }$. We refer to [1] for further details.

Fig. 2.

CTL abstraction $\alpha _\phi :\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ for each CTL formula $\phi$. The function $\mathrm {trans}_\mathsf {Q}$ stands for $\mathrm {pre}$, if $\mathsf {Q}$ is $\mathsf {E}$, or $\widetilde{\mathrm {pre}}$, if $\mathsf {Q}$ is $\mathsf {A}$ (cf. Sect. 2). The state function $\mathrm {st} :\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow \mathcal {P}\left( \varSigma \right)$ collects all states of a given set of sequences T: $\mathrm {st} (T) {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ s \in \varSigma \mid \exists \sigma ' \in \varSigma ^*,\sigma '' \in \varSigma ^{*\infty }: \sigma 's\sigma '' \in T \right\}$. The ranking abstraction $\alpha ^\text {rk}_{\mathsf {Q}} :\mathcal {P}\left( \varSigma ^+\right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ is defined in Eq. 4.1, while the subsequence abstraction $\alpha ^\text {sq} _{\mathsf {Q} \mathsf {F} \phi }:\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow \mathcal {P}\left( \varSigma ^+\right)$ is defined in Eqs. 4.2 and 4.3. In the last two rows, $f_1 {\mathop {\,=\,}\limits ^{{\tiny def}}} \alpha _{\phi _1}(T)$ and $f_2 {\mathop {\,=\,}\limits ^{{\tiny def}}} \alpha _{\phi _2}(T)$.

4 Program Semantics for CTL Properties

In the following, we derive a program semantics that is sound and complete for proving a CTL property. We define the semantics inductively on the structure of a CTL formula. More specifically, for each formula $\phi$, we define the CTL abstraction $\alpha _\phi :\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ which extracts a partial function $f:\varSigma \rightharpoonup \mathbb {O}$ from program states to ordinals from a given set of sequences $T \in \mathcal {P}\left( \varSigma ^{+\infty } \right)$ by building upon the CTL abstractions of the sub-formulas of $\phi$. The domain of f coincides with the set of program states that satisfy $\phi$. Ordinal values are needed to support programs with possibly unbounded non-determinism [18]. The definition of $\alpha _\phi$ for each CTL formula is summarized in Fig. 2 and explained in more detail below. We use the CTL abstraction to define the program semantics $\varLambda _\phi :\varSigma \rightharpoonup \mathbb {O}$ for a formula $\phi$ by abstraction of the maximal trace semantics $\varLambda$.

Definition 1

Given a CTL formula $\phi$ and the corresponding CTL abstraction $\alpha _\phi :\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$, the program semantics $\varLambda _\phi :\varSigma \rightharpoonup \mathbb {O}$ for $\phi$ is defined as $\varLambda _\phi {\mathop {\,=\,}\limits ^{{\tiny def}}} \alpha _\phi (\varLambda )$, where $\varLambda$ is the maximal trace semantics (cf. Eq. 2.1).

Remarks. It may seem unintuitive to define $\varLambda _\phi$ starting from program traces rather than program states (as in Sect. 3). The reason behind this deliberate choice is that it allows placing $\varLambda _\phi$ in the hierarchy of semantics defined by Cousot [14], which is a uniform framework that makes program semantics easily comparable and facilitates explaining the similarities and correspondences between semantic models. Specifically, this enables the comparison with existing semantics for termination [18] and other liveness properties [41] (cf. Sect. 7).

It may also seem unnecessary to define $\varLambda _\phi$ to be a function. However, this choice yields a uniform treatment of CTL formulas independently of whether they express safety or liveness properties (or a combination of these). Additionally, it allows leveraging existing abstract domains [38, 39] (cf. Sect. 5) to obtain a sound static analysis for CTL properties. In particular, the proof of the soundness of the static analysis (cf. Theorem 2 and [38] for more details) requires reasoning both about the domain of $\varLambda _\phi$ as well as its value.

Atomic Propositions.

For an atomic proposition a, the CTL abstraction $\alpha _a:\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ simply extracts from a given set T of sequences a partial function that maps the states of the sequences in T (i.e., $s \in \mathrm {st} (T)$) that satisfy a (i.e., $s \,\models \, a$) to the constant value zero, meaning that no program execution steps are needed until a is satisfied for all executions starting in those states. Thus, the domain of the corresponding program semantics $\varLambda _a:\varSigma \rightharpoonup \mathbb {O}$ is (cf. Definition 1) is the set of program states that satisfy a (since $\mathrm {st} (\varLambda ) = \varSigma$).

Next-Formulas.

Next-formulas $\mathsf {Q} \mathsf {X} \phi$ express that the next state of all traces (if $\mathsf {Q}$ is $\mathsf {A}$) or at least one trace (if $\mathsf {Q}$ is $\mathsf {E}$) satisfies $\phi$.

The CTL abstraction $\alpha _{\mathsf {Q} \mathsf {X} \phi }:\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ for a next-formula $\mathsf {Q} \mathsf {X} \phi$ (cf. Fig. 2) maps a set T of sequences to a partial function defined over the states of the sequences in T (i.e., $s \in \mathrm {st} (T)$) that are the predecessors of the states that satisfy $\phi$, that is, the predecessors of the states in the domain of the CTL abstraction for $\phi$ (i.e., $s \in \mathrm {trans}_\mathsf {Q} (\mathrm {dom} (\alpha _{\phi }(T)))$). The function has constant value zero over its domain, again meaning that no program execution steps are needed until $\mathsf {Q} \mathsf {X} \phi$ is satisfied for all executions starting in those states.

Thus, the domain of the program semantics $\varLambda _{\mathsf {Q} \mathsf {X} \phi }:\varSigma \rightharpoonup \mathbb {O}$ is the set of states inevitably (for $\varLambda _{\mathsf {A} \mathsf {X} \phi }$) or possibly (for $\varLambda _{\mathsf {E} \mathsf {X} \phi }$) leading to a state in the domain $\mathrm {dom} (\varLambda _{\phi })$ of the program semantics of the sub-formula $\phi$ (cf. Definition 1).

Until-Formulas.

Until-formulas $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ express that some desired state (i.e., a state satisfying the sub-formula $\phi _2$) is eventually reached during program execution, either in all traces (if $\mathsf {Q}$ is $\mathsf {A}$) or in at least one trace (if $\mathsf {Q}$ is $\mathsf {E}$), and the sub-formula $\phi _1$ is satisfied in all program states encountered until then. Thus, we can observe that an until-formula is satisfied by finite subsequences of possibly infinite program traces. To reason about subsequences, we define the subsequence function $\mathrm {sq} :\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow \mathcal {P}\left( \varSigma ^+\right)$ which extracts all finite subsequences of a given set of sequences T: $\mathrm {sq} (T) {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma \in \varSigma ^+ \mid \exists \sigma ' \in \varSigma ^*,\sigma '' \in \varSigma ^{*\infty }: \sigma '\sigma \sigma '' \in T \right\}$. In the following, given a formula $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$, we define the corresponding subsequence abstraction $\alpha ^\text {sq} _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}:\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow \mathcal {P}\left( \varSigma ^+\right)$ which extracts the finite subsequences that satisfy $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ from of a set of sequences T. We can then use $\alpha ^\text {sq} _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$ to define the CTL abstraction $\alpha _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}:\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ as shown in Fig. 2. The ranking abstraction $\alpha ^\text {rk}_{\mathsf {Q}} :\mathcal {P}\left( \varSigma ^+\right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ is:

$$\begin{aligned} \alpha ^\text {rk}_{\mathsf {Q}} (T) {\mathop {\,=\,}\limits ^{{\tiny def}}} \alpha ^\text {v}_{\mathsf {Q}} ({\mathop {\alpha }\limits ^{\scriptscriptstyle \rightarrow }} (T)) \end{aligned}$$

(4.1)

where ${\mathop {\alpha }\limits ^{\scriptscriptstyle \rightarrow }} :\mathcal {P}\left( \varSigma ^+\right) \rightarrow \mathcal {P}\left( \varSigma \right) \times \mathcal {P}\left( \varSigma \times \varSigma \right)$ extracts from a given set of non-empty finite sequences T the smallest transition system $\langle S, r \rangle$ that generates $T: {\mathop {\alpha }\limits ^{\scriptscriptstyle \rightarrow }} (T) {\mathop {\,=\,}\limits ^{{\tiny def}}} \langle \mathrm {st} (T), \left\{ \langle s, s' \rangle \in \varSigma \times \varSigma \mid \exists \sigma \in \varSigma ^*, \sigma ' \in \varSigma ^{*\infty }:\sigma ss' \sigma ' \in T \right\} \rangle$ and the function $\alpha ^\text {v}_{\mathsf {Q}} :\mathcal {P}\left( \varSigma \right) \times \mathcal {P}\left( \varSigma \times \varSigma \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ provides the rank of the elements in the domain of the transition relation of the transition system:

$$\begin{aligned} \alpha ^\text {v}_{\mathsf {Q}} \langle S, r \rangle s {\mathop {\,=\,}\limits ^{{\tiny def}}} {\left\{ \begin{array}{ll} 0 &{} \forall s' \in S: \langle s, s' \rangle \not \in r \\ \mathrm {bnd} _\mathsf {Q} \left\{ \alpha ^\text {v}_{\mathsf {Q}} \langle S, r \rangle s' + 1 \Bigg \vert \begin{matrix} s \ne s', \langle s,s' \rangle \in r, \\ s' \in \mathrm {dom} (\alpha ^\text {v}_{\mathsf {Q}} \langle S, r \rangle ) \end{matrix}\right\}&\mathrm {otherwise} \end{array}\right. } \end{aligned}$$

where $\mathrm {bnd} _\mathsf {Q}$ stands for $\mathrm {sup}$, if $\mathsf {Q}$ is $\mathsf {A}$, or $\mathrm {inf}$, if $\mathsf {Q}$ is $\mathsf {E}$. The CTL abstraction $\alpha _{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$ (resp. $\alpha _{\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$) maps the states $\mathrm {st} (T)$ of a given set of sequences T that satisfy $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ to an upper bound (resp. lower bound) on the number of program execution steps until the sub-formula $\phi _2$ is satisfied, for all (resp. at least one of the) executions starting in those states.

Existential Until-Formulas. The subsequence abstraction $\alpha ^\text {sq} _{\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$ for a formula $\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ extracts from a given a set of sequences T the finite subsequence of states that terminate in a state satisfying $\phi _2$ and all predecessor states satisfy $\phi _1$ (and not $\phi _2$). It is defined as follows:

$$\begin{aligned} \begin{aligned} \alpha ^\text {sq} _{\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}(T)&{\mathop {\,=\,}\limits ^{{\tiny def}}} \overline{\alpha }_{\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[\mathrm {dom} (\alpha _{\phi _1}(T))][\mathrm {dom} (\alpha _{\phi _2}(T))]T \\ \overline{\alpha }_{\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[S_1][S_2]T&{\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma s \in \mathrm {sq} (T) \mid \sigma \in (S_1 \setminus S_2)^*, s \in S_2 \right\} \end{aligned} \end{aligned}$$

(4.2)

where $S_1$ is the set of states that satisfy the sub-formula $\phi _1$ (i.e., $\mathrm {dom} (\alpha _{\phi _1}(T))$), and $S_2$ is the set of desired states (i.e., $\mathrm {dom} (\alpha _{\phi _2}(T))$).

Universal Until-Formulas. A finite subsequence of states satisfies a universal until-formula $\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ if and only if it terminates in a state satisfying $\phi _2$, all predecessor states satisfy $\phi _1$, and all other sequences with a common prefix also terminate in a state satisfying $\phi _2$ (and all its predecessors satisfy $\phi _1$), i.e., the program reaches a desired state (via states that satisfy $\phi _1$) independently of the non-deterministic choices made during execution. We define the neighborhood of a sequence of states $\sigma$ in a given set T as the set of sequences $\sigma ' \in T$ with a common prefix with $\sigma$: $\mathrm {nbhd} (\sigma , T) {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma ' \in T \mid \mathrm {pf} (\sigma ) \mathrel {\cap } \mathrm {pf} (\sigma ') \not = \emptyset \right\}$, where the prefixes function $\mathrm {pf} :\varSigma ^{+\infty } \rightarrow \mathcal {P}\left( \varSigma ^{+\infty } \right)$ yields the set of non-empty prefixes of a sequence $\sigma \in \varSigma ^{+\infty }$: $\mathrm {pf} (\sigma ) {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma ' \in \varSigma ^{+\infty } \mid \exists \sigma '' \in \varSigma ^{*\infty }:\sigma = \sigma '\sigma '' \right\}$.

We can now defined the subsequence abstraction $\alpha ^\text {sq} _{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$:

$$\begin{aligned} \begin{aligned} \alpha ^\text {sq} _{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}(T)&{\mathop {\,=\,}\limits ^{{\tiny def}}} \overline{\alpha }_{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[\mathrm {dom} (\alpha _{\phi _1}(T))][\mathrm {dom} (\alpha _{\phi _2}(T))]T \\ \overline{\alpha }_{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[S_1][S_2]T&{\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma s \in \mathrm {sq} (T)~\Bigg \vert ~ \begin{matrix} \sigma \in (S_1 \setminus S_2)^*, s \in S_2, \\ \mathrm {nbhd} (\sigma , \mathrm {sf} (T) \cap \overline{S_2}^{+\infty }) = \emptyset , \\ \mathrm {nbhd} (\sigma , \mathrm {sf} (T) \cap Z) = \emptyset \end{matrix}\right\} \end{aligned} \end{aligned}$$

(4.3)

where the suffixes function $\mathrm {sf} :\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow \mathcal {P}\left( \varSigma ^{+\infty } \right)$ yields the set of non-empty suffixes of a set of sequences T: $\mathrm {sf} (T) {\mathop {\,=\,}\limits ^{{\tiny def}}} \bigcup \left\{ \sigma \in \varSigma ^{+\infty } \mid \exists \sigma ' \in \varSigma ^*: \sigma ' \sigma \in T \right\}$, and $Z {\mathop {\,=\,}\limits ^{{\tiny def}}} \left\{ \sigma s \sigma ' \in \varSigma ^{+\infty } \mid \sigma \in \varSigma ^* \wedge s \in \overline{S_1 \cup S_2} \wedge \sigma ' \in \varSigma ^{+\infty } \right\}$ is the set of sequences of states in which at least one state satisfies neither $\phi _1$ nor $\phi _2$. The last two conjuncts in the definition of the helper function $\overline{\alpha }_{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[S_1][S_2]$ ensure that a finite subsequence satisfies $\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ only if it does not have a common prefix with any subsequence of T that never reaches a desired state in $S_2$ (i.e., $\mathrm {nbhd} (\sigma , \mathrm {sf} (T) \cap \overline{S_2}^{+\infty }) = \emptyset$) and with any subsequence that contains a state that does not belong to $S_1$ and $S_2$ (i.e., $\mathrm {nbhd} (\sigma , \mathrm {sf} (T) \cap Z) = \emptyset$).

Example 1

Let us consider again the acquire/release program of Fig. 1 and let T be the set of its traces. The suffixes starting at program point of the traces in T can be visualized as follows:

Observe that these sequences form a neighborhood in the set $\mathrm {sf} (T)$ of suffixes of T (i.e., the set of all these sequences is the neighborhood $\mathrm {nbhd} (\sigma , \mathrm {sf} (T))$ of any sequence $\sigma$ in the set). In the following, we write $\text {x}_i$ and $\text {n}_i$ for the states denoted above by $\text {x} = i$ and $\text {n} = i$, respectively.

Let us consider the universal until-formula $\mathsf {A} (\text {x} = 1 \mathrel {\mathsf {U}} \text {x} = 0)$. The set of desired states is $S_2 = \left\{ \text {x}_0\right\}$ and $S_1 = \left\{ \text {x}_1\right\} \cup \left\{ \text {n}_i \mid i \in \mathbb {Z} \right\}$ is the set of states that satisfy $\text {x} = 1$. All sequences in the neighborhood have prefixes of the form $\sigma s$ where $\sigma = \text {x}_1 \dots \in (S_1 \cap \overline{S_2})^*$ and $s = \text {x}_0 \in S_2$. Thus, the neighborhood of any subsequence $\sigma s$ does not contain sequences in $\overline{S_2}^{+\infty }$ that never reach the desired state $\text {x}_0$ (i.e., $\mathrm {nbhd} (\sigma s, \mathrm {sf} (T) \cap \overline{S_2}^{+\infty }) = \emptyset$). Furthermore, the neighborhood does not contain sequences in Z in which at least one state neither satisfies $\text {x} = 1$ nor $\text {x} = 0$ (i.e., $\mathrm {nbhd} (\sigma , \mathrm {sf} (T) \cap Z) = \emptyset$). Therefore, the until-formula $\mathsf {A} (\text {x} = 1 \mathrel {\mathsf {U}} \text {x} = 0)$ is satisfied at program point .

Let us consider now the formula $\mathsf {A} (\text {x} = 1 \wedge 0 \le \text {n} \mathrel {\mathsf {U}} \text {x} = 0)$. Again, all sequences in the neighborhood eventually reach the desired state $\text {x}_0$. However, in this case, the set $S_1$ is limited to states with non-negative values for n, i.e., $S_1 = \left\{ \text {x}_1\right\} \,\cup \,\left\{ \text {n}_i \mid 0 \le i \right\}$. Thus, the neighborhood also contains sequences in which at least one state satisfies neither $\text {x} = 1 \wedge 0 \le \text {n}$ nor $\text {x} = 0$ (e.g., the sequence $\text {x}_1\text {n}_{-1}\dots$). Hence $\mathsf {A} (\text {x} = 1 \wedge 0 \le \text {n} \mathrel {\mathsf {U}} \text {x} = 0)$ is not satisfied at program point since $\mathrm {nbhd} (\sigma , \mathrm {sf} (T) \cap Z) \ne \emptyset$. Instead, the existential until-formula $\mathsf {E} (\text {x} = 1 \wedge 0 \le \text {n} \mathrel {\mathsf {U}} \text {x} = 0)$ is satisfied since, for instance, the subsequence $\sigma s$ where $\sigma = \text {x}_1 \text {n}_1$ and $s = \text {x}_0$ satisfies $(\text {x} = 1 \wedge 0 \le \text {n} \mathrel {\mathsf {U}} \text {x} = 0)$.

Until Program Semantics. We now have all the ingredients that define the program semantics $\varLambda _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}:\varSigma \rightharpoonup \mathbb {O}$ for an until-formula $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ (cf. Definition 1). Let $\langle \varSigma \rightharpoonup \mathbb {O}, \sqsubseteq \rangle$ be the partially ordered set for the computational order $f_1 \sqsubseteq f_2 \Leftrightarrow \mathrm {dom} (f_1) \subseteq \mathrm {dom} (f_2) \wedge \forall x \in \mathrm {dom} (f_1): f_1(x) \le f_2(x)$. The program semantics $\varLambda _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$ can be expressed as a least fixpoint in $\langle \varSigma \rightharpoonup \mathbb {O}, \sqsubseteq \rangle$ as:

$$\begin{aligned} \begin{aligned} \varLambda _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}&= \mathrm {lfp} _{\dot{\emptyset }}^\sqsubseteq \varTheta _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[\mathrm {dom} (\varLambda _{\phi _1})][\mathrm {dom} (\varLambda _{\phi _2})] \\ \varTheta _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[S_1][S_2]f&{\mathop {\,=\,}\limits ^{{\tiny def}}} \lambda s. {\left\{ \begin{array}{ll} 0 &{} s \in S_2 \\ \mathrm {bnd} _\mathsf {Q} \left\{ f(s')+1 \mid \langle s, s' \rangle \in \tau \right\} &{} s \in S_1 \wedge s \not \in S_2 \mathrel {\wedge } \\ &{} s \in \mathrm {trans}_\mathsf {Q} (\mathrm {dom} (f)) \\ \mathrm {undefined} &{} \mathrm {otherwise} \end{array}\right. } \end{aligned} \end{aligned}$$

(4.4)

where $\dot{\emptyset }$ is the totally undefined function. The program semantics $\varLambda _{\mathsf {A} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$ (resp. $\varLambda _{\mathsf {E} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$) is a well-founded function mapping each program state in $\mathrm {dom} (\varLambda _{\phi _1})$ inevitably (resp. possibly) leading to a desirable state in $\mathrm {dom} (\varLambda _{\phi _2})$ to an ordinal, which represents an upper bound (resp. lower bound) on the number of program execution steps needed until a desirable state is reached.

Globally-Formulas.

Globally-formulas $\mathsf {Q} \mathsf {G} \phi$ express that $\phi$ holds indefinitely in all traces (if $\mathsf {Q}$ is $\mathsf {A}$) or at least one trace (if $\mathsf {Q}$ is $\mathsf {E}$) starting in a state.

The definition of the CTL abstraction $\alpha _{\mathsf {Q} \mathsf {G} \phi }:\mathcal {P}\left( \varSigma ^{+\infty } \right) \rightarrow (\varSigma \rightharpoonup \mathbb {O})$ for $\mathsf {Q} \mathsf {G} \phi$ given in Fig. 2 retains the value of the CTL abstraction corresponding to the sub-formula $\phi$. Intuitively, each iteration discards the states that satisfy $\phi$ (i.e., the states in $\mathrm {dom} (\alpha _\phi (T))$) but branch to (sub)sequences of T that do not satisfy $\mathsf {Q} \mathsf {G} \phi$. Preserving the value of $\alpha _\phi$ provides more information than just mapping each state to the constant value zero. For instance, the CTL abstraction $\alpha _{\mathsf {A} \mathsf {G} \mathsf {A} \mathsf {F} \phi }$ for a globally-formula $\mathsf {A} \mathsf {G} \mathsf {A} \mathsf {F} \phi$ provides an upper bound on the number of program execution steps needed until the next occurrence of $\phi$ is satisfied, for all executions starting in the corresponding state.

The corresponding program semantics $\varLambda _{\mathsf {Q} \mathsf {G} \phi }:\varSigma \rightharpoonup \mathbb {O}$ (cf. Definition 1) preserves the value of $\varLambda _\phi$ for each state satisfying the sub-formula $\phi$ and inevitably (if $\mathsf {Q}$ is $\mathsf {A}$) or possibly (if $\mathsf {Q}$ is $\mathsf {E}$) leading only to other states that also satisfy $\phi$.

Other Formulas.

We are left with describing the CTL abstraction of $\lnot \phi$, $\phi \wedge \phi$, and $\phi \vee \phi$ defined in Fig. 2. For a negation $\lnot \phi$, the CTL abstraction $\alpha _{\lnot \phi }$ maps each program state that does not satisfy $\phi$ to the value zero. The CTL abstraction for a binary formula $\phi _1 \wedge \phi _2$ or $\phi _1 \vee \phi _2$ retains the largest value of the functions $\varLambda _{\phi _1}$ and $\varLambda _{\phi _2}$ for each program state satisfying both $\phi _1$ and $\phi _2$; for a disjunction $\phi _1 \vee \phi _2$, it also retains the value of the function for each program state satisfying either sub-formula.

Theorem 1

A program satisfies a CTL formula $\phi$ for all traces starting from a given set of states $\mathcal {I}$ if and only if $\mathcal {I} \subseteq \mathrm {dom} (\varLambda _\phi )$.

Proof

The proof proceeds by induction over the structure of the CTL formula $\phi$. The base case are atomic propositions a for which the proof is immediate.

For a next-formulas $\mathsf {Q} \mathsf {X} \phi$, by induction hypothesis, $\mathrm {dom} (\varLambda _\phi )$ coincides with the set of states that satisfy $\phi$. By Definition 1 and the definition of $\alpha _{\mathsf {Q} \mathsf {X} \phi }$ in Fig. 2, the domain of $\varLambda _{\mathsf {Q} \mathsf {X} \phi }$ coincides with $\mathrm {trans}_\mathsf {Q} (\mathrm {dom} (\alpha _{\phi }(T)))$. Thus, by definition of $\mathrm {trans}_\mathsf {Q}$, we have that $\mathrm {dom} (\varLambda _{\mathsf {Q} \mathsf {X} \phi })$ coincides with the set of states that satisfy $\mathsf {Q} \mathsf {X} \phi$ (cf. Eqs. 3.1 and 3.2).

For an until-formula $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$, by induction hypothesis, $\mathrm {dom} (\varLambda _{\phi _1})$ and $\mathrm {dom} (\varLambda _{\phi _2})$ coincide with the set of states that satisfy $\phi _1$ and $\phi _2$, respectively. We have $\varLambda _\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2) = \varTheta _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}[\mathrm {dom} (\varLambda _{\phi _1})][\mathrm {dom} (\varLambda _{\phi _2})](\varLambda _\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2))$ from Eq. 4.4. Therefore, by definition of $\varTheta _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$, $\mathrm {dom} (\varLambda _\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2))$ coincides with the states that satisfy $\phi _2$ and all states that satisfy $\phi _1$ and inevitably (if $\mathsf {Q}$ is $\mathsf {A}$) or possibly (if $\mathsf {Q}$ is $\mathsf {E}$) lead to states that satisfy $\phi _2$. So $\mathrm {dom} (\varLambda _\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2))$ coincides with the states that satisfy $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ (cf. Eqs. 3.1 and 3.2).

For a globally-formula $\mathsf {Q} \mathsf {G} \phi$, by induction hypothesis, $\mathrm {dom} (\varLambda _\phi )$ coincides with the set of states that satisfy $\phi$. By Definition 1 and the definition of $\alpha _{\mathsf {Q} \mathsf {G} \phi }$ in Fig. 2, we have that $\varLambda _{\mathsf {Q} \mathsf {G} \phi } = \varTheta _{\mathsf {Q} \mathsf {G} \phi }(\varLambda _{\mathsf {Q} \mathsf {G} \phi })$. Therefore, by definition of $\varTheta _{\mathsf {Q} \mathsf {G} \phi }$, we have that $\mathrm {dom} (\varLambda _{\mathsf {Q} \mathsf {G} \phi })$ coincides with the states that satisfy $\phi$ inevitably (if $\mathsf {Q}$ is $\mathsf {A}$) or possibly (if $\mathsf {Q}$ is $\mathsf {E}$) lead to other states that satisfy $\phi$. So $\mathrm {dom} (\varLambda _{\mathsf {Q} \mathsf {G} \phi })$ coincides with the states that satisfy $\mathsf {Q} \mathsf {G} \phi$ (cf. Eqs. 3.1 and 3.2).

Finally, all other cases ($\lnot \phi$, $\phi _1 \wedge \phi _2$, and $\phi _1 \vee \phi _2$) follow immediately from the induction hypothesis, the semantics of the CTL formulas (cf. Eq. 3.1) and the definition of the corresponding program semantics (cf. Definition 1 and the CTL abstractions in Fig. 2). $\square$

The program semantics for a CTL formula is not computable when the program state space is infinite. In the next section, we present decidable abstractions by means of piecewise-defined functions [38, 39].

5 Static Analysis for CTL Properties

We recall here the features of the abstract domain of piecewise-defined functions [39] that are relevant for our purposes, and describe the new elements that we need to introduce to obtain a static analysis for proving CTL properties. We refer to [38] for an exhaustive presentation of the original abstract domain.

For illustration, we model a program using a control flow graph $\langle \mathcal {L}, E \rangle$, where $\mathcal {L}$ is the set of program points and $E \subseteq \mathcal {L} \times A \times \mathcal {L}$ is the set of edges in the control flow graph. Each edge is labeled by an action $s \in A$; possible actions are $\text {skip}$, a boolean condition b, or an assignment $x := e$. In the following, we write out(l) to denote the set of outgoing edges from a program point l.

Fig. 3.

Simplified decision tree representation of the piecewise-defined function inferred at program point of the program of Fig. 1 (cf. Eq. 1.1). Each constraint is satisfied by the left subtree of the decision node, while the right subtree satisfies its negation. The leaves represent partial functions whose domain is determined by the constraints satisfied along the path to the leaf.

Piecewise-Defined Functions Abstract Domain.

An element $t \in \mathcal {T}$ of the abstract domain is a piecewise-defined partial function represented by a decision tree, where the decision nodes are labeled by linear constraints over the program variables, and the leaf nodes are labeled by functions of the program variables. The decision nodes recursively partition the space of possible values of the program variables, and the leaf nodes represent the value of the function corresponding to each partition. An example of (simplified) decision tree representation of a piecewise-defined function is shown in Fig. 3.

Specifically, the decision nodes are labeled by linear constraints supported by an existing underlying numerical domain, i.e., interval [15] constraints (of the form $\pm \text {x} \le \text {c}$), octagonal [30] constraints (of the form $\pm \text {x}_i \pm \text {x}_j \le c$), or polyhedral [19] constraints (of the form $\text {c}_1 \cdot \text {x}_1 + \dots + \text {c}_k \cdot \text {x}_k \le \text {c}_{k+1}$). The leaf nodes are labeled by affine functions of the program variables (of the form $\text {m}_1 \cdot \text {x}_1 + \dots + \text {m}_k \cdot \text {x}_k + \text {q}$), or the special elements $\bot$ and $\top$, which explicitly represent undefined functions. The element $\top$ is introduced to manifest an irrecoverable precision loss of the analysis. We also support lexicographic affine functions $(\text {f}_k, \dots , \text {f}_1, \text {f}_0)$ in the isomorphic form of ordinals $\omega ^k \cdot \text {f}_k + \dots + \omega \cdot \text {f}_1 + \text {f}_0$ [29, 40].

The partitioning is dynamic: during the analysis of a control flow graph, partitions (i.e. decision nodes and constraints) are modified by assignments and split (i.e., added) by boolean conditions and when merging control flows. More specifically, for each action $s \in A$, we define sound over-approximating abstract transformers $\llbracket {s}\rrbracket _o:\mathcal {T} \rightarrow \mathcal {T}$ as well as new under-approximating abstract transformers $\llbracket {s}\rrbracket _u:\mathcal {T} \rightarrow \mathcal {T}$. These transformers always increase by one the value of the functions labeling the leaves of a given decision tree to count the number of executed program steps (i.e., actions in the control flow graph). The transformers for boolean conditions and assignments additionally modify the decision nodes by building upon the underlying numerical abstract domain. For instance, the abstract transformer $\llbracket {b}\rrbracket _o$ (resp. $\llbracket {b}\rrbracket _u$) for a boolean condition b uses the underlying numerical domain to obtain an over-approximation (resp. an under-approximation) of b as a set of linear constraints; then it adds these constraints to the given decision tree and discards the paths that become unfeasible (because they do not satisfy the added constraints). Let $\left\{ n \le 0 \right\}$ (resp. $\left\{ n = 0\right\}$) be the set of constraints obtained by $\llbracket {b}\rrbracket _o$ (resp. $\llbracket {b}\rrbracket _u$) for the boolean condition $b \equiv n \le 0 \wedge n \% 2 = 0$; then, given the right subtree in Fig. 3, $\llbracket {b}\rrbracket _o$ (resp. $\llbracket {b}\rrbracket _u$) would discard the path leading to the leaf with value $2n + 2$ by replacing it with a leaf with undefined value $\bot$ (resp. replace $n \le 0$ with $n = 0$ and replace $2n + 2$ with $\bot$). Decision trees are merged using either the approximation join $\curlyvee$ or the computational join $\sqcup$. Both join operators add missing decision nodes from either of the given trees; $\curlyvee$ retains the leaves that are labeled with an undefined function in at least one of the given trees, while $\sqcup$ preserves the leaves that are labeled with a defined function over the leaves labeled with $\bot$ (but preserves the leaves labeled with $\top$ over all other leaves). To minimize the cost of the analysis and to enforce termination, a (dual) widening operator limits the height of the decision trees and the number of maintained partitions.

Fig. 4.

Abstract program semantics $\varLambda ^\natural _\phi$ for each CTL formula $\phi$. The join operator and the abstract transformer $\llbracket {s}\rrbracket _\mathsf {Q}$ respectively stand for $\sqcup$ and $\llbracket {s}\rrbracket _u$, if $\mathsf {Q}$ is $\mathsf {E}$, or $\curlyvee$ and $\llbracket {s}\rrbracket _o$, if $\mathsf {Q}$ is $\mathsf {A}$. With abuse of notation, we use $\bot$ to denote a decision tree with a single undefined leaf node.

Abstract Program Semantics for CTL Properties. The abstract program semantics $\varLambda ^\natural _\phi :\mathcal {L} \rightarrow \mathcal {T}$ for a CTL formula $\phi$ maps each program point $l \in \mathcal {L}$ to an element $t \in \mathcal {T}$ of the piecewise-defined functions abstract domain. The definition of $\varLambda ^\natural _\phi$ for each CTL formula $\phi$ is summarized in Fig. 4 and explained in some detail below. More details and formal definitions can be found in [37, 38].

The analysis starts with the totally undefined function (i.e., a decision tree that consists of a single leaf with undefined value $\bot$) at the final program points (i.e., nodes without outgoing edges in the control flow graph). Then it proceeds backwards through the control flow graph, taking the encountered actions into account, and joining decision trees when merging control flows. For existential CTL properties, the analysis uses the under-approximating abstract transformers $\llbracket {s}\rrbracket _u$ for each action s, to ensure that program states that do not satisfy the CTL property are discarded (i.e., removed from the domain of the current piecewise-defined function), and joins decision trees using the computational join $\sqcup$, to ensure that the current piecewise-defined function remains defined over states that satisfy the CTL property in at least one of the merged control flows. Dually, for universal CTL properties, the analysis uses the over-approximating abstract transformers $\llbracket {s}\rrbracket _o$ and joins decision trees using the approximation join $\curlyvee$, to ensure that the current piecewise-defined function remains defined only over states that satisfy the CTL property in all of the merged control flows.

At each program point, the analysis additionally performs operations that are specific to the considered CTL formula $\phi$. For an atomic proposition a (cf. Eq. 5.1), the analysis performs a $\textsc {reset}\llbracket {a}\rrbracket$ operation, which is analogous to the under-approximating transformer for boolean conditions but additionally replaces all the leaves that satisfy a with leaves labeled with the function with value zero. For example, given the atomic proposition $n = 0$ and the right subtree in Fig. 3, $\textsc {reset}\llbracket {n = 0}\rrbracket$ would replace the constraint $n \le 0$ with $n = 0$, the leaf $2n + 2$ with $\bot$ and the leaf 2 with 0. For a next-formula $\mathsf {Q} \mathsf {X} \phi$ (cf. Eq. 5.2), the analysis approximates the effect of the transition from each program point l to each successor program point $l'$ and performs a $\textsc {zero}$ operation to replace all defined functions labeling the leaves of the so obtained decision tree with the function with value zero. For an until-formula $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$ (cf. Eq. 5.4), the analysis performs an ascending iteration with widening [13]. At each iteration, the analysis approximates the effect of the transition from each program point l to each successor program point $l'$ and performs an $\textsc {until}$ operation to model the until temporal operator: $\textsc {until}$ replaces with the function with value zero all leaves that correspond to defined leaves in the decision tree $\varLambda ^\natural _{\phi _2}(l)$ obtained for $\phi _2$, and retains all leaves that are labeled with an undefined function in both $\varLambda ^\natural _{\phi _1}(l)$ and $\varLambda ^\natural _{\phi _1}(l)$. For a globally-formula $\mathsf {Q} \mathsf {G} \phi$ (cf. Eq. 5.5), the analysis performs a descending iteration with dual widening [41], starting from the abstract semantics $\varLambda ^\natural _\phi$ obtained for $\phi$. At each iteration, the $\textsc {mask}$ operation models the globally temporal operator: it discards all defined partitions in $\varLambda ^\natural _\phi (l)$ that become undefined as a result of the transition from each program point l to each successor program point $l'$; at the limit, the only defined partitions are those that remain defined across transitions and thus satisfy the globally-formula. For a negation formula $\lnot \phi$ (cf. Eq. 5.5), the analysis performs a $\textsc {complement}$ operation on the decision tree $\varLambda ^\natural _\phi (l)$ obtained for $\phi$ at each program point l; $\textsc {complement}$ replaces all defined functions labeling the leaves of a decision tree with $\bot$, and all $\bot$ with the function with value zero. Note that $\varLambda ^\natural _\phi$ is an abstraction of $\varLambda _\phi$ and thus not all undefined partitions in $\varLambda ^\natural _\phi$ necessarily correspond to undefined partitions in $\varLambda _\phi$. Leaves that are undefined in $\varLambda ^\natural _\phi$ due to this uncertainty are labeled with $\top$, and are left unchanged by $\textsc {complement}$ to guarantee the soundness of the analysis. Finally, for binary formulas $\phi _1 \wedge \phi _2$ and $\phi _1 \vee \phi _2$, the abstract semantics $\varLambda ^\natural _{\phi _1 \wedge \phi _2}$ and $\varLambda ^\natural _{\phi _1 \vee \phi _2}$ (cf. Eqs. 5.6 and 5.7) merge the decision trees obtained for $\phi _1$ and $\phi _2$ using the approximation join $\curlyvee$ and the computational join $\sqcup$, respectively.

The abstract program semantics $\varLambda ^\natural _\phi$ for each CTL formula $\phi$ is sound with respect to the approximation order $f_1 \preccurlyeq f_2 \Leftrightarrow \mathrm {dom} (f_1) \supseteq \mathrm {dom} (f_2) \wedge \forall x \in \mathrm {dom} (f_1): f_1(x) \le f_2(x)$, which means that the abstract semantics $\varLambda ^\natural _\phi$ over-approximates the value of the concrete semantics $\varLambda _\phi$ and under-approximates its domain of definition $\mathrm {dom} (\varLambda _\phi )$. In this way, the abstraction provides sufficient preconditions for the CTL property $\phi$: if the abstraction is defined for a state then that state satisfies $\phi$.

Theorem 2

A program satisfies a CTL formula $\phi$ for all traces starting from a given set of states $\mathcal {I}$ if $\mathcal {I} \subseteq \mathrm {dom} (\gamma (\varLambda ^\natural _\phi ))$.

Proof

(Sketch). The proof proceeds by induction over the structure of the formula $\phi$. The base case are atomic propositions for which the proof is immediate.

For a next-formula $\mathsf {Q} \mathsf {X} \phi$, by induction hypothesis, $\mathrm {dom} (\varLambda ^\natural _\phi )$ is a subset of the set of states that satisfy $\phi$. Using the over-approximating transformers $\llbracket {s}\rrbracket _o$ together with the approximation join $\curlyvee$ (resp. the under-approximating transformers $\llbracket {s}\rrbracket _u$ together with the computational join $\sqcup$) ensures that $\varLambda ^\natural _{\mathsf {Q} \mathsf {X} \phi }$ soundly under-approximates the set of states that satisfy $\mathsf {Q} \mathsf {X} \phi$.

For an until-formula $\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)$, by induction hypothesis, $\mathrm {dom} (\varLambda ^\natural _{\phi _1})$ and $\mathrm {dom} (\varLambda ^\natural _{\phi _2})$ are a subset of the set of states that satisfy $\phi _1$ and $\phi _2$, respectively. By definition, $\varLambda _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$ is the limit of an ascending iteration sequence using widening. Again, using the over-approximating transformers $\llbracket {s}\rrbracket _o$ together with the approximation join $\curlyvee$ (resp. the under-approximating transformers $\llbracket {s}\rrbracket _u$ together with the computational join $\sqcup$) guarantees the soundness of the analysis with respect to each transition. The soundness of each iteration without widening is then guaranteed by the definition of the $\textsc {until}$ operation. The iterations with widening are allowed to be unsound but the limit of the iterations (i.e., $\varLambda _{\mathsf {Q} (\phi _1 \mathrel {\mathsf {U}} \phi _2)}$) is guaranteed to soundly under-approximate the set of states that satisfy $(\phi _1 \mathrel {\mathsf {U}} \phi _2)$. We refer to [38] for a detailed proof for formulas of the form $(true \mathrel {\mathsf {U}} \phi _2)$. The generalization to $(\phi _1 \mathrel {\mathsf {U}} \phi _2)$ is trivial.

For a globally-formula $\mathsf {Q} \mathsf {G} \phi$, $\varLambda _{\mathsf {Q} \mathsf {G} \phi }$ is the limit of a descending iteration sequence with dual widening, starting from $\varLambda ^\natural _\phi$, which soundly under-approximates the set of states that satisfy $\phi$. The soundness of each iteration is guaranteed by the definition of the $\textsc {mask}$ operation and the dual widening operator (see [38]).

The case of a negation $\lnot \phi$ is non-trivial since, by induction hypothesis, $\mathrm {dom} (\varLambda ^\natural _\phi )$ is a subset of the set of states that satisfy $\phi$. Specifically, $\varLambda ^\natural _\phi$ maps each program point $l \in \mathcal {L}$ to a decision tree whose leaves determine this under-approximation: leaves labeled with $\bot$ represent states that do not satisfy $\phi$ while leaves labeled with $\top$ represent states that may or may not satisfy $\phi$. The $\textsc {complement}$ operation performed by $\varLambda ^\natural _{\lnot \phi }$ only considers leaves labeled by $\bot$ and ignores (i.e., leaves unchanged) leaves labeled by $\top$. Thus, $\varLambda ^\natural _{\lnot \phi }$ soundly under-approximates the set of states that satisfy $\lnot \phi$.

Finally, for binary formulas $\phi _1 \wedge \phi _2$ and $\phi _1 \vee \phi _2$, the proof follows immediately from the definition of the approximation join $\curlyvee$ and the computational join $\sqcup$ used in the definition of $\varLambda ^\natural _{\phi _1 \wedge \phi _2}$ and $\varLambda ^\natural _{\phi _1 \vee \phi _2}$, respectively. $\square$

6 Implementation

The proposed static analysis method for proving CTL properties is implemented in the prototype static analyzer $\textsc {FuncTion}$ [13].

The implementation is in OCaml and consists of around 9K lines of code. The current front-end of $\textsc {FuncTion}$ accepts non-deterministic programs written in a C-like syntax (without support for pointers, struct and union types). The only basic data type is mathematical integers. $\textsc {FuncTion}$ accepts CTL properties written using a syntax similar to the one used in the rest of this paper, with atomic propositions written as C-like pure expressions. The abstract domain of piecewise-defined functions builds on the numerical abstract domains provided by the Apron library [24], and the under-approximating numerical operators provided by the Banal static analyzer [31].

The analysis is performed backwards on the control flow graph of a program with a standard worklist algorithm [32], using widening and dual widening at loop heads. Non-recursive function calls are inlined, while recursion is supported by augmenting the control flow graphs with call and return edges. The precision of the analysis can be tuned by choosing the underlying numerical abstract domain, by activating the extension to ordinal-value functions [40], and by adjusting the precision of the widening [13] and the widening delay. It is also possible to refine the analysis by considering only reachable states.

Fig. 5.

Evaluation of $\textsc {FuncTion}$ on selected test cases collected from various sources. All test cases were analyzed using polyhedral constraints for the decision nodes, and affine functions for the leaf nodes of the decision tree.

Experimental Evaluation. We evaluated our technique on a number of test cases obtained from various sources, and compared $\textsc {FuncTion}$ against T2 [8] and Ultimate LTL Automizer [20] as well as E-HSF [4], and the prototype implementation from [10]. Figs. 5 and 6 show an excerpt of the results, which demonstrates the differences between $\textsc {FuncTion}$, T2 [8] and Ultimate LTL Automizer. The first set of test cases are programs that we used to test our implementation. The second and third set were collected from [25] and the web interface of Ultimate LTL Automizer [20]. The fourth set are examples from the termination category of the 6th International Competition on Software Verification (SV-COMP 2017). The experiments were conducted on an Intel i7-6600U processor with 20 GB of RAM on Arch Linux with Linux 4.11 and OCaml 4.04.1.

$\textsc {FuncTion}$ passes all test cases with the exception of 2.4, 3.9, 3.14, and 3.15, which fail due to imprecisions introduced by the widening, and 1.8 and 4.1, which fail due to an unfortunate interaction of the under-approximations needed for existential properties and non-deterministic assignments in the programs. However, note that for these test cases we still get some useful information. For instance, for 3.15, $\textsc {FuncTion}$ infers that the CTL property is satisfied if $\text {x} < 0$.

Fig. 6.

Differences between $\textsc {FuncTion}$, T2, and Ultimate LTL Automizer.

In Fig. 6, the missing results for T2 are due to a missing conversion of the test cases to the T2 input format. The comparison with Ultimate LTL Automizer is limited to the test cases where the CTL property can be equivalently expressed in LTL (i.e., universal CTL properties). The results show that only $\textsc {FuncTion}$ succeeds on numerous test cases (1.2, 1.4, 1.7, 1.11, 1.12, 4.3, 4.4, and 4.5). Ultimate LTL Automizer performs well on the supported test cases, but $\textsc {FuncTion}$ still succeeds on most of the test cases provided by Ultimate LTL Automizer (not shown in Fig. 6, since there are no differences between the results of $\textsc {FuncTion}$ and Ultimate LTL Automizer). Overall, none of the tools subsumes the others. In fact, we observe that their combination is more powerful than any of the tools alone, as it would succeed on all test cases.

Finally, $\textsc {FuncTion}$ only succeeds on two of the industrial benchmarks from [10], while T2, E-HSF and [10] fare much better (see [8, Fig. 11]). The reason for the poor performance is that in these benchmarks the effect of function calls is modeled as a non-deterministic assignment and this heavily impacts the precision of $\textsc {FuncTion}$. We are confident that we would obtain better results on the original benchmarks, where function calls are not abstracted away.

7 Related Work

In the recent past, a large body of work has been devoted to proving CTL properties of programs. The problem has been extensively studied for finite-state programs [7, 26, etc.], while most of the existing approaches for infinite-state systems have limitations that restrict their applicability. For instance, they only support certain classes of programs [36], or they limit their scope to a subset of CTL [11], or to a single CTL property such as termination [27, 34, etc.] or non-termination [2, 5, etc.]. Our approach does not suffer from these limitations.

Some other approaches for proving CTL properties do not reliably support CTL formulas with arbitrary nesting of universal and existential path quantifiers [23], or support existential path quantifiers only indirectly by building upon recent work for proving non-termination [22], or by considering their universal dual [8]. In particular, the latter approach is problematic: since the universal dual of an existential until formula is non-trivial to define, the current implementation of T2 does not support such formulas (see Fig. 6). Other indirect approaches [4, 10] perform unnecessary computations that result in slower runtimes (see [8, Fig. 12]). In comparison to all these approaches, our approach provides strictly more information in the form of a ranking function whose domain gives a precondition for a given CTL property and whose value estimates the number of program execution steps until the property is satisfied.

In [17], Cousot and Cousot define a trace-based semantics for a very general temporal language which subsumes LTL and CTL; this is subsequently abstracted to a state-based semantics. The abstraction has been later shown to be incomplete by Giacobazzi and Ranzato [21]. In contrast to the work of Cousot and Cousot, we do not define a trace-based semantics for CTL. The semantics that we propose is close to their state-based semantics in that their state-based semantics coincides with the domain of the functions that we define. Note that Theorem 1 is not in contrast with the result of Giacobazzi and Ranzato because completeness is proven with respect to the state-based semantics of CTL.

Finally, our abstract interpretation framework generalizes an existing framework [41] for proving guarantee and recurrence properties of programs [28]. Guarantee and recurrence properties are equivalently expressed in CTL as $\mathsf {A} (true\mathrel {\mathsf {U}} \phi )$ and $\mathsf {A} \mathsf {G} \mathsf {A} (true\mathrel {\mathsf {U}} \phi )$, respectively. In fact, we rediscover the guarantee and recurrence program semantics defined in [41] as instances of our framework: the guarantee semantics coincides with $\varLambda _{\mathsf {A} (true\mathrel {\mathsf {U}} \phi )}$ (cf. Sect. 4) and the recurrence semantics coincides with $\varLambda _{\mathsf {A} \mathsf {G} \mathsf {A} (true\mathrel {\mathsf {U}} \phi )}$ (cf. Sect. 4). The common insight with our work is the observation that CTL (sub)formulas are satisfied by finite subsequences (which can also be single states) of possibly infinite sequences. The program semantics for these (sub)formulas then counts the number of steps in these subsequences. Our work generalizes this idea to all CTL formulas and integrates the corresponding semantics in a uniform framework.

8 Conclusion and Future Work

In this paper, we have presented a new static analysis method for inferring preconditions for CTL properties of programs that overcomes the limitations of existing approaches. We have derived our static analysis within the framework of abstract interpretation by abstraction of the operational trace semantics of a program. Using experimental evidence, we have shown that our analysis is effective and performs well on a wide variety of benchmarks, and is able to prove CTL properties that are out of reach for state-of-the-art tools.

It remains for future work to investigate and improve the precision of the analysis in the presence of non-deterministic program assignments. We also plan to support LTL properties [20] or, more generally, CTL$^*$ properties [9]. This requires some form of trace partitioning [35] as the interpretation of LTL formulas is defined in terms of program executions instead of program states as CTL.