Keywords

1 Introduction

FO transition systems (FO for First-order) are a convenient tool for specifying systems where the number of agents is not known in advance. This is very useful for modeling systems like network protocols [22] or web-based workflows like conference management, banking or commerce platforms. Consider, e.g., the specification from Fig. 1 modeling parts of the review process of a conference management system as a FO transition system.

Fig. 1.
figure 1

A conference management system.

Full size image

Assume that initially, all predicates with the exception of \(\textsf {auth}\) are false, i.e., the property \({\mathcal {H}}\) given by

$$\begin{aligned} \begin{aligned} \forall x_1,x_2,p,r,d.&\lnot \textsf {conf}(x_1,p)\wedge \lnot \textsf {assign}(x_1,p)\ \wedge \\&\lnot \textsf {report}(x_1,p,r)\wedge \lnot \textsf {discuss}(x_1,x_2,p,d) \end{aligned} \end{aligned}$$
(1)

holds. The predicates \(A_1,\ldots ,A_4\) are input predicates whose values either represent agents’ decisions or actions from the environment. Intuitively, the transition system works as follows: First, each PC member x possibly declares her conflict with each paper p. Then, papers p are assigned to PC members x in such a way that the conf relation is respected. Repeatedly, reports for PC members x about papers p arrive, where a subsequent discussion between PC members \(x_1,x_2\) on some paper p is only possible if both have received a report on that paper and may update their reviews based on the discussions. Variants of this example have already been studied in [19, 25].

A useful property to ensure in this example is that a discussion between \(x_1\) and \(x_2\) on some paper p is only possible if neither \(x_1\) nor \(x_2\) are authors of p:

$$\begin{aligned} \forall x_1,x_2,p,d.\lnot \textsf {discuss}(x_1,x_2,p,d)\vee \lnot \textsf {auth}(x_1,p)\wedge \lnot \textsf {auth}(x_2,p) \end{aligned}$$
(2)

As FO predicate logic is undecidable, we cannot hope to find an effective algorithm for proving an invariant such as (2) for arbitrary FO transition systems. That does not exclude, though, that at least some invariants can be proven inductive and thus, to be valid. Also, approximation techniques may be conceived to construct strengthenings of given invariants which, hopefully turn out to be inductive and thus may serve as certificates for the invariants in question.

The idea of using FO predicate logic for specifying the semantics of systems has perhaps been pioneered by abstract state machines (ASMs) [6, 7, 14]. Recently, it has successfully been applied for the specification and verification of software-defined networks [2, 20], of network protocols [23], of distributed algorithms [22]. The corresponding approach is built into the tool Ivy [18, 23]. Ivy is a proof assistant for systems specified in FO logic which is carefully designed around a decidable many-sorted extension of EPR (Effectively Propositional Logic, or \(\exists ^*\forall ^*\)FO logic). In the base setting, invariants are provided manually and then checked for inductiveness by the theorem prover Z3 [8]. Some effort, though, has been invested to come up with more automatic techniques for specific settings such as threshold algorithms [4] or more general FO invariant inference [15, 16]. The fundamental problem thereby is that repeated application of the weakest precondition operator may introduce additional first-order variables, new instances of input predicates or existential quantifiers and thus result in formulas outside the decidable fragment of FO logic.

This problem also has been encountered in  [10, 11, 19] where noninterference [13] is investigated for multi-agent workflows in the spirit of the conference management system from Fig. 1. In [19], the authors present a a symbolic verification approach where the agent capabilities as well as declassification and self-composition of the original system \(\mathcal {T}\) is encoded into a FO transition system \(\mathcal {T}^2\). Noninterference of the original system is thus reduced to a universal invariant of the resulting system \(\mathcal {T}^2\). Further abstraction (i.e., strengthening of the encountered formulas) is applied in order to arrive at a practical algorithm which iteratively strengthens the initial invariant.

Only for rare cases, so far, decidability could be shown. In [21], Sagiv et al. show that inferring universal inductive invariants is decidable when the transition relation is expressed by formulas with unary predicates and a single binary predicate restricted by the background theory of singly-linked-lists. The same problem becomes undecidable when the binary symbol is not restricted by a background theory. In [19] on the other hand, syntactic restrictions are introduced under which termination at least of an abstract fixpoint iteration can be guaranteed. The abstraction thereby, consists in strengthening each occurring existential quantifier via appropriate instantiations (see also [9]). The syntactic restrictions proposed in [19] essentially amount to introducing a stratification on the predicates and restricting substitutions to be stratified and guarded updates. It is argued that these restrictions are not unrealistic in specifications of multi-agent systems where the computation proceeds in stages each of which accumulates information based on the results obtained in earlier stages. The example transition system from Fig. 1, e.g., is stratified: there is a mapping \(\lambda \) assigning a level \(\lambda (R)\) to each predicate R so that the predicates occurring in right-hand sides which are distinct from the left-hand side have lower levels. In the example, \(\lambda \) could be given by

$$ \{ \textsf {auth}\mapsto 0, \textsf {conf}\mapsto 1, \textsf {assign}\mapsto 2, \textsf {report}\mapsto 3, \textsf {discuss}\mapsto 4 \} $$

Intuitively, stratification limits dependencies between predicates to be acyclic. Examples of stratified guarded updates on the other hand, are the two statements in the loop body of Fig. 1. Guarded updates only allow to extend predicates where the extensions constrain the use of existential quantifiers to the format \(\varphi \vee \exists \bar{z}.A\bar{y}\bar{z}\wedge \psi \) for some input predicate A and quantifier-free subformulas \(\varphi ,\psi \).

The loop of the example thus satisfies the requirements of [19], implying that an abstract fixpoint iteration is guaranteed to terminate for every universal invariant. Here, we show that under the given assumptions, no abstraction is required: the concrete fixpoint iteration in question already terminates and returns the weakest inductive invariant, which happens to consist of universal formulas only. We conclude that universal invariants for the given class of FO transition systems are decidable.

Beyond that, we extend this class of FO transition systems by additionally allowing stratified guarded resets such as the two assignments before the loop in Fig. 1. Guarded stratified resets are seemingly easier than updates, as they define their left-hand sides solely in terms of predicates of lower levels. In full generality, though, when there are both updates and resets, we failed to prove that universal invariants are decidable. We only succeed so—provided further (mild) restrictions are satisfied. Our results are that jointly, stratified guarded updates and resets can be allowed

  • when resets refer to predicates at the highest and at the lowest level of the stratification only; or

  • when all predicates of level at least 1, occur in right-hand sides only positively; or

  • when all updates are not only guarded, but strictly guarded.

2 Basic Definitions

Assume that we are given a finite set of predicate names \(\mathcal {R}\) together with a finite set of constant names \(\mathcal {C}\). A FO structure \(s=\langle I,\rho \rangle \) over a given universe \(\mathcal {U}\) consists of an interpretation I of the predicates in \(\mathcal {R}\), i.e., a mapping which assigns to each predicate \(R\in \mathcal {R}\) of arity \(k\ge 0\), a k-ary relation over \(\mathcal {U}\), together with a valuation \(\rho :\mathcal {C}\rightarrow \mathcal {U}\) which assigns to each constant name an element in \(\mathcal {U}\). The semantics of FO (first-order) formulas as well as SO (second-order) formulas with free occurrences of predicates and variables in \(\mathcal {R}\) and \(\mathcal {C}\), respectively, is defined as usual. We write \(s\models \varphi \) or \(I,\rho \models \varphi \) to denote that \(\varphi \) is valid for the given interpretation I and valuation \(\rho \) as provided by s. For FO transition systems, we distinguish between the set \({\mathcal {R}_{ state }}\) of state predicates and the disjoint set \(\mathcal {A}\) of input predicates. While the values of constants as well as the interpretation of the state predicates constitute the state attained by the system, the input predicates are used to model (unknown) input from the environment or decisions of participating agents.

At each transition of a FO transition system, the system state \(s'\) after the transition is determined in terms of the system state s before the transition via a substitution \(\theta \). For each state predicate \(R\in {\mathcal {R}_{ state }}\), \(\theta \) provides a FO formula to specify the interpretation of R after the transition in terms of the interpretation and valuation in s.

Technically, we introduce a set \(\mathcal {Y}= \{y_i\mid i\in \mathbb {N}\}\) of distinct formal parameters where \(\mathcal {C}\cap \mathcal {Y}=\emptyset \). For a predicate R of arity \(k\ge 0\), we write \(R\bar{y}\) for the literal \(R(y_1,\ldots ,y_k)\) and assume that each substitution \(\theta \) maps each literal \(R\bar{y}\), \(R\in {\mathcal {R}_{ state }}\), to some FO formula \(\theta (R\bar{y})\) with predicates in \({\mathcal {R}_{ state }}\cup \mathcal {A}\) and free variables either from \(\mathcal {C}\) or occurring among the variables in \(\bar{y}\). In case that \(\theta (R\bar{y}) = \psi \) and \(\theta (R'\bar{y}) = R'\bar{y}\) for all \(R'\in {\mathcal {R}_{ state }}\setminus \{R\}\), we also denote \(\theta \) by \(R\bar{y}\,{:=}\,\psi \).

Example 1

In the example from Fig. 1, \({\mathcal {R}_{ state }}\) consists of the predicates \(\textsf {conf}\), \(\textsf {auth}\), \(\textsf {assign}\), \(\textsf {report}\) and \(\textsf {discuss}\) while \({\mathcal {R}_{ input }}\) consists of the predicates \(A_1\ldots A_4\). No constants are needed, so \(\mathcal {C}= \emptyset \). The edge from node 1 to 2, e.g., specifies a substitution \(\theta \) that updates \(\textsf {assign}\) with

$$ \theta (\textsf {assign}(x,p)) = A_2(x,p) \wedge \lnot \textsf {conf}(x,p) $$

but does not change literals of predicates \(\textsf {conf},\textsf {auth},\textsf {report}\) or \(\textsf {discuss}\).    \(\square \)

Applying \(\theta \) to a FO formula \(\varphi \) results in the FO formula \(\theta (\varphi )\) which is obtained from \(\varphi \) by replacing each literal \(R\bar{z}\) with the FO formula \(\theta (R\bar{y})[\bar{z}/\bar{y}]\). Here, \([\bar{z}/\bar{y}]\) represents the simultaneous substitution of the variables in \(\bar{y}\) by the corresponding variables in \(\bar{z}\).

Example 2

Consider formula \(\varphi \) that specifies that the author of a paper p should never be assigned to provide a review for p:

$$ \varphi = \forall x,p.\lnot \textsf {assign}(x,p)\vee \lnot \textsf {auth}(x,p) $$

Applying the substitution \(\theta \) from Example 1 results in

$$ \theta (\varphi ) = \forall x,p.\lnot (A_2(x,p) \wedge \lnot \textsf {conf}(x,p)) \vee \lnot \textsf {auth}(x,p) $$

   \(\square \)

A FO transition system \(\mathcal {T}\) (over the given sets \({\mathcal {R}_{ state }}\) of predicates, \(\mathcal {A}\) of input predicates and \(\mathcal {C}\) of constant names) consists of a finite set of nodes V together with a finite set E of edges of the form \(e=(u,\theta ,v)\) where \(u,v\in V\) and \(\theta \) is a substitution of the predicates in \({\mathcal {R}_{ state }}\). W.l.o.g., we assume that each substitution \(\theta \) at some edge e always has occurrences of at most one input predicate, which we denote by \(A_e\). For a given universe \(\mathcal {U}\), a program state s attained at a program point is a FO structure for the predicates in \({\mathcal {R}_{ state }}\) and the constants in \(\mathcal {C}\) over the universe \(\mathcal {U}\). Let S denote the set of all program states. A configuration of \(\mathcal {T}\) is a pair \((v,s)\in V\times S\). A (finite) run \(\tau \) of \(\mathcal {T}\) starting in configuration \((v_0,s_0)\) and ending at node v in state s, i.e., in configuration (v, s) is a sequence of configurations \((v_i,s_i)\), \(i=0,\ldots ,n\) where \((v_n,s_n) = (v,s)\) and for all \(i=1,\ldots ,n\), there is some edge \(e_i=(v_{i-1},\theta _i,v_i)\in E\) such that for \(s_{i-1} =\langle I,\rho \rangle \), \(s_i=\langle I',\rho \rangle \) where for some interpretation \(R_{i}\) of the input predicate \(A_{e_i}\), and every valuation \(\rho _\mathcal {Y}\) of the formals, \(I',\rho \oplus \rho _\mathcal {Y}\models R\bar{y}\) iff \(I\oplus \{A_{e_i}\mapsto R_{i}\} ,\rho \oplus \rho _\mathcal {Y}\models \theta (R\bar{y})\). Assume that we are given an initial node \(v_0\in V\) together with an initial hypothesis \({\mathcal {H}}\), i.e., a FO formula (with predicates in \({\mathcal {R}_{ state }}\) and free variables only in \(\mathcal {C}\)) characterizing all possible initial states attained at \(v_0\).

Example 3

According to the specification in Eq. (1) for the example transition system in Fig. 1, the single initial state is a pair of state 0 and the FO structure which interprets the relations \(\textsf {auth},\textsf {assign},\textsf {report}\) and \(\textsf {discuss}\) with the empty relation.    \(\square \)

Input predicates may take fresh interpretations whenever the substitution of the corresponding edge is executed. This should be contrasted to state predicates whose interpretations stay the same if they are not explicitly updated by the transition system. The constant interpretation of such predicates instead may be constrained by suitable background theories as provided, e.g., via conjuncts of the initial hypothesis.

Assume that \(\varPsi \) assigns to each program point \(v\in V\), a FO formula \(\varPsi [v]\). Then \(\varPsi \) is a valid invariant (relative to the initial hypothesis \({\mathcal {H}}\)), if every run \(\tau \) of the system starting in a configuration \((v_0,s_0)\) with \(s_0\models {\mathcal {H}}\) and visiting some configuration (v, s), it holds that \(s\models \varPsi [v]\). \(\varPsi \) is inductive if

$$\begin{aligned} \varPsi [u]\rightarrow \theta (\varPsi [v]) \qquad \text {forall}\;(u,\theta ,v)\in E \end{aligned}$$
(3)

If \(\varPsi \) is inductive, then \(\varPsi \) is a valid whenever

$$\begin{aligned} {\mathcal {H}}\rightarrow \varPsi [v_0] \end{aligned}$$
(4)

Indeed, it is this observation which is used in the Ivy project to verify distributed algorithms such as the Paxos protocol, essentially, by manually providing the invariant \(\varPsi \) and verifying properties (3) and(4) via the theorem prover Z3 [8].

Not each valid invariant \(\varPsi \), though, is by itself inductive. If this is not yet the case, iterative strengthenings \(\varPsi ^{(h)}, h\ge 0,\) of \(\varPsi \) may be computed as follows:

(5)

For computing the next iterate in (5), universal SO quantification over the input predicate \(A_e\) is required in order to account for every input possibly occurring during a run at the given edge. As, e.g., noted in [25], \(s\models \varPsi ^{(h)}[u]\) iff every run of length at most h starting in (u, s), ends in some configuration \((u',s')\) with \(s'\models \varPsi [u']\). In particular, the assignment \(\varPsi \) is a valid invariant iff \({\mathcal {H}}\rightarrow \varPsi ^{(h)}[v_0]\) for all \(h\ge 0\). The iteration thus can be considered as computing the weakest pre-condition of the given invariant \(\varPsi \) – as opposed to the collecting semantics of the FO transition system, which corresponds to the set of all configurations reachable from the set of all initial configurations \((v_0,s),s\models {\mathcal {H}}\). Whenever the fixpoint iteration (5) terminates, we obtain the weakest strengthening of the given invariant \(\varPsi \) which is inductive. We have:

Lemma 1

Let \(\mathcal {T}\) be a FO transition system and let \(\varPsi \) an invariant. Assume that for some \(h\ge 0,\) \( \varPsi ^{(h)} = \varPsi ^{(h+1)} \) holds. Then \(\varPsi ^{(h)}\) is the weakest inductive invariant implying \(\varPsi \). Moreover, \(\varPsi \) is valid iff \({\mathcal {H}}\rightarrow \varPsi ^{(h)}[v_0]\).    \(\square \)

In general, the required SO quantifier elimination may not always be possible, i.e., there need not always exist an equivalent FO formula [1], and even if SO quantifier elimination is always possible, the fixpoint iteration need not terminate. Non-termination may already occur when all involved predicates either have no arguments or are monadic [25]. Termination as well as effective computability can be enforced by applying abstraction (see, e.g., [24] for a general discussion). Applying an abstraction \(\alpha \) amounts to computing a sufficient condition for the invariant \(\varPsi \) to hold. Technically, an abstraction maps each occurring formula \(\psi \) to a formula \(\alpha [\psi ]\) (hopefully of a simpler form) so that \(\alpha [\psi ]\rightarrow \psi \). Subsequently, we list three examples for such strengthenings.

Example 4

Abstraction of existentials.   In [19], formulas with universal SO quantifiers and universal as well as existential quantifiers are strengthened to formulas with universal quantifiers only. The idea is to replace an existentially quantified subformula \(\exists x.\varphi \) with a disjunction \(\bigvee _{y\in Y}\varphi [y/x]\) where Y is the subset of constants and those universally quantified variables in whose scope \(\varphi \) occurs. So, the formula \(\forall y_1,y_2.\exists x. R(x)\) is abstracted by \(\forall y_1,y_2.R(y_1)\vee R(y_2)\). This abstraction is particularly useful, since SO universal quantifiers can be eliminated from universally quantified formulas.

Abstraction of Universals.   Fixpoint iteration for universally quantified formulas still may not terminate due to an ever increasing number of quantified variables. The universally quantified variable x in an otherwise quantifier-free formula \(\psi \) in negation normal form can be removed by replacing each literal containing x with \(\textit{false}\). In this way, the formula \(\forall x.\;(Rx\vee \lnot Sy\vee Tz)\wedge (\lnot Rx\vee \lnot Ty)\) is strengthened to \((\lnot Sy\vee Tz)\wedge \lnot Ty\).

Abstraction of Conjunctions.   Assume that the quantifier-free formula \(\psi \) is a conjunction of clauses. Then \(\psi \) is implied by the single clause c consisting of all literals which all clauses in \(\psi \) have in common. The formula \((Rx\vee \lnot Sy\vee Tz)\wedge (Rx\vee Tz\vee \lnot Tx)\), e.g., can be strengthened to \(Rx\vee Tz\).    \(\square \)

In this paper, rather than focusing on using abstractions, we identify sufficient criteria when the concrete iteration (5) terminates without any further abstraction.

3 Stratification and Guardedness

Subsequently, we concentrate on initial conditions in the \(\exists ^*\forall ^*\) fragment and universal invariants, i.e., where the invariant \(\varPsi \) consists of universal FO formulas only. Already for this setting, non-termination of the inference algorithm may occur even without SO quantification when a single binary predicate is involved.

Example 5

Consider the FO transition system \(\mathcal {T}\) over a monadic state predicate R, a binary state predicate E and a constant element a. \(\mathcal {T}\) consists of a single state u with a single transition:

$$\begin{aligned} R(y)\;{:=}\;R(y)\vee \exists z.\ E(y,z)\wedge R(z) \end{aligned}$$

Consider the invariant \(\varPsi [u] = \lnot R(a)\). Then for \(h\ge 0\),

$$ \varPsi ^{(h)}[u] = \lnot R(a)\wedge \bigwedge _{k=1}^h \forall z_1,\ldots ,z_k.\,\lnot E(a,z_1)\vee \bigvee _{i=1}^{k-1}\lnot E(z_i,z_{i+1})\vee \lnot R(z_k) $$

The weakest inductive invariant thus represents the set of elements which are not reachable from a via the edge relation E. This property is not expressible in FO predicate logic. Accordingly, \(\varPsi ^{(h)}[u]\ne \varPsi ^{(h+1)}[u]\) must hold for all \(h\ge 0\).    \(\square \)

Our goal is to identify useful non-trivial classes of FO transition systems where the fixpoint iteration is guaranteed to terminate. One ingredient for this definition is a stratification mapping \(\lambda :{\mathcal {R}_{ state }}\rightarrow \mathbb {N}\) which assigns to each state predicate R a level \(\lambda (R)\). Intuitively, this mapping is intended to describe how the information flows between predicates. Thereby, we use the convention that \(\lambda (R) = 0\) only for predicates R which are never substituted, i.e., whose values stay the same throughout each run of the transition system.

We will consider substitutions which are guarded and stratified. A substitution \(\theta \) is called guarded if it modifies at most one predicate \(R \in {\mathcal {R}_{ state }}\) at a time and is of one of the following forms:

$$\begin{aligned} {Update:\qquad \qquad } R\bar{y}&{:=}&R\bar{y}\vee \varphi \vee \exists \bar{z}.\,A\bar{y}\bar{z}\wedge \psi \end{aligned}$$
(6)
$$\begin{aligned} {Reset:\qquad \qquad } R\bar{y}&{:=}&\varphi \vee \exists \bar{z}.\,A\bar{y}\bar{z}\wedge \psi \end{aligned}$$
(7)

where \(A \in {\mathcal {R}_{ input }}\) is an input predicate and \(\varphi ,\psi \) are quantifier-free FO formulas without occurrences of predicate A. If additionally, each predicate \(R'\) occurring in \(\varphi \) or \(\psi \) has level less than \(\lambda (R)\), then \(\theta \) is called stratified.

According to our definition, a guarded substitution only updates a single predicate R. We might wonder whether the single update restriction could be lifted by additionally allowing simultaneous updates of several predicates which are coupled via the same input predicate. For this extension, however, termination can no longer be guaranteed.

Lemma 2

There exists a FO transition system \(\mathcal {T}\) using stratified simultaneous guarded updates and resets, together with some universal invariant \(\varPsi \) such that for each \(h\ge 0\), \(\varPsi ^{(h)}\) is universal FO definable, but \(\varPsi ^{(h)}[u] \not \rightarrow \varPsi ^{(h+1)}[u]\) for some program point u.

Proof

Consider the FO transition system \(\mathcal {T}\) as shown in Fig. 2 for some binary predicate E, together with the invariant \(\varPsi =\{1\mapsto \textsf {error}\vee \lnot \textsf {hull}(a,b), 0,2\mapsto \top \}\) for constants a, b. Initially, the predicate \(\textsf {hull}\) is set to \(\bot \). By executing the loop h times, either the error flag \(\textsf {error}\) is set to \(\top \), or \(\textsf {hull}\) receives kfold compositions of E for \(k=0,\ldots ,h\). Still, we can assign levels to the predicates used by \(\mathcal {T}\) which meet the requirements of a stratification:

$$ \lambda = \{ E \mapsto 0, \textsf {add}\mapsto 0, \textsf {hull}\mapsto 1, \textsf {error}\mapsto 2 \} $$

For \(h \ge 0\), we obtain \(\varPsi ^{(h)}[1] = \)

$$\begin{aligned}&\bigwedge _{j=1}^h \forall y_1\ldots y_j.\ \textsf {error}\vee \lnot \textsf {hull}(a,b) \vee \lnot \textsf {hull}(a,y_1) \vee \bigvee _{i=1}^{j-1}\lnot E(y_i,y_{i+1}) \vee \lnot E(y_j,b) \end{aligned}$$

For the required SO quantifier elimination of \(A_1,A_2\), we note that in order to avoid \(\textsf {error}\) to be set to \(\top \), \(\textsf {add}(x,y,z)\) must imply \(\textsf {hull}(x,y)\wedge E(y,z)\). In order to falsify the invariant at program point 1 whenever possible, thus, \(A_1(x,y,z)\) should be set to \(\textsf {hull}(x,y)\wedge E(y,z)\), and \(A_2(x,z,y)\) at least to \(\textsf {add}(x,y,z)\). Altogether thus, the weakest inductive invariant for program point 0 is given by \(\textsf {error}\vee \lnot E^*(a,b)\) where \(E^*\) is the transitive closure of E. As transitive closure is not FO definable, we conclude that the fixpoint iteration cannot terminate.    \(\square \)

Fig. 2.
figure 2

FO transition system capturing transitive closure.

Full size image

At the expense of slightly more complicated formulas for \(\varPsi ^{(h)}\), the right-hand side for \(\textsf {add}\) could be brought into the form (6). Thus, the crucial issue which results in inexpressible weakest inductive invariants, is the use of the same input predicate in two simultaneous updates. In the next section, we indicate how to generally deal with SO quantifiers, once a guarded substitution has been applied.

4 Universal So Quantifier Elimination

It is well-known that universal SO quantifiers can be removed from otherwise quantifier-free formulas [12, 19]. For example,

$$ \forall A.\,R\bar{x}\vee A\bar{y}\vee \lnot A\bar{z}\quad \longleftrightarrow \quad R\bar{x}\vee (\bar{y}=\bar{z}) $$

where for \(\bar{y}=(y_1,\ldots ,y_k)\) and \(\bar{z}=(z_1,\ldots ,z_k)\), \(\bar{y}=\bar{z}\) is a shortcut for the formula \((y_1=z_1)\wedge \ldots \wedge (y_k=z_k)\). Interestingly, there are also cases where SO quantifier elimination is possible even in presence of FO existential quantifiers.

Example 6

Consider the substitution \(\theta \)

$$ R(y)\;{:=}\;R(y) \vee \exists z.\, A(y,z)\wedge S(y,z) $$

In that case, \(\theta (R(a)\vee \lnot R(b))\) is given by

figure a

A closer inspection reveals that in this case, SO quantifier elimination of A is possible where \(\forall A.\,\theta (R(a)\vee \lnot R(b))\) is equivalent to

In particular, the resulting FO formula has universal FO quantifiers only.    \(\square \)

The observation in Example 6 can be generalized.

Lemma 3

  1. 1.

    If \(\varPsi \) is of the form

    $$\begin{aligned} \bigvee _{i=1}^n\ (\exists \bar{z}.\,A\bar{y}_i\bar{z}\wedge \varphi [\bar{y}_i/\bar{y}]) \vee \bigvee _{j=1}^m\ (\forall \bar{z}.\lnot A \bar{y}'_j\bar{z}\vee \lnot \varphi [\bar{y}'_j/\bar{y}]) \end{aligned}$$
    (8)

    for \(n,m \in \mathbb {N}\) where \(\varphi \) is a FO formula without occurrences of A. Then \(\forall A.\;\varPsi \) is equivalent to

    $$\begin{aligned} \bigvee _{j=1}^m (\bigvee _{i=1}^n \bar{y}_i = \bar{y}'_{j})\vee (\forall \bar{z}.\lnot \varphi [\bar{y}'_j/\bar{y}]) \end{aligned}$$
    (9)
  2. 2.

    If \(\varPsi \) is of the form

    $$\begin{aligned} \varphi '\vee \bigvee _{i=1}^n\ (\exists \bar{z}.\,A\bar{y}_i\bar{z}\wedge \varphi [\bar{y}_i/\bar{y}]) \vee \bigvee _{j=1}^m\ (\forall \bar{z}.\lnot A \bar{y}'_j\bar{z}\vee \lnot \varphi [\bar{y}'_j/\bar{y}])\wedge \psi '_j \end{aligned}$$
    (10)

    for \(n,m \in \mathbb {N}\) where \(\varphi ,\varphi ',\psi '_j\) all are FO formulas without occurrences of A. Then \(\forall A.\;\varPsi \) is equivalent to

    $$\begin{aligned} \varphi '\vee \bigvee _{j=1}^m (\bigvee _{i=1}^n (\bar{y}_i = \bar{y}'_{j})\vee (\forall \bar{z}.\lnot \varphi [\bar{y}'_j/\bar{y}])\wedge \psi '_j \end{aligned}$$
    (11)

Proof

For proving statement (1), we consider the negated formula \(\exists A.\lnot \varPsi \) and apply Ackermann’s lemma in order to remove existential SO quantification. We calculate:

figure b

where the last formula is equivalent to the negation of formula (9). The second statement then follows from statement (1) by distributivity.    \(\square \)

Interestingly, the same result is obtained when the existentially quantified variables \(\bar{z}\) do not occur as arguments to the input predicate A.

Lemma 4

  1. 1.

    If \(\varPsi \) is of the form

    $$\begin{aligned} \bigvee _{i=1}^n\ A\bar{y}_i\wedge (\exists \bar{z}.\,\varphi [\bar{y}_i/\bar{y}]) \vee \bigvee _{j=1}^m\ \lnot A \bar{y}'_j \vee (\forall \bar{z}.\lnot \varphi [\bar{y}'_j/\bar{y}]) \end{aligned}$$
    (12)

    for \(n,m \in \mathbb {N}\) where \(\varphi \) is a FO formula without occurrences of A. Then \(\forall A.\;\varPsi \) is equivalent to

    $$\begin{aligned} \bigvee _{j=1}^m (\bigvee _{i=1}^n \bar{y}_i = \bar{y}'_{j})\vee (\forall \bar{z}.\lnot \varphi [\bar{y}'_j/\bar{y}]) \end{aligned}$$
    (13)
  2. 2.

    If \(\varPsi \) is of the form

    $$\begin{aligned} \varphi '\vee \bigvee _{i=1}^n\ A\bar{y}_i\wedge (\exists \bar{z}.\,\varphi [\bar{y}_i/\bar{y}]) \vee \bigvee _{j=1}^m\ (\lnot A \bar{y}'_j \vee (\forall \bar{z}.\lnot \varphi [\bar{y}'_j/\bar{y}]))\wedge \psi '_j \end{aligned}$$
    (14)

    for \(n,m \in \mathbb {N}\) where \(\varphi ,\varphi ',\psi '_j\) all are FO formulas without occurrences of A. Then \(\forall A.\;\varPsi \) is equivalent to

    $$\begin{aligned} \varphi '\vee \bigvee _{j=1}^m (\bigvee _{i=1}^n (\bar{y}_i = \bar{y}'_{j})\vee (\forall \bar{z}.\lnot \varphi [\bar{y}'_j/\bar{y}])\wedge \psi '_j \end{aligned}$$
    (15)

Proof

For proving statement (1), we again consider the negated formula \(\exists A.\lnot \varPsi \) and apply Ackermann’s lemma in order to remove existential SO quantification. By introducing the shortcut \(\varPhi \) for \(\exists \bar{z}.\,\varphi \), we calculate:

figure c

where the last formula is equivalent to the negation of formula (13). Again, the second statement then follows from statement (1) by distributivity.    \(\square \)

In light of Lemmas 3 and 4, we introduce simplified versions of guarded updates and resets where the input predicate no longer occurs in the scope of existential quantifiers:

$$\begin{aligned} \textit{Simplified Update:}\qquad R\bar{y}&{:=}&R\bar{y}\vee \varphi \vee A\bar{y}\wedge \exists \bar{z}.\ \psi \end{aligned}$$
(16)
$$\begin{aligned} \textit{Simplified Reset:}\qquad R\bar{y}&{:=}&\varphi \vee A\bar{y}\wedge \exists \bar{z}.\ \psi \end{aligned}$$
(17)

As a first corollary, we obtain:

Corollary 1

Assume that \(\theta \) is a guarded update of the form (6) (guarded reset of the form (7)), and that \(\theta '\) is the corresponding simplified update (16) (simplified reset (17)). Then for every universal FO formula \(\varPsi \),

$$\forall A.\ \theta (\varPsi ) \quad \longleftrightarrow \quad \forall A.\ \theta '(\varPsi ) $$

   \(\square \)

In light of Corollary 1, we subsequently consider FO transition systems with simplified guarded updates and resets only.

Example 7

Consider the second update in the loop of the transition system from Fig. 1. Its simplified variant removes \(r_1\) and \(r_2\) from the signature of \(A_4\):

Let \(\theta _4\) denote this simplified update, and consider the invariant (2) from the introduction. Application of \(\theta _4\) results in the formula

$$ \begin{array}{l} \forall x_1,x_2,p,d,r_1,r_2. \lnot \textsf {discuss}(x_1,x_2,p,d)\;\wedge \\ \qquad (\lnot A_4(x_1,x_2,p,d)\vee \lnot \textsf {report}(x_1,p,r_1)\vee \lnot \textsf {report}(x_2,p,r_2))\;\vee \\ \qquad (\lnot \textsf {auth}(x_1,p)\wedge \lnot \textsf {auth}(x_2,p)) \end{array} $$

Since \(A_4\) only occurs negatively, universal SO quantifier elimination of \(A_4\) yields

$$ \begin{array}{l} \forall x_1,x_2,p,d,r_1,r_2. \lnot \textsf {discuss}(x_1,x_2,p,d)\wedge \; \\ \qquad (\lnot \textsf {report}(x_1,p,r_1)\vee \lnot \textsf {report}(x_2,p,r_2))\;\vee \\ \qquad (\lnot \textsf {auth}(x_1,p)\wedge \lnot \textsf {auth}(x_2,p)) \end{array} $$

   \(\square \)

Corollary 2

Assume \(\varPsi \) is a formula of the form (14). Then \(\forall A.\,\varPsi \longleftrightarrow \theta (\varPsi )\) where \(\theta \) is given by

$$\begin{aligned} A\bar{y}\;{:=}\;\bigwedge _{i=1}^n(\bar{y}_i\ne \bar{y}) \end{aligned}$$
(18)

The definition (18) thus provides us with the worst adversarial strategy to defeat the proposed invariant. As another consequence of Lemma 3, we find that in presence of subsequent SO quantifier elimination, the effect of a guarded substitution of the forms (16) or (17) could also be simulated by the corresponding nonuniform substitutions:

$$\begin{aligned} R\bar{y}&{:=}&R\bar{y}\vee \varphi \vee A\bar{y}\nonumber \\ \lnot R\bar{y}&{:=}&\lnot R\bar{y}\wedge \lnot \varphi \wedge (\lnot A\bar{y}\vee \forall \bar{z}.\lnot \psi ) \end{aligned}$$
(19)
$$\begin{aligned}&\text {and}&\nonumber \\ R\bar{y}&{:=}&\varphi \vee A\bar{y}\nonumber \\ \lnot R\bar{y}&{:=}&\lnot \varphi \wedge (\lnot A\bar{y}\vee \forall \bar{z}.\lnot \psi ) \end{aligned}$$
(20)

respectively. Here, nonuniform means that positive and negative occurrences of literals are substituted differently. We have:

Corollary 3

Assume that \(\theta \) is a guarded substitution of the form (16) or (17). Assume that \(\theta '\) is the nonuniform substitution of the corresponding form (19) or (20), respectively. Then for every universal formula \(\varPsi \),

$$ \forall A.\,\theta (\varPsi ) \quad \longleftrightarrow \quad \forall A.\,\theta '(\varPsi ) $$

   \(\square \)

Finally, as another important consequence of Lemma 3, we obtain:

Theorem 1

Assume that \(\mathcal {T}\) is a FO transition system with guarded (simplified) updates and resets only, and \(\varPsi \) a universal FO invariant.

  1. 1.

    The iterates \(\varPsi ^{(h)}[u],h\ge 0\), in (5) all are effectively equivalent to universal FO formulas.

  2. 2.

    The iteration terminates, i.e., \(\varPsi ^{(h)} = \varPsi ^{(h+1)}\) for some \(h\ge 0\), iff for each program point u, the weakest strengthening of all iterates \(\varPsi ^{(h)}[u]\) is FO-definable.

Proof

Due to Lemmas 3 and 4, for each universal FO formula \(\varphi \) and each guarded (simplified) update or reset \(\theta \) with input predicate A, \(\forall A.\,(\theta \varphi )\) is equivalent to a universal FO formula. That implies statement (1). Now assume for for each \(h\ge 0\) and each \(v\in V\), \(\varPhi ^{(h)}[v]\) is FO definable. Then due to the compactness theorem for FO predicate logic [5], there is some \(h\ge 0\) such that \(\varPsi ^{(h)}[v] \leftrightarrow \varPsi ^{(h+j)}[v]\) holds for all \(v\in V\) and \(j\ge 0\), iff for each \(v\in V\), the conjunction \(\bigwedge _{h\ge 0} \varPsi ^{(h)}[v]\) is again FO definable.    \(\square \)

Example 8

Consider again the specification from Fig. 1, and let \(\theta _1,\theta _2,\theta _3,\) and \(\theta _4\) denote the simplified substitutions occurring therein. Assume that \(\varPsi \) equals the universal formula in (2), and we are interested in its validity at program point 2 of the transition system. The formula \(\forall A_3.\,\theta _3(\forall A_4.\,\theta _4(\varPsi ))\) is given by

$$ \begin{array}{ll} &{}\forall A_3.\,\theta _3( \forall x_1,x_2,p,d,r_1,r_2.\lnot \textsf {discuss}(x_1,x_2,p,d)\;\wedge \\ &{}\qquad ( \lnot \textsf {report}(x_1,p,r_1)\vee \lnot \textsf {report}(x_2,p,r_2))\vee (\lnot \textsf {auth}(x_1,p)\wedge \lnot \textsf {auth}(x_2,p)) \\ \longleftrightarrow &{} \forall x_1,x_2,p,d,r_1,r_2.\lnot \textsf {discuss}(x_1,x_2,p,d)\;\wedge \\ &{} \qquad ( \lnot \textsf {report}(x_1,p,r_1)\wedge \lnot \textsf {assign}(x_1,p)\vee \lnot \textsf {report}(x_2,p,r_2)\wedge \lnot \textsf {assign}(x_2,p))\;\vee \\ &{} \qquad (\lnot \textsf {auth}(x_1,p)\wedge \lnot \textsf {auth}(x_2,p)) \end{array} $$

The resulting formula \(\varPsi '\) already equals the fixpoint for the loop. Since the predicate \(\textsf {assign}\) only occurs negatively in \(\varPsi '\) and \(\textsf {conf}\) only negatively in the right-hand side for \(\textsf {assign}\), the formula \(\forall A_1.\theta _1(\forall A_2.\theta _2(\varPhi '))\) construction from \(\varPsi '\) via the substitution \(\theta _\textsf {assign}\) defined by

$$ \textsf {assign}(y_1,y_2)\;{:=}\;\lnot \textsf {auth}(y_1,y_2) $$

This means the formula \(\varPsi ''\) for the initial node of the transition system is given by

$$ \begin{array}{l} \forall x_1,x_2,p,d,r_1,r_2.\lnot \textsf {discuss}(x_1,x_2,p,d)\;\wedge \\ \qquad ( \lnot \textsf {report}(x_1,p,r_1)\wedge \textsf {auth}(x_1,p)\vee \lnot \textsf {report}(x_2,p,r_2)\wedge \textsf {auth}(x_2,p))\;\vee \\ \qquad (\lnot \textsf {auth}(x_1,p)\wedge \lnot \textsf {auth}(x_2,p)) \end{array} $$

By the initial condition \({\mathcal {H}}\) from the introduction, \(\lnot \textsf {discuss}(x_1,x_2,p,d)\) holds at the initial node of the transition system, as well as \(\lnot \textsf {report}(x_1,p,r_1)\) and \(\lnot \textsf {report}(x_2,p,r_2)\) for all \(x_1,x_2,p,d,r_1,r_2\). Therefore, \({\mathcal {H}}\) implies \(\varPsi ''\), and the property \(\varPsi \) at the exit of the transition system is valid.    \(\square \)

In this section we have shown comprehensively how to eliminate universal SO quantifiers introduced by guarded updates in a FO transition system and introduced a non-uniform variant of any guarded updates and resets which removes all possibly introduced existential FO quantifiers. In the next two sections, we will apply these results to FO transition systems which additionally are stratified.

5 Stratified Guarded Updates

In [19], termination was announced for FO transition systems with stratified guarded updates where instantiation of existential quantifiers was applied as an abstraction to enforce all occurring formulas to be universal. Here, we improve on that result in two respects. First, we present a proof that termination can also be guaranteed without any abstraction. Second, we generalize the setting to allow stratified guarded resets—at least at the maximal and minimal levels.

Theorem 2

Assume that \(\mathcal {T}\) is a FO transition system where each occurring substitution is stratified guarded with the restriction that resets only occur for predicates of level 1 and the maximal level L. Then for every universal invariant \(\varPsi \), the weakest inductive invariant is again universal and can effectively be computed.

Proof

W.l.o.g., we assume that each occurring substitution is a simplified update or reset, i.e., either of the form (16) or (17). We show that there is some \(h\ge 0\), so that \(\varPsi ^{(h+1)} = \varPsi ^{(h)}\). Since by Lemma 4, \(\varPsi ^{(h)}[u]\) is a universal formula for all \(h\ge 0\) and program points u, the statement of the theorem follows.

Assume that each simplified update \(\theta \) of a predicate R always is specified by means of the same input predicate \(A_R\). Let \(\varTheta \) denote the finite set of stratified guarded substitutions occurring in \(\mathcal {T}\), and \(\varPhi \) a universal FO formula. Let \(\pi = \theta _N,\ldots ,\theta _1\) be any sequence of nonuniform substitutions where for each \(i = 1,\ldots ,N\), \(\theta _i = \theta '_i[A_i/A_{R}]\) holds for a fresh input predicate \(A_i\), and a nonuniform substitution \(\theta '_i\) of the form (19) corresponding to a simplified update or reset \(\theta ''\in \varTheta \) with left-hand side \(R\bar{y}\).

Lemma 5

There is some number V only depending on \(\varPhi \) and \(\varTheta \) so that \(\pi (\varPhi ) = \theta _N(\ldots \theta _1(\varPhi )\ldots ) = \bigwedge _{h=t}^N (\forall \bar{z}_t.c_t)\) for clauses \(c_t\) where the number of FO variables in \(\bar{z}_t\) is bounded by V. In particular, V is independent of the number N of substitutions in \(\pi \).

Given Lemma 5, the number of argument tuples \(\bar{z}\) of occurring literals \(A_i\bar{z}\) in any \(c_t\) is bounded. Due to Corollary 2, a bounded number of substitutions of the form (18) therefore suffices to realize SO quantifier elimination of \(A_1,\ldots ,A_N\) in \(c_t\). As a consequence, the number of universal FO formulas possibly occurring in each conjunct of \(\forall A_1\ldots A_N.\,\pi (\varPhi )\), and thus also the number of conjunctions of these formulas is finite. Accordingly, there must be some \(h\ge 0\) so that \(\varPhi ^{(h+1)} = \varPhi ^{(h)}\), and the theorem follows. It therefore remains to prove Lemma 5.

Proof

(of Lemma 5). Let us first consider the case where there is no reset of predicates at maximal level L. We introduce a dedicated class of formulas g as finite conjunctions of generalized clauses c which are built up according to the following abstract grammar

where \(c_0\) is an ordinary clause without occurrences of input predicates, R is a predicate, \(A,A_n\) are input predicates, \(\bar{a},\bar{b}\) are sequences of arguments, \(\bar{z}_R\) is a sequence of fresh variables whose length only depends on R, and formulas \(o_{\bar{b}}\) where all state predicates are of level 0. A formula \(f_{R\bar{b}}\) is also called negation tree with head \(\lnot R\bar{b}\), while we call a formula \(o_{\bar{b}}\) a level 0 chunk. Moreover,

  1. (a)

    All literals occurring in the generalized clauses \(c_n\) inside the conjunction within \(f_{R\bar{b}}\) are of levels less than \(\lambda (R)\);

  2. (b)

    For any two negation trees \(\varphi _1,\varphi _2\) with identical head \(\lnot R\bar{b}\), there is some formula \(\varDelta \) so that either \(\varphi _1=\varphi _2\wedge \varDelta \) or vice versa, \(\varphi _2=\varphi _1\wedge \varDelta \) holds.

\(\varPhi \) can be brought into the form \(\forall \bar{z}.\,\bigwedge _{t=1}^m c_t\) where each \(c_t\) is an ordinary clause without occurrences of input predicates, i.e., a plain disjunction of literals and (dis-)equalities. Therefore, now consider a single generalized clause c which satisfies properties (a) and (b). We show that for each nonuniform update substitution \(\theta \) of the form

\(\theta (c)\) can again be represented as a conjunction of generalized clauses satisfying properties (a) and (b), and whose free variables are all contained in the set of free variables from c and \(\theta \). Assume that c is of the form \( c'\vee \bigvee _{i=1}^sR\bar{a}_i\vee \bigvee _{j=1}^t f_{R\bar{b}_j} \) where \(c'\) is a generalized clause without further top-level occurrences either of positive literals \(R\bar{a}'\) or negation trees with head \(\lnot R\bar{b}'\) for any \(\bar{a}',\bar{b}'\), and \(f_{R\bar{b}_j} = \lnot R\bar{b}_j\wedge \forall \bar{z}_R.\, \bigwedge _{\nu =1}^{u_j}(\lnot A_{j,\nu }\bar{b}_j\vee c_{j,\nu })\) is a negation tree with head \(\lnot R\bar{b}_j\). Then

where \(\mathcal C\) and \(\bar{\mathcal{C}}\) are the sets of clauses in the normal forms of \(\varphi \) and \(\lnot \varphi \), respectively. The resulting formula can indeed be represented as a conjunction of generalized clauses satisfying property (a). Concerning property (b), we observe that for every fresh negative literal property (b) trivially holds, while for existing negation trees, this property is preserved. If on the other hand, \(\theta \) is a reset of a predicate at level 1, \(\theta (c)\) is a conjunction of generalized clauses where some negation trees have been replaced by level 0 chunks. In particular, properties (a) and (b) still hold.

Assume now that we are given a generalized clause c satisfying properties (a) and (b). Then c is called flat up to level i, if the roots of all negation trees occurring in c with a nonempty conjunction, have level at most i, and for every predicate R of level i and every possible argument tuple \(\bar{b}\), there is at most one negation tree with head \(\lnot R\bar{b}\). For a generalized clause c which is flat up to level i, we define the transformation \(\textsf {flatten}_i\) as follows. Assume that c is of the form

$$ c'\vee \bigvee _{j=1}^t \lnot R_j\bar{b}_j\wedge \forall \bar{z}_j.\bigwedge _{\nu =1}^{u_j} (\lnot A_{j,\nu }\bar{b}_j\vee c_{j,\nu }) $$

where the \(\lnot R_j\bar{b}_j\) represent all occurrences of negated literals of level i. Then

In each quantified clause \(\forall \bar{z}_{j_1}\ldots \bar{z}_{j_k}.\,c'\) in the conjunction, all occurring negation trees have level less than i. Now due to property (2), \(c'\) can be simplified so that for each negated literal \(R'\bar{b}\) where \(R'\) is of level \(i-1\), there is at most one negation tree. The resulting conjunction of quantified clauses is denoted by \(\textsf {flatten}_i\,c\).

To compute a bound on the number of possible argument variables, let us introduce the following structural parameters:

figure d

Successive application of \(\textsf {flatten}_L,\ldots ,\textsf {flatten}_1\) allows us to construct for a generalized clause c satisfying properties (a) and (b), an equivalent conjunction of formulas \(\forall \bar{z}'.\,c'\) where \(c'\) is disjunction of literals, (dis-)equalities and level 0 chunks \(o_{\bar{b}}\) only, and \(\bar{z}'\) is the list of globally bound variables occurring freely in \(c'\).

For \(i=L,\ldots ,1\), we inductively determine a bound \(V_i\) to the number of distinct FO variables possibly occurring as arguments of literals at level i in a clause \(c'\). For \(i=L\), we can set \(V_L = v\), since the only literals at level L occurring in \(c'\) already must have occurred in \(\varPhi \). Therefore, assume that \(i < L\) and a bound \(V_{i+1}\) has already been found. Then \(V_i\) can be bound as follows: Given the number \(V_{i+1}\), the number of literals of predicates at level \(i+1\) can be bound by \(m\cdot V_{i+1}^r\). For each of these literals, a fresh list of variables of length at most l can be provided. Accordingly,

$$ V_i = V_{i+1}+l\cdot m\cdot V_{i+1}^r \le (1+l\cdot m)\cdot V_{i+1}^r $$

Altogether, this means that the total number of variables possibly occurring in literals of \(c'\) (outside of level 0 chunks) at level at least 0 is bounded by

$$\begin{aligned} V\le \left\{ \begin{array}{ll} (1+l\cdot m)^{L}\cdot v &{}\text {if}\;r=1 \\ \left( 1+ l\cdot m \right) ^{\frac{r^{L}-1}{r-1}}\cdot v^{r^{L}} &{}\text {if}\;r>1 \end{array}\right. \end{aligned}$$
(21)

Now given that there is a bound \(V_1\) to the number of variables possibly occurring as arguments of predicates at level 1, there is also only a bounded number O of non-equivalent subformulas \(o_{\bar{b}}\) (after SO quantifier elimination) in any of the generalized clauses from \(\textsf {flatten}_1(\ldots \textsf {flatten}_L(c')\ldots )\). Accordingly, \(V_0+O\cdot l\) bounds the number of variables occurring in equalities, disequalities and literals of predicates at level 0.

Let us finally also consider the case when additionally resets of predicates at maximal level L occur. Such a reset for a predicate R takes effect at most once. It thus introduces one fresh list of universally quantified variables for each occurrence \(\lnot R\bar{b}\) of the negated the negated literal at most once where we w.l.o.g. may even assume that the list of outside universal quantifiers of the negation tree for that literal can be reused. Thus, no further universal quantifiers are introduced. Altogether, therefore, the number of FO variables in quantified clauses \(\forall \bar{z}'.c'\) contained in \(\pi (\varPhi )\) remains bounded. This completes the proof of Lemma 5.    \(\square \)

We remark that Theorem 2 remains true if there are predicates \(R'\) with stratified guarded updates as well as resets also at non-extremal levels—given that neither their updates nor their resets introduce FO variables, i.e., the variable lists \(\bar{z}\) in (6) and (7) ((16) and (17)) are empty. In general, though, the proof technique of Theorem 2 cannot easily be extended to FO transition systems with arbitrary resets of the form (7), since then conjunctions of the form \(o_{\bar{b}}\) with non-empty lists of quantified variables may also occur at higher levels—where it is no longer clear how to prove that their number is finite.

6 Allowing Guarded Stratified Resets

We would like to extend Theorem 2 from the last section to FO transition systems which additionally have resets at arbitrary levels. We succeed in doing so in two special cases (see Theorems 3 and 4, respectively). Let us call an update strictly guarded it it is of the form:

$$\begin{aligned} R\bar{y}&{:=}&R\bar{y}\vee A\bar{y}\wedge \exists \bar{z}.\,\psi \end{aligned}$$
(22)

for some predicate R and quantifier-free FO formula \(\psi \) without occurrences of A. Furthermore, let us call an update or reset \(\theta \) positive if all predicates only occur positively in the right-hand side.

Theorem 3

Consider a FO transition system \(\mathcal {T}\) where all substitutions are stratified, guarded, and all substitutions of predicates not of level 0 are positive. Then for every universal invariant \(\varPsi \), the weakest inductive invariant is again universal and can effectively be computed.

Proof

Let \(\varTheta \) denote the set of substitutions occurring in \(\mathcal {T}\). As in the proof of Theorem 2, let \(\pi = \theta _N,\ldots ,\theta _1\) be any sequence of nonuniform substitutions where for each \(i = 1,\ldots ,N\), \(\theta _i = \theta '_i[A_i/A_{R}]\) holds for a fresh input predicate \(A_i\), and a nonuniform substitution \(\theta '_i\) of the form (19) corresponding to an update or reset substitution \(\theta ''\in \varTheta \) with left-hand side \(R\bar{y}\). Let \(\bigwedge _{j=1}^M (\forall \bar{z}_j.\,c_j)\) denote the conjunction of quantified generalized clauses for \(\pi (\varPhi )\)—now possibly also with sub-formulas \(o_{\bar{b}}\) holding predicates of level \(> 0\). Then each FO variable x occurring in a positive literal \(A_i\bar{a}\) in any \(c_j\), already occurs in \(\varPhi \). In light of Corollary 2, it therefore suffices to use only a globally bounded number of input predicates in each \(c_j\). If the number of predicate symbols is bounded, then also the number of generalized clauses as well as the number of non-equivalent formulas \(\forall A_1\ldots A_N.\,\pi (\varPhi )\)—implying that for every universal invariant \(\varPsi \), \(\varPsi ^{(h+1)} = \varPsi ^{(h)}\) for some \(h\ge 0\). From that, the statement of the theorem follows.    \(\square \)

The proof argument for Theorem 3 cannot easily be extended to unrestricted stratified guarded substitutions. In presence of negated literals in substitutions, it is no longer the case that the arguments of positive literals \(R\bar{a}\) occurring in \(\pi (\varPhi )\) have already occurred in \(\varPhi \), so for the next result we have to rely on a different proof strategy.

Theorem 4

Consider a FO transition system \(\mathcal {T}\) where all substitutions are guarded and stratified. Assume furthermore that all updates are strictly guarded. Then for every universal invariant \(\varPsi \), the weakest inductive invariant is again universal and can effectively be computed.

Proof

For this proof, it is convenient to use the notation \(\varPhi \ni \forall \bar{x}.\,c\) for a universal FO formula \(\varPhi \), a clause c, and a list \(\bar{x}\) of distinct variables so that for the prenex CNF \(\forall \bar{z}.\,c_1\wedge \ldots \wedge c_m\) of \(\varPhi \), c occurs among the \(c_j\), and \(\bar{x}\) is the subsequence of variables in \(\bar{z}\) which occur in c. We rely on the following technical lemma:

Lemma 6

Assume that c is a clause and \(\theta \) a stratified reset or stratified strictly guarded update with input predicate A which substitutes a predicate R with \(\lambda (R)=s\). Let \(c'\) be a clause with \(\forall A.\,\theta (c)\ni \forall \bar{x}.\,c'\) where \(\bar{x}\) is the list of newly introduced variables in \(c'\). Then either \(c=c'\) and \(\bar{x}\) is empty, or the number of literals at level s of \(c'\) is less than the corresponding number of c.

Proof

Assume that the clause c is of the form

$$ c_0\vee R\bar{y}_1\vee \ldots \vee R\bar{y}_n\vee \lnot R\bar{y}'_1\vee \dots \vee \lnot R\bar{y}'_m $$

where \(c_0\) does not contain the predicate R. If \(\theta \) is a reset, all literals containing R are eliminated. Therefore, the assertion of the lemma trivially holds. Now assume that \(\theta \) is a strictly guarded update, i.e., of the form (22). Then by Lemma 3,

where \(\bar{z}_j\) is a fresh list of FO variables of the same length as \(\bar{z}\), and \(\bar{z}_J\) is the concatenation of all lists \(\bar{z}_j,j\in J\). In particular for \(J=\emptyset \), \(\bar{z}_J\) is empty and the corresponding clause equals c. If on the other hand \(J\ne \emptyset \), the number of negated literals occurring in the clause has decreased.    \(\square \)

By Lemma 6, the number of literals at level s therefore either decreases, or the clause stays the same. Let \(\varTheta \) denote a finite set of stratified guarded substitutions where all updates in \(\varTheta \) are strictly guarded, and let \(c_0\) denote any clause. Consider a sequence \((\theta _t,\forall \bar{x}_t.c_t), t\ge 1\), where for all \(t\ge 1\), \(\theta _t\in \varTheta \) with some input predicate \(A_t\), and \(\forall A_t.\,(\theta _t c_{t-1})\ni \forall \bar{x}_t.\,c_t\) holds. We claim that then there is some \(t'\ge 1\) so that \(c_{t'} = c_{t''}\) and \(\bar{x}_{t''}\) is empty for all \(t''>t'\).

In order to prove that claim, we introduce for \(t\ge 1\), the vector \(v_t = (v_{t,L},\ldots ,v_{t,1})\in \mathbb {N}^L\) where L is the maximal level of a predicate in \({\mathcal {R}_{ state }}\), and \(v_{t,i}\) is the number of literals with predicates of level i. By Lemma 6, it holds for all \(t\ge 0\), that either \(c_t = c_{t+1}\) and \(\bar{z}_t\) is empty, or \(v_t > v_{t+1}\) w.r.t. the lexicographic order on \(\mathbb {N}^L\). Since the lexicographical ordering on \(\mathbb {N}^L\) is well-founded, the claim follows. We conclude that the set of quantified clauses \(\forall \bar{z}.c\) with \(\varPsi ^{(h)}[u]\ni \forall \bar{z}.c\) for any u and h, is finite. From that, the statement of the theorem follows.    \(\square \)

Theorem 4 leaves open the case of transition systems with stratified guarded resets and stratified guarded updates of which some are not strictly guarded. To these, the presented proof technique cannot be easily extended. The reason is that a non-strictly guarded update \(\theta \) for some predicate R, when applied to some clause c, may result in a quantified clause \(\forall \bar{z}.\,c'\) with \(\forall A.\theta (c)\ni \forall \bar{z}.\,c'\) so that neither \(c=c'\) holds nor does the number of literals \(\lnot R\bar{b}\) decrease.

7 Conclusion

We have investigated FO transition systems where all substitutions are either guarded updates or guarded resets. For these, we observed that the exact weakest pre-condition of a universal FO formula is again a universal FO formula, thus allowing us to realize a fixpoint computation of iterated strengthening for proving the validity of universal invariants. In order to identify sub-classes of FO transition systems where termination can be guaranteed, we relied on a natural notion of stratification. Here, we were able to prove termination (and thus decidability) for three interesting sub-classes of stratified guarded FO transition systems. However, it remains as an open question whether termination can be proven for all FO transition systems with stratified guarded updates and resets.

The results of our paper can immediately be applied to the multi-agent workflow language as considered in [19] for analyzing noninterference in presence of declassification and agent coalitions. There, transformations are presented to encode noninterference properties as invariants of the self-composition of the given workflow [3, 17]. At least for the case of stubborn agents [11], i.e., agents who do not participate in adversarial coalitions, the given transformation preserves both guardedness and the stratification. The same also holds true if the size of adversarial coalitions is bounded. For these cases, our novel decidability results therefore translate into decidability of noninterence.