First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of occurring negated literals decreases in every iteration, or the number of required instances of input predicates or the number of first-order variables remains bounded. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed. We apply these results to identify classes of multi-agent systems, when formalized as first-order transition systems, where noninterference in presence of declassification is decidable for coalitions of attackers of bounded size.
Hinweise
Christian Müller and Helmut Seidl have contributed equally to this work.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
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 [1] 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
A conference management system
×
Assume that initially, all predicates with the exception of \(\textsf {auth}\) are false, i.e., the property \({{\mathcal {H}}}\) given by
holds. The predicates \(A_1,\ldots ,A_4\) are input predicates whose values either represent agents’ decisions or input from the environment. Intuitively, the transition system works as follows: First, each PC member x possibly declares her conflict with each paper p. Then the assignment relation of papers p to PC members x is extended 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 [2, 3].
Anzeige
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:
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) [4‐6]. Recently, it has successfully been applied for the specification and verification of software-defined networks [7, 8], of network protocols [9], of distributed algorithms [1]. The corresponding approach is built into the tool Ivy [9, 10]. 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 [11]. Some effort, though, has been invested to come up with more automatic techniques for specific settings such as threshold algorithms [12] or more general FO invariant inference [13, 14]. 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 [3, 15, 16] where noninterference [17] is investigated for multi-agent workflows in the spirit of the conference management system from Fig. 1. In [3], 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 [18], 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 [3] 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 [19]). The syntactic restrictions proposed in [3] essentially amount to introducing a stratification on the predicates and restricting substitutions to be stratified 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
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 \).
Anzeige
The loop of the example thus satisfies the requirements of [3], 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. Resets are seemingly easier than updates, as they define their left-hand sides solely in terms of predicates of lower levels without resorting to input predicates. 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 all updates are not only guarded, but strictly guarded; or
when all substitutions are single, and all predicates of level at least 1, occur in right-hand sides only positively; or
when resets refer to predicates at the highest and at the lowest level of the stratification only.
Data sharing is not applicable to this article as no new data were created or analyzed in this study. A preliminary version of this paper has appeared in [20]. There just single updates of predicates at a time have been considered — while simultaneous updates are crucial for the application to noninterference in multi-agent systems with declassification where agent capabilities are taken into account (NDA). A detailed study of that application makes up the second part of the paper. For this, we review the constructions for self-composition from [3] and present their adaptations to FO transition systems. Based on these constructions, we provide general classes of multi-agent systems, when formalized as FO transition systems, where NDA is in fact decidable. In this way, we strengthen the results from [3] in two ways: on the one hand, our systems are more general in that (some forms of) resets are additionally allowed; on the other, we obtain decidability of NDA where termination could only be proven for an abstraction of the system.
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 interpretationI 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 an assumption formula g and a substitution\(\theta \). The transition can only take place when the assumption formula g is satisfied. For each state predicate \(R\in {{\mathcal {R}}_{ state }}\), \(\theta \) then 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}}_R\) for the literal \(R(y_1,\ldots ,y_k)\) and assume that each substitution \(\theta \) maps each literal \(R{\bar{y}}_R\), \(R\in {{\mathcal {R}}_{ state }}\), to some FO formula \(\theta (R{\bar{y}}_R)\) 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_i{\bar{y}}_{R_i}) = \psi _i\) for \(i=1,\ldots ,r\), and \(\theta (R'{\bar{y}}_{R'}) = R'{\bar{y}}_{R'}\) for all \(R'\in {{\mathcal {R}}_{ state }}\setminus \{R_1,\ldots ,R_r\}\), we also denote \(\theta \) by
if \(r=1\). In this case, we call \(\theta \)single. Finally, the assumption formula g at edges is omitted if it equals \(\top \).
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 {A}}}\) consists of the predicates \(A_1\ldots A_4\). No constants are needed, so \({\mathcal {C}}= \emptyset \). The edge from node 1 to 2 has no assumption and specifies a single substitution \(\theta \) that updates \(\textsf {assign}\) with
while leaving literals of predicates \(\textsf {conf},\textsf {auth},\textsf {report}\) or \(\textsf {discuss}\) unchanged. \(\square \)
Applying the substitution \(\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}}_R)[{\bar{z}}/{\bar{y}}_R]\). Here, \([{\bar{z}}/{\bar{y}}_R]\) represents the simultaneous substitution of the variables in \({\bar{y}}_R\) by the corresponding variables in \({\bar{z}}\) (perhaps, with appropriate renaming of bound variables in the formula \(\theta (R{\bar{y}}_R)\)).
Example 2
Consider formula \(\varphi \) that specifies that the author of a paper p should never be assigned to provide a review for p:
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,(g;\theta ),v)\) where \(u,v\in V\), and g, \(\theta \) specify an assumption and substitution of the predicates in \({{\mathcal {R}}_{ state }}\), respectively. W.l.o.g., we assume that the assumption g and substitution \(\theta \) at each 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},(g_i;\theta _i),v_i)\in E\) such that for \(s_{i-1} =\langle I,\rho \rangle \) and some interpretation \(R_{i}\) of the input predicate \(A_{e_i}\), the following holds:
\(I\oplus \{A_{e_i}\mapsto R_{i}\} ,\rho \models g\), and
\(s_{i} =\langle I',\rho \rangle \) where for every state predicate R and valuation \(\rho _R\) of the formals \(y_i\) occurring in \({\bar{y}}_R\),
Here, the operator \(\oplus \) is meant to extend the assignment in the left argument with the assignment to the right.
Subsequently, we 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 (w.r.t. any given universe) is the pair of node 0 and the FO structure which interprets the relations \(\textsf {auth},\textsf {assign},\textsf {report}\) and \(\textsf {discuss}\) with empty relations each. \(\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. State predicates which are never updated, thus have constant interpretations. These still may be constrained by some background theory provided via conjuncts of the initial hypothesis.
Assume that \(\Psi \) assigns to each program point \(v\in V\), a FO formula \(\Psi [v]\). Then \(\Psi \) 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 \Psi [v]\). \(\Psi \) is inductive if
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 \(\Psi \) and verifying properties (3) and(4) via the theorem prover Z3 [11].
Not every valid invariant \(\Psi \), though, is by itself inductive. If this is not yet the case, iterative strengthenings\(\Psi ^{(h)}, h\ge 0,\) of \(\Psi \) may be computed as follows:
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 when executing the edge e. As, e.g., noted in [2], \(s\models \Psi ^{(h)}[u]\) iff every run of length at most h starting in (u, s), ends in some configuration \((u',s')\) with \(s'\models \Psi [u']\). In particular, the assignment \(\Psi \) is a valid invariant iff \({{\mathcal {H}}}\rightarrow \Psi ^{(h)}[v_0]\) for all \(h\ge 0\). The iteration thus can be considered as computing the weakest pre-condition of the given invariant \(\Psi \) – as opposed to the collecting semantics of the FO transition system, which corresponds to the set of all configurations reachable from the set of initial configurations \((v_0,s),s\models {{\mathcal {H}}}\). Whenever the fixpoint iteration (5) terminates, we obtain the weakest strengthening of the given invariant \(\Psi \) which is inductive. We have:
Lemma 1
Let \({\mathcal {T}}\) be a FO transition system and let \(\Psi \) an invariant. Assume that for some \(h\ge 0,\)\( \Psi ^{(h)} = \Psi ^{(h+1)} \) holds. Then \(\Psi ^{(h)}\) is the weakest inductive invariant implying \(\Psi \). Moreover, \(\Psi \) is valid iff \({{\mathcal {H}}}\rightarrow \Psi ^{(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 [21], 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 [2]. Termination as well as effective computability can be enforced by applying abstraction (see, e.g., [22] for a general discussion). Applying an abstraction \(\alpha \) amounts to computing a sufficient condition for the invariant \(\Psi \) 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
In [3], 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. \(\square \)
Example 5
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 \(\textsf {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\). \(\square \)
Example 6
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 article, rather than focusing on abstractions, we identify sufficient criteria for the concrete iteration (5) to terminate without any abstraction.
3 Stratification and guardedness
Subsequently, we concentrate on initial conditions in the \(\exists ^*\forall ^*\) fragment and universal invariants, i.e., where the invariant \(\Psi \) 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 7
Consider the FO transition system \({\mathcal {T}}\) over a monadic state predicate R, a binary state predicate E and a constant a. \({\mathcal {T}}\) consists of a single node u with a single transition \((u,\theta ,u)\) where \(\theta \) is given by
The weakest inductive invariant thus states that the unary predicate R only holds for elements which are not reachable from a via the edge predicate E. This property is not expressible in FO predicate logic. Accordingly, \(\Psi ^{(h)}[u]\ne \Psi ^{(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 are constant throughout each run of the transition system.
We only consider substitutions which are either guarded updates or resets. Thereby, a substitution \(\theta \) is called a (simultaneous) guarded update if it simultaneously modifies predicates \(R_1,\ldots ,R_r \in {{\mathcal {R}}_{ state }}\) by
where \(A \in {{\mathcal {A}}}\) is the input predicate of \(\theta \), \({\bar{y}}_{R_j}^{\sigma _j}\) is the sequence of variables obtained by applying the permutation \(\sigma _j\) to the sequence of FO variables \({\bar{y}}_{R_j}\), \({\bar{z}}_{j}\) is a sequence of FO variables, dedicatedly used for the right-hand side of \(R_j\) in \(\theta \), and \(\varphi _j,\psi _j\) are quantifier-free FO formulas without occurrences of predicate A which do not contain occurrences of left-hand sides \(R_1,\ldots ,R_r\) either. We remark here that, technically speaking, allowing permutations \(\sigma _j\) does not introduce extra technical difficulties, but conveniently supports specifications, e.g., as in Fig. 1 where a non-trivial permutation is used for the predicate \(\textsf {discuss}\) (see section 8 for a usage of such reordering).
The guarded update is called strict if additionally, all formulas \(\varphi _i\) are \(\bot \) (false), i.e., are missing. Note that we do not assume here that all left-hand sides in updates agree in their arities. Instead, for each j, the sum of the lengthes of \({\bar{y}}_{R_j}\) and \({\bar{z}}_j\) should all equal the arity of the input predicate A of the update. Accordingly, also the sequences of existentially quantified variables in right-hand sides of guarded updates need not agree in their lengthes. Guarded updates according to this definition, are specific instances of the basic constituents of workflows as considered in [3, 15]. There, simultaneous updates are called blocks, where the left-hand sides \(R_i\) are allowed to be extended (or filtered) by means of arbitrary FO formulas. Here, we only allow extensions and only by means of formulas of the restricted form (6).
Additionally, we now also allow substitutions to be resets. The substitution \(\theta \) is called a reset, if it substitutes just a single predicate R by means of
where \(\varphi \) is a quantifier-free FO formula without occurrences of the left-hand side R or any input predicate. The update \(\theta \) is called stratified, if additionally all substituted predicates \(R_j\) have identical level, and each predicate \(R'\) occurring in the \(\varphi _j,\psi _j\) has level less than \(\lambda (R_j)\). Likewise, a reset is called stratified, if all predicates occurring in the right-hand side for the substituted predicate R have levels less than \(\lambda (R)\).
According to our definition, a stratified guarded update, may simultaneously substitute predicates at the same level only. We thus might wonder whether this restriction could be lifted. For FO transition systems with this extension, however, termination can no longer be guaranteed.
Lemma 2
There exists a FO transition system \({\mathcal {T}}\) without assumptions, using stratified strictly guarded updates and resets, with simultaneous substitutions of predicates at different levels, together with some universal invariant \(\Psi \) such that for each \(h\ge 0\), \(\Psi ^{(h)}\) is universal FO definable, but \(\Psi ^{(h)}[u] \not \rightarrow \Psi ^{(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 \(\Psi =\{0\mapsto \top ,1\mapsto \top ,2\mapsto \textsf {error}\vee \lnot \textsf {hull}(a,b), 3\mapsto \top \}\) for constants a, b. Initially, the predicate \(\textsf {hull}\) is set to E. By executing the loop k times, either the error flag \(\textsf {error}\) is set to \(\top \), or \(\textsf {hull}\) receives at most \((k+1)\)fold compositions of E. Still, we can assign levels to the predicates used by \({\mathcal {T}}\) which meet the requirements of a stratification, namely,
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)\). For the iterates \(\Psi ^{(h)}\) at program point 2, we therefore obtain
Altogether, 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 the transitive closure of a binary relation is not FO definable, we conclude that the fixpoint iteration cannot terminate. \(\square \)
Fig. 2
FO transition system capturing transitive closure
×
Thus, the crucial issue which results in inexpressible weakest inductive invariants, is the use of the same input predicate in the simultaneous update of predicates at different level. In the next section, we indicate how to generally deal with SO quantifiers, once a guarded update has been applied.
4 Universal SO quantifier elimination
It is well-known that universal SO quantifiers can be removed from otherwise quantifier-free formulas [3, 23]. For example,
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.
for \(m\le n \in {\mathbb {N}}\) and fresh sequences of FO variables \({\bar{z}}_i\) where \(\varphi _i\) are FO formulas without occurrences of A. Then \(\forall A.\;\Psi \) is equivalent to
Here, juxtaposition is meant to denote the concatenation of the corresponding sequences of FO variables, while an equality \({\bar{x}}_i={\bar{x}}'_j\) for sequences \({\bar{x}}_i,{\bar{x}}'_j\) with \(\vert {\bar{x}}_i\vert \le \vert {\bar{x}}'_j\vert \) denotes the conjunction of equalities between the variables in \({\bar{x}}_i\) and the variables from the prefix of \({\bar{x}}'_j\) of the length \(\vert {\bar{x}}_i\vert \).
for \(m\le n \in {\mathbb {N}}\) where \(\varphi ,\varphi _i,\psi _j\) all are FO formulas without occurrences of A. Then \(\forall A.\;\Psi \) is equivalent to
In case that all formulas \(\varphi _i,i=1,\ldots ,m\) are all equivalent to \(\varphi '\) and and for \(j=m+1,\ldots ,n\), \(\varphi _j=\lnot \varphi '[{\bar{b}}_j{\bar{z}}_j/{\bar{y}}]\) where all lists \({\bar{a}}_i,{\bar{b}}_j\) have the same length, then the formulas (9) and (11) after second-order quantifier elimination of A, can be simplified to:
where for \(i=1,\ldots ,m\), \({\bar{y}}_i\) is the prefix of \({\bar{y}}\) of length \(\vert {\bar{a}}_i\vert \), while \({\bar{z}}_i\) is considered as the corresponding suffix, i.e., \({\bar{y}}= {\bar{y}}_i{\bar{z}}_i\). The equivalence for (10) is obtained by using the same definition for \(\varphi \), but replacing the formula \(\psi \) with
where \(\varphi _0,\varphi _1,\varphi _2,\varphi _3\) are quantifierfree formulas not containing occurrences of the SO variable A. Let \(\Psi \) a universal FO invariant. Then the following holds:
1.
The iterates \(\Psi ^{(h)}[u],h\ge 0\), in (5) all are effectively equivalent to universal FO formulas.
2.
The iteration terminates, i.e., \(\Psi ^{(h)} = \Psi ^{(h+1)}\) for some \(h\ge 0\), iff for each program point u, the weakest strengthening of all iterates \(\Psi ^{(h)}[u]\) is FO-definable.
Proof
Due to lemma 3, for each universal FO formula \(\psi \), each guard g of appropriate form, and each guarded update or reset \(\theta \) with input predicate A, \(\forall A.\,(\lnot g\vee \theta \psi )\) is equivalent to a universal FO formula. That implies statement (1). Now assume for for each \(h\ge 0\) and each \(v\in V\), \(\Phi ^{(h)}[v]\) is FO definable. Then due to the compactness theorem for FO predicate logic [25], there is some \(h\ge 0\) such that \(\Psi ^{(h)}[v] \leftrightarrow \Psi ^{(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} \Psi ^{(h)}[v]\) is again FO definable. \(\square \)
Example 10
Consider again the specification from Fig. 1, and let \(\theta _1,\theta _2,\theta _3,\) and \(\theta _4\) denote the substitutions occurring therein.
Assume that \(\Psi \) 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(\Psi ))\) is given by
The resulting formula \(\Psi '\) already equals the fixpoint for the loop.
Since the predicate \(\textsf {assign}\) only occurs negatively in \(\Psi '\) 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(\Phi '))\) is constructed from \(\Psi '\) via the substitution \(\theta _\textsf {assign}\) defined by
By the initial condition \({{\mathcal {H}}}\) from the introduction, \(\lnot \textsf {discuss}(x_1,x_2,p,d)\) generally holds at node 0 of the transition system, as well as \(\lnot \textsf {report}(x_i,p,r_i),\lnot \textsf {assign}(x_i,p),\) and \(\lnot \textsf {conf}(x_i,p)\) for \(i=1,2\). Therefore, \({{\mathcal {H}}}\) implies \(\Psi ''\), and the property \(\Psi \) at node 3 of the transition system is valid. \(\square \)
In this section we have shown comprehensively how to eliminate universal SO quantifiers introduced by guarded updates or resets in a FO transition system. In the next two sections, we will apply these results to FO transition systems which additionally are stratified.
5 Strictly guarded stratified updates
In this section, we consider FO transition systems without guards with stratified guarded updates and resets, where all guarded updates are strict. This means they all are of the form
for predicates \(R_1,\ldots ,R_r\) all of the same level. Let us call such a FO transition system strictly guarded and stratified.
Theorem 5
Assume we are given a strictly guarded and stratified FO transition system. Then for every universal invariant \(\Psi \), the weakest inductive invariant strengthening \(\Psi \) can be represented by universal FO formulas, and can effectively be computed.
Proof
For this proof, it is convenient to use the notation \(\Phi \ni \forall {\bar{x}}.\,c\) for a universal FO formula \(\Phi \), 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 \(\Phi \), 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 a stratified strictly guarded update with input predicate A which substitutes predicates of level s.
Let \(c'\) be a clause with \(\forall A.\,\theta (c)\ni \forall {\bar{z}}.\,c'\) where \({\bar{z}}\) is the list of newly introduced variables in \(c'\). Then either \(c=c'\) and \({\bar{z}}\) is empty, or the number of literals at level s of \(c'\) is less than the corresponding number of literals in c, while the set of literals at levels exceeding s stays the same.
where \(R_i{\bar{y}}_i, R_j{\bar{y}}_j\) are the literals of c substituted by \(\theta \), while \(c_0\) does not contain occurrences of left-hand sides of \(\theta \).
If \(\theta \) is a reset, all literals containing \(R_i\) are eliminated from c.
Therefore, the assertion of the lemma holds. Now assume that \(\theta \) is a strictly guarded update where \(\theta (R_i{\bar{y}}_{R_i}) = R_i{\bar{y}}_{R_i}\vee \exists {\bar{z}}_{i}. A{\bar{y}}_{R_i}^{\sigma _i}{\bar{z}}_{i} \wedge \psi _i\) for some permutation \(\sigma _i\). 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 \(\Theta \) denote a finite set of stratified guarded substitutions where all updates in \(\Theta \) 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 \Theta \) 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 \(\Psi ^{(h)}[u]\ni \forall {\bar{z}}.c\) for any u and h, is finite. From that, the statement of the theorem follows. \(\square \)
Theorem 5 leaves open the case of transition systems with stratified 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.
6 Positive guarded and stratified updates
Let us consider another case where termination can be guaranteed in presence of updates as well as resets. We call an update or reset \(\theta \)positive if all predicates only occur positively in the right-hand sides of \(\theta \). Let us call a FO transition system positive if it uses no assumptions and only positive stratified guarded updates and resets at all levels at least 1.
Theorem 7
Assume that \({\mathcal {T}}\) is a positive FO transition system where all updates are single. Then for every universal invariant \(\Psi \), the weakest inductive invariant implying \(\Psi \) is again universal and can effectively be computed.
Proof
Let \(\Theta \) denote the substitutions occurring at edges in \({\mathcal {T}}\). For \(\theta \in \Theta \), let \([\![ \theta ]\!]\) denote the transformation of universal FO formulas which maps every universal FO formula \(\psi \) to a universal FO formula equivalent to \(\forall A.\theta (\psi )\), if A is the input predicate corresponding to \(\theta \). Let \(\pi = \theta _L\ldots \theta _1\) denote a sequence of substitutions from \(\Theta \). Then \([\![ \pi ]\!] = [\![ \theta _N ]\!]\circ \ldots \circ [\![ \theta _1 ]\!]\) is the composition of the transformations corresponding to the substitutions occurring in \(\pi \). Now consider a quantifierfree formula \(\psi \) in conjunctive normal form with predicates from \({{\mathcal {R}}_{ state }}\) and FO variables from X. Consider some \(\theta \in \Theta \). Since \(\theta \) is a stratified reset or a stratified guarded update which is single and positive, \([\![ \theta ]\!](\psi )\) can be chosen in such a way that all occurring argument lists \({\bar{b}}\) of positive literals \(R{\bar{b}}\), \(R\in {\mathcal {R}}\), only use variables from X. Since \(\theta \) is single, SO quantifier elimination of the input predicate A of \(\theta \) can be realized by a single substitution of the form
for suitable \(n\ge 0\) and sequences \({\bar{a}}_{i}\) of FO variables from X. Let us call the right-hand side here a worst attacker. This means that, for all levels \(t=L,\ldots ,1\), there are only finitely many possibilities of worst attackers to substitute the occurring input predicates. Let L denote the maximal level of predicates from \({{\mathcal {R}}_{ state }}\). Moreover for \(t=L,\ldots ,1\), let \({\bar{z}}_t\) denote one distinct enumeration of variables occurring in substitutions in \(\Theta \) whose right-hand sides are of level t. The formulas \([\![ \pi _N ]\!](\psi )\) thus can all be represented as finite conjunctions g of generalized clauses \(c^{(L)}\) according to the following grammar:
where \(c_0\) is a disjunction of literals without negative literals \(\lnot R{\bar{b}}\) using FO variables from X; while for \(0\le t\le L\), the clause \(c^{(t)}\) satisfies the following side constraints:
For every occurring negative literal \(\lnot R{\bar{b}}\), \(\lambda (R)\le t\) holds and all variables in \({\bar{b}}\) are contained in X or occur in \({\bar{z}}_L\ldots {\bar{z}}_{t+1}\);
\(e_t\) ranges over equalities or disequalities between FO variables from X or \({\bar{z}}_L\ldots {\bar{z}}_{t+1}\).
Moreover, for \(o^{(t)}\), all FO variables occurring in the lists \({\bar{a}}_i\) are from X only, while those occurring in \({\bar{b}}\) are either from X or occur in \({\bar{z}}_L\ldots {\bar{z}}_{t-1}\). By induction on t, we verify that for each level \(t\ge 0\), the number of non-equivalent formulas \(o^{(t)}\) and thus also the number of non-equivalent formulas \(c^{(t)}\) is finite. We conclude that also the number on non-equivalent formulas c as well as the number of non-equivalent formulas g is finite.
Accordingly, the number of non-equivalent formulas \(\forall A_1\ldots A_N.\,\pi (\psi )\) is finite — implying that for every universal invariant \(\Psi \), \(\Psi ^{(h+1)} = \Psi ^{(h)}\) for some \(h\ge 0\). From that, the statement of the theorem follows. \(\square \)
The proof argument for theorem 7 cannot easily be extended to unrestricted stratified guarded substitutions. In presence of negated literals in substitutions or updates which are not single, the arguments of positive literals \(R{\bar{a}}\) occurring in \([\![ \pi ]\!](\psi )\) need not necessariliy have already occurred in \(\psi \). For the next result, we therefore have to rely on a different proof strategy.
7 Stratified guarded updates
Let us finally consider FO transition systems without assumptions where all occurring substitituions are resets or guarded updates which are stratified. Let us call such a FO transition system stratified guarded. In [3], termination was announced for stratified guarded FO transition systems without resets, where additionally 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 by allowing stratified resets — at least at the maximal and minimal levels.
Theorem 8
Assume that \({\mathcal {T}}\) is a stratified guarded FO transition system where resets only occur for predicates of level 1 and the maximal level L. Then for every universal invariant \(\Psi \), the weakest inductive invariant is again universal and can effectively be computed.
Proof
We show that there is some \(h\ge 0\), so that \(\Psi ^{(h+1)} = \Psi ^{(h)}\). Since by lemma 3, \(\Psi ^{(h)}[u]\) is a universal formula for all \(h\ge 0\) and program points u, the statement of the theorem follows.
Let \(\Theta \) denote the finite set of stratified guarded substitutions occurring in \({\mathcal {T}}\). W.l.o.g., we assume that each substitution in \(\Theta \) simultaneously substitutes all predicates at a given level t. Let \(\psi \) a quantifierfree FO formula in negation normal form. Let \(\pi = \theta _N,\ldots ,\theta _1\) be any sequence of substitutions where for each \(i = 1,\ldots ,N\), \(\theta _i = \theta '[A_i/A_{e_i}]\) holds for a fresh input predicate \(A_i\), and some substitution \(\theta '\in \Theta \). Thereby, let \(\lambda (A_i)\) denote the level of left-hand sides of \(\theta '\). Termination of fixpoint iteration is based on the following lemma. \(\square \)
Lemma 9
There is a fixed finite sequence \({{\textbf {z}}}\) of variables only depending on \(\psi \) and the substitutions from \({\mathcal {T}}\) so that \(\forall A_N\ldots A_1.\pi (\psi ) = \forall {{\textbf {z}}}.\psi '\) for some quantifierfree FO formula \(\psi '\). In particular, \({{\textbf {z}}}\) can be chosen independently of the length N of \(\pi \).
Since the number of quantifierfree FO formulas with a given fixed finite set of FO variables is finite, lemma 9 implies that the number of non-equivalent universal FO formulas possibly occurring as \(\forall A_N\ldots A_1.\pi (\psi )\) for every universally quantified FO formula \(\psi \), and thus also the number of non-equivalent conjunctions of these formulas is finite. Accordingly, there must be some \(h\ge 0\) so that in (5), \(\Psi ^{(h+1)} = \Psi ^{(h)}\), and the theorem follows. \(\square \)
Let us first consider the case where there is no reset of predicates. Let \({{\mathcal {R}}_{ state }}\) denote the finite set of predicate symbols used by \({\mathcal {T}}\). Let X and Z denote the finite sets of variables occurring in \(\psi \) and introduced by substitutions from \(\Theta \), respectively. Let L denote the maximal level of a predicate in \({\mathcal {R}}\). For \(1\le t\le L\), let \(V_t\) denote the set of all variables
$$\begin{aligned} z_{R,{\bar{b}}} \end{aligned}$$
(16)
with \(z\in Z\), \(\lambda (R) = t\), and \({\bar{b}}\) a sequence of variables from \(X\cup V_L\cup \ldots \cup V_{t+1}\) whose length equals the arity of R. We then will use the set \(V = V_1\cup \ldots \cup V_L\) as our set of bound variables. According to the definition of the \(V_t\), the set V is finite. By induction on the length N of \(\pi \), we construct a formula in a particular normal form \(\psi _N\) which is equivalent to \(\pi (\psi )\). In this construction, we make sure that all variables bound by existential or universal quantifiers are always taken from V. The normal form g of formulas we rely on, consists of a finite conjunction of generalized clauses c which are built up according to the following abstract grammar
In the second line, \(c_0\) is an ordinary clause without occurrences of input predicates, \(A'\) is an input predicate where all predicates occurring in \(g'\) have levels less than \(\lambda (A')\). In the third line, R is a predicate, \({\bar{b}}\) are sequences of arguments, \({\bar{z}}_R\) is a sequence of FO variables whose length only depends on R and contains all FO variables required by substitutions of R, \(A_n\) are input predicates of levels \(\lambda (R)\), and all predicates occurring in any of the \(c_n\) have levels less than \(\lambda (R)\). A formula \(f_{R,{\bar{b}}}\) is also called negation tree with head \(\lnot R{\bar{b}}\). \(f_{R,{\bar{b}}}\) is called non-trivial, if it contains occurrences of input predicates, i.e., the conjunction in the second conjunct is non-empty. Thereby, we maintain the invariant that on the toplevel, i.e., outside the scopes of all quantifiers, the heads of all negation trees are distinct.
This normal form can be obtained for \(\psi \) by constructing the conjunctive normal form of \(\psi \) and thereby, removing all duplicates of literals in clauses. Let \(\psi _0\) denote the resulting conjunction for \(\psi \). Now assume that we have already constructed the normal form \(\psi _{N-1}\). By using distributivity of \(\wedge \), the corresponding normal form for \(\psi _N = \theta _N(\psi _{N-1})\) can be readily computed. For maintaining the invariant on negation trees, we recall that \(\lnot R{\bar{b}}\vee \lnot R{\bar{b}}\wedge g \longleftrightarrow \lnot R{\bar{b}}\), i.e., newly created literals \(\lnot R{\bar{b}}\) in clauses kill already existing negation trees with this head.
Given the normal form \(\psi _N\) for \(\pi (\psi )\), we now successively apply SO quantifier elimination. We proceed from input predicates \(A_i\) of higher levels downwards towards the input predicates of smaller levels. For each clause, we thereby collect the lists of FO variables \({\bar{z}}_t\) required to be universally quantified and prove that these lists possibly introduced for level t, consist of variables from \(V_t\) only. In the end, we thus arrive at a formula \(\forall {{\textbf {z}}}_1\ldots {{\textbf {z}}}_L.\psi '\) where \({{\textbf {z}}}_t\) is the sequence of variables in \(V_t\), and \(\psi '\) is a quantifierfree conjunction of (plain) clauses with variables from \(X\cup V\) only. Since there is only a finite set of of such clauses, the theorem follows.
So, let \(\tau \) denote a permutation of \(\{1,\ldots ,N\}\) so that \(\lambda (A_{\tau (N)})\le \ldots \le \lambda (A_{\tau (1)})\) holds. In particular, \(\lambda (A_{\tau (1)})\) and \(\lambda (A_{\pi (N)})\) denote input predicates of highest and lowest occurring levels, respectively. Then we successively remove the occurrences of \(A_{\tau (1)},A_{\tau (2)},\ldots \) by maintaining the normal form of the resulting formulas — while introducing fresh bound variable names just from the set V. Let \(\psi '_{L+1} = \psi _N\). Now we proceed level by level. for \(L\ge t >0\), assume that \(\forall {{\textbf {z}}}_{t+1}\ldots {{\textbf {z}}}_{L}.\psi '_{t+1}\) has already been constructed such that \(\psi '_{t+1}\) is in our normal form where the heads of all non-trivial negation trees on top-level are distinct and have levels at most t. Let us consider a single generalized clause c of \(\psi '_{t+1}\). Let \(f_{R_1,{\bar{b}}_1},\ldots , f_{R_m{\bar{b}}_m}\) denote the sequence of top-level negation trees in \(\psi '_{t+1}\) of level t in c.
If this sequence is empty, then we set \({{\textbf {z}}}_{t} = \epsilon \) (the empty sequence) and \(\psi '_t\) as the formula obtained from \(\psi '_{t+1}\) by removing all occurrences of subformulas \(\exists {\bar{z}}_R.A'{\bar{b}}{\bar{z}}\wedge \psi '\) with \(\lambda (A') = t\).
Otherwise, let \(A_{\tau (j_1)}\ldots A_{\tau (j_2)}\) denote the subsequence of input predicates of level t occurring in c. Then for each \(j=1,\ldots ,m\), the negation tree \(f_{R_j,{\bar{b}}_j}\) is of the form
for suitable input predicates \(A'_k\) of level t, subsequences \({\bar{z}}_{jk}\) of \({\bar{z}}_{R_j}\) and (generalized) clauses \(c_{jk}\) containing predicates only of levels less than t. Since the heads of the negation trees \(f_{R_j,{\bar{b}}_j}\) are all distinct, we can rename the corresponding universally quantified variables to distinct sequences \({\bar{z}}_{R_j,{\bar{b}}_j} = z_{(R_j,{\bar{b}}_j),1}\ldots z_{(R_j,{\bar{b}}_j),l_j}\) if \(l_j\) is the length of the corresponding list of bound variables and let the sequences \({\bar{z}}_{{\bar{b}}_j,jk}\) be appropriate subsequences of this list for the \({\bar{z}}_{jk}\). By inductive hypothesis for variables in \({\bar{b}}_j\) and the definition of the set \(V_t\), all these variables are contained in \(V_t\). Therefore, c is equivalent to the formula \(\forall {{\textbf {z}}}_t.c'\) where \(c'\) coincides with c up the negation trees of level t, which now take the form
(\(j=1,\ldots ,m\)). Performing SO quantifier elimination of all input predicates \(A_{\tau (j_1)},\ldots ,A_{\tau (j_2)}\) in a row removes all subformulas \(\exists {\bar{z}}_{R'}.A'{\bar{a}}{\bar{z}}_{R'}\wedge \psi '\) where \(\lambda (A') = t\) from \(c'\), and additionally replaces the subformulas (18) with formulas
for suitable conjunctions of (generalized) clauses \(g_{ji}\) in with constants from X and free variables from \({\bar{z}}_{R}\) and some list of parameters \({\bar{y}}\) for which a subformula \(\exists {\bar{z}}_{ji}.A'_k{\bar{a}}_{ji}^{\sigma _{ji}}{\bar{z}}_{ji}\wedge g_{ji}[{\bar{a}}_{ji}/{\bar{y}}]\) has occurred in \(c'\). In particular, each predicate occurring in any of the \(g_{ji}\) is of level less than t. By distributivity, the resulting formula is equivalent to a conjunction \(g'\) of (generalized) clauses \(c''\) each of which is obtained from \(c'\) by replacing each of the subformulas (18) with \(\lnot R_j{\bar{b}}_j\), or, for some k and some subset \(I\subseteq \{1,\ldots ,n_j\}\), with the clause
where \(c'_{ji}\) is any clause of \(g_{ji}\). The clauses from \(g'\) constructed in this way, may contain negation trees which agree in their heads. Consider two such negation trees both with head \(\lnot R{\bar{b}}\) occurring in the same clause \(c''\) of \(g'\) on top-level. If both originate from \(\psi \) or have been introduced by means of the same substitution, say, \(\theta _j\), the same sequence of substitutions has been applied to both, and subsequently also to their negation trees. Accordingly, the two negation trees are equivalent, meaning that one of them can be removed from \(c''\). Therefore, now assume that one literal \(\lnot R{\bar{b}}\) has been introduced by substitution \(\theta _j\) while the the other did already occur in \(\psi _{j-1}\). That means that the sequence of substitutions applied to the later one and its negation tree, also is applied to the earlier one and its negation tree. In their disjunction (now introduced due to SO quantifier elimination), therefore, the negation tree of the earlier literal implies the negation tree of the later, and therefore can be omitted. Performing this normalization on the clauses of \(g'\), we achieve that in the resulting conjunction \(g''\) of (generalized) clauses
all heads of top-level negation trees are distinct. Then we set \(\psi '_t\) to \(g''\).
In order to compute an explicit bound on the number of possible FO variables occurring as arguments to predicates of level \(t=L,\ldots ,0\), let us introduce the following structural parameters:
$$\begin{aligned} \begin{array}{lll} v &{} \quad \text {---} &{}\quad \text {the number of variables occurring in } \psi \\ L &{} \quad \text {---} &{} \quad \text {the number of levels of predicates } \\ r &{} \quad \text {---} &{} \quad \text {maximal arity of a predicate } \\ m &{} \quad \text {---} &{} \quad \text {maximal number predicates at some level } i \\ l &{} \quad \text {---} &{} \quad \text {maximal length of } {\bar{z}}\text {in subformulas } \exists {\bar{z}}.\,\psi \text {occurring in the substitutions from } \Theta \end{array} \end{aligned}$$
For \(t=L,\ldots ,0\), we inductively determine a bound \(B_t\) to the number of distinct FO variables possibly occurring as arguments of literals at level t. Thereby, we set \(B_L = v\), since the only literals at level L occurring in \(c'\) already must have occurred in \(\psi \). Therefore, assume that \(t < L\) and a bound \(B_{t+1}\) has already been found. Given the number \(B_{t+1}\), the number of negated literals of predicates at level \(t+1\) can be bound by \(m\cdot B_{t+1}^r\). For each of these literals, a fresh list of variables of length at most l may be provided. Accordingly, we set
It remains to consider the case when resets occur either on the highest level L or at level 1. We claim that with these kinds of resets, still the same set V for bound variables suffices to construct a FO universally quantified formula for \(\forall A_1\ldots A_N.\pi (\psi )\). Let us first consider resets of predicates at top-level L. Each of these, either has no effect or replaces all occurrences of one predicate R with \(\lambda (R) = L\) with a quantifierfree formula with occurrences of state predicates of lower levels and no input predicates. The only FO variables occurring in literals \(R{\bar{b}}\) or \(\lnot R{\bar{b}}\) for predicates R of level L are the variables from X occurring already in \(\psi \). Accordingly, we modify the first phase of constructing \(\psi _1,\ldots ,\psi _N\) as follows. We put the list \({{\textbf {z}}}_L\) as universally prenex in front of all \(\psi _j\) in order to have a reservoir of FO variables for all univerally quantified bound variables introduced at level L. As soon as an update substitution \(\theta _i\) of a predicate R at level L occurs, we rename in each clause the universally quantified variables from \({\bar{z}}_R\) introduced for \(\lnot R{\bar{b}}\) to \({\bar{z}}_{R,{\bar{b}}}\) from the reservoir and immediately perform SO quantifier elimination for \(A_i\). Then we bring the resulting formula into the format g to obtain \(\psi _i\). With this preparation, a reset \(\theta _j\) at level L can be dealt with during the construction of the sequence \(\psi _1,\ldots ,\psi _N\) just by replacing literals at level L with appropriate clauses of literals with predicates of lower level all using variables from X as arguments only. In particular, no new variables are introduced. For the second phase, it then remains to perform SO quantifier elimination just for the levels \(L-1,\ldots ,1\).
Now additionally, consider resets of predicates at level 1. In principle, we proceed as before. The resets at level 1, however, may additionally introduce subformulas of the form \(o_{{\bar{b}}}\) in clauses where
where \({\bar{b}}\) is a sequence of variables, \(A_k\) are input variables of level 1, and \(c_n\) contains predicates of level 0 only with arguments possibly from X, \({\bar{b}}\), and \({\bar{z}}\). No uniqueless can be guaranteed for subformulas of the form \(o_{{\bar{b}}}\). We note, however, that in the second phase when we perform SO quantifier elimination of SO predicates of level 1 for a (generalized) clause c, a formula is encountered of the form
where \(c_0\) consists of literals using variables from \(V'\), the lists of variables \({\bar{a}}_{lji}\) are only from \(V'\), and the subformulas \(g_{lji}\) and \(c_{lj}\) use state predicates of level 0 only where all occurring FO variables are from \(V'\cup Z\). The number of non-equivalent such formulas \(g_{lji}\) as well as \(c_{lj}\) with this restriction onto the occurring FO variables, however, is finite. Therefore, there is a fixed finite prefix of FO variables, independent of the length of the sequence of substitutions \(\pi \) to take all universal quantifications from (23) into account.
Altogether, therefore, the number of FO variables in quantified clauses \(\forall {\bar{z}}'.c'\) contained in \(\pi (\psi )\) remains bounded – even when we allow resets both on the maximal level and on level 1. This completes the proof of lemma 9.
We remark that theorem 8 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) are empty. In general, though, the proof technique of theorem 8 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.
8 Noninterference for Multi-agent systems
In the following we would like to apply the termination results from the last section to prove non-interference for multi-agent systems represented as FO transition system. In this representation, we assume the FO transition system to be executed by agents. Thereby, an agent a can observe all tuples of state relations that mention her in the first component (i.e., all tuples of the form \(a{\bar{b}}\) satisfying some predicate R). Accordingly, we assume all predicates to have arities at least 1. Subsequently, we assume that each substitution of the FO transition system \({\mathcal {T}}\) either is an update or a reset. In particular, there are no conditions at edges in the control-flow graph. Besides public input from the environment, we distinuish two dedicated further kinds of input predicates, namely, oracles and choices.
An oracle predicate O is used to represent secret data input to the FO transition system which is meant to be disclosed only to a subset of agents. Thereby, each oracle O comes with a FO formula \(\delta _O x{\bar{y}}\) specifying for each agent x, which tuples \({\bar{y}}\) should possibly be visible to x.
We remark that an oracle predicate O with \(\delta _O x{\bar{y}}= \top \) (true) for all \(x,{\bar{y}}\), does not pose any restrictions on the visibility of tuples \({\bar{y}}\) and thus may serve as (public) input from the environment. It is for conceptual clarity only, that we consider environment input separately.
Choice predicates C formalize the behavior and individual decisions of agents. The literal \(C x{\bar{y}}\), when true, indicates that agent x offers tuple \(x{\bar{y}}\) for the current update operation. Let \({{\mathcal {R}}_{ env }},{\mathcal {R}}_{ high },{\mathcal {R}}_{ low }\subseteq {{\mathcal {A}}}\) denote the set of all environment input, oracle and choice predicates, respectively, that are used by the given FO transition system.
Consider, e.g., the FO transition system from Fig. 1. Then \(A_1,A_2\) may be considered as input from the environment (providing information on conflicts and the assignment of papers to pc members), while \(A_3\) is an oracle: it provides reports on papers which should not be disclosed to all members of the pc. The input predicate \(A_4\), on the other hand, represents the choices of pc members what to contibute to the discussion on papers. According to our convention, it is agent \(x_2\) who (by means of \(A_4\)) decides to add tuples to predicate \(\textsf {discuss}\) which in this way become visible to \(x_1\).
Noninterference is best formulated as a 2-hyperproperty [26], that is, a property of pairs of traces. In our application, the sequence of edges traversed by an execution of the workflow is determined externally, i.e., independent of any oracle or choice predicate. For instance in case of a conference management system, it is up to the PC chair to decide when a particular stage is complete and which next stage to execute. This means that we are only interested in 2-hyperproperties where the considered two traces follow the same control flow path, but may differ in the sequences of attained states. This restriction has also been imposed in [15, 16]. In order to reason about the pairs of states attained by a pair of traces, we introduce a copy \({\mathcal {R}}'=\{R'\mid R\in {\mathcal {R}}\}\) of the predicates in \({\mathcal {R}}\) and assume that the states \(s'_i\) are expressed by means of the predicates in \({{\mathcal {R}}_{ state }}'\), i.e., primed state predicates. Thus, we can combine each pair \(\langle s_i,s'_i \rangle \) of first-order structures into a single structure \(s_i\otimes s'_i\) over \({{\mathcal {R}}_{ state }}\cup {{\mathcal {R}}_{ state }}'\). Following [3, 15, 16], noninterference is expressed from the point of view of a single (but arbitrary) agent, and the notions of high/low security inputs/outputs from the standard definition of noninterference [17] are interpreted with respect to this agent. Furthermore, the property is parameterized by an assumption on the behavior of agents (called agent model) and by declassification conditions, which specify when and what information can be legitimately exposed. Therefore, Noninterference with Declassification and Agent model (NDA) is expressed by the FOLTL formula
where \(\textsf {G}\) is the LTL globally operator. The property states that for any two traces following the same control-flow path, a given agent model for every agent a, and the assumption that public input from the environment does not differ on both traces, that the noninterference property holds iff agent a is never able to observe a difference between two traces that differ only in the (non-declassified) inputs from the oracles:
where \({\bar{y}}_R,{\bar{z}}_R,{\bar{z}}_O\) are sequences of distinct variables of appropriate lengthes. For each oracle predicate O and agent x, the formula \(\delta _{O}x{\bar{z}}_O\) using predicates from \({{\mathcal {R}}_{ state }}\) encodes a declassification condition that specifies which tuples \({\bar{z}}_O\) from O can be made visible without causing a security breach to x. For our running example, we use \(\delta _O(x, y, p, r) := \lnot \textsf {conf}(x,p)\). This example declassification condition allows any agent x to safely read reports p by reviewer y on paper p, as lang as x neither is an author of p nor has declared conflict with p.
For any agent, we consider two kinds of possible behavior. One agent either stubbornly makes the same choices, independently of its observations; or its choices may depend on previous observations, i.e., it acts causally. Causal behavior characterizes the behavior of members of an adversarial coalition who in this way try to spread secret information. The two behaviors are captured by the following formulas, respectively.
$$\begin{aligned} same\_low\_inputs (x) := \bigwedge _{C\in {\mathcal {R}}_{ low }} \big (\forall {\bar{z}}_C.\, C x{\bar{z}}_C \leftrightarrow C' x{\bar{z}}_C\big ) \end{aligned}$$
and \(\textsf {W}\) denotes the weak until LTL operator. Note that any stubborn agent also satisfies the causality assumption which allows for more behaviors. Therefore, the most general agent model is when each agent is causal, while the most restrictive model is when each agent is stubborn.
We thus assume that the \( agent\_model \) formula from the formalization of NDA can be instantiated with one of the following formulas:
where \(t\ge 0\). Note that \( agent\_model ^{(c,0)}\equiv \forall x. stubborn (x)\). We denote this formula by \( agent\_model ^{(s)}\).
9 Encoding agent models and declassification
The key idea for verifying NDA from [3] is to introduce a fresh agent constant a, and then encode property (24) for a, a particular agent model and a given FO transition system \({\mathcal {T}}\) as an invariant of a (suitably defined) synchronous self-composition of the FO transition system \({\mathcal {T}}\) in a way that the invariant consists of universal FO formulas only. For convenience, we recall these constructions in order to adapt these to the specific setting of FO transition systems with guarded stratified updates and resets. Let us first assume that all agents are stubborn. The new FO transition system \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) then is constructed as follows. Let \({{\mathcal {R}}'_{ state }}\) denote the set of primed predicates \(R'\) corresponding to the state predicates R used by \({\mathcal {T}}\). For a first-order formula \(\varphi \) with predicates from \({{\mathcal {R}}_{ state }}\), let \([\varphi ]'\) denote the formula obtained from \(\varphi \) by replacing each predicate \(R\in {{\mathcal {R}}_{ state }}\) with the corresponding predicate \(R'\) in \({{\mathcal {R}}'_{ state }}\). Then each edge \(e=(u,\theta ,v)\) of \({\mathcal {T}}\) gives rise to a sequence of edges
for a sequence of fresh auxiliary nodes \(u_{e,1},\ldots ,u_{e,r}\) and a sequence \(\theta _0,\ldots ,\theta _r = {{{\mathcal {P}}}}^{(s)}_a\theta \) defined as follows.
Reset.
If \(\theta \) is a reset of the form \(R{\bar{y}}\,{:=}\,\varphi \), then \({{{\mathcal {P}}}}^{(s)}_a(\theta )\) is given by the sequence of resets, first, of R, then of \(R'\):
If A is an input predicate from the environment, or a choice predicate, then A is used both for updating the state predicates and the primed state predicates. This means that \({{{\mathcal {P}}}}^{(s)}_a(\theta )\) is given by the single update
In particular, no auxiliary nodes are required here.
If the input predicate A equals some secret oracle O, then the construction must make sure that, generally, the value of O may differ on both traces – up to when declassification for O and a applies. Accordingly, we split the corresponding update into the sequence of updates \(\theta _0,\theta _1,\theta _2\).
The update \(\theta _0\) takes care of argument tuples \(x{\bar{y}}\) where declassification w.r.t. agent a applies, while \(\theta _1,\theta _2\) deal with argument tuples where declassification does not apply.
The update \(\theta _0\) is as (25) only that the formulas \(\psi _j,[\psi _j]'\) in the right-hand sides are now replaced with
Tuples then may independently be added to \(R_j\) and \(R'_j\), when declassification does not apply. This independent addition is taken care of by the updates \(\theta _1,\theta _2\):
Causality. Let us now consider causal agents. The corresponding new FO transition system \({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\) is constructed as the FO transition system \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) – with the only difference that choices of agents now may depend on whether they previously have acquired knowledge about secrets or not.
In order to capture causality, a new unary predicate \(I(x)\) is introduced which records all agents x that have already made observations depending on information secret to a. These agents’ choices may diverge when updating predicates \(R,R'\), respectively. Initially, \(\forall x.\lnot I(x)\) holds.
Moreover, after each sequence of substitutions realizing the modification of unprimed or primed state predicates, the predicate \(I\) itself must be updated — depending on whether the substituted predicates \(R_1,\ldots , R_r\) differ from their primed versions. This update \(\theta _I\) is given by
where \({\bar{z}}_j\) are lists of distinct FO variables, and \({\bar{z}}\) is an enumeration of all FO variables occurring in the lists \({\bar{z}}_j\). Informally, update \(\theta _I\) checks wether a difference in any relation \(R_j\) can be been observed by agent x and if so, adds x to the predicate \(I\). The input predicate A guards this check, which allows us to later eliminate the existential quantifier during the fixpoint iteration.
Beyond the addition of \(\theta _I\), a second modification occurs for updates \(\theta \) of the form
which query some choice predicate C. This update is simulated in the self-composition by the sequence of substitutions \(\theta _0,\theta _1,\theta _2,\theta _I\). Thereby, \(\theta _0\) is defined as (25) (with \(A=C\)) — with the only exception that the subformulas \(\psi _j,[\psi _j]'\) in right-hand sides are replaced with
if x is the first variable from the sequence \({\bar{y}}_{R_j}^{\sigma _j}{\bar{z}}_j\). The substitutions \(\theta _1,\theta _2\) perform independent updates — given that agent x already has been informed. This means that
\(A_3\) is a secret oracle with corresponding declassification formula \(\lnot \textsf {conf}(a,p)\). Let us first consider stubborn agents only: Then the transformation results in the sequence of three updates
where \(A_4\) is a choice predicate, allowing agent \(x_2\) to decide which tuples to add. In case of stubborn agents, agent choices are independent of acquired information about secrets. Therefore, the transformation results in just one (simultaneous) update of both \(\textsf {discuss}\) and \(\textsf {discuss}'\) together with an update of the predicate \(I\). In case of causal agents, however, four updates are introduced in a row, namely,
Splitting the updates to \(\textsf {discuss}\) and \(\textsf {discuss}'\) into three only takes effect for agents \(x_2\) which are already informed, i.e., for which \(I(x_2)\) holds true. For the others, just the first (simultaneous) update takes effect. \(\square \)
The transformed workflow \({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\) (or \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\)) captures all pairs of traces of \({\mathcal {T}}\) that satisfy the causal (or stubborn) agent model together with declassification, relative to a. We recall the following theorem from [3].
Theorem 10
[ [3]] Let \({\mathcal {T}}\) without assumptions and stratified guarded updates and resets only.
Let \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) (\({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\)) denote FO transition systems obtained as the self-composition of \({\mathcal {T}}\) for stubborn (causal) agents. Let \(\Phi _{\text {NDA}}\) denote the universal invariant mapping each node u to the formula
where for each predicate \(R\in {{\mathcal {R}}_{ state }}\), \({\bar{y}}'_R\) is an appropriate list of distinct FO variables, and \({\bar{y}}\) is an enumeration of the FO variables occurring in any of the \({\bar{y}}'_R\).
Then the following holds for \({\mathcal {T}}\) with initial hypothesis \({{\mathcal {H}}}\).
1.
2-hyperproperty (NDA) holds for stubborn agents iff invariant \(\Phi _{\text {NDA}}\) holds for \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) with initial hypothesis
Theorem 10 allows us to apply our methods for constructing weakest inductive invariants for proving NDA for certain FO transition systems. Let us first consider stubborn agents only. Assume that the FO transition system \({\mathcal {T}}\) is stratified and guarded without using assumptions at edges. Then the same is true for the transformed workflow \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) which takes care of stubbornness of agents and declassification relative to a — at least, when for each oracle O, the declassification formula \(\delta _O\) is sufficiently well-behaved — i.e. is quantifierfree and uses only predicates of level less than the left-hand sides of substitutions where O is queried. Thereby, we assign to primed predicates \(R'\) the same levels as the corresponding unprimed predicates R. Furthermore, if all resets of \({\mathcal {T}}\) occur either on level 1, or the maximal level, then this property also holds for \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\). Likewise, if \({\mathcal {T}}\) uses arbitrary resets, but strict updates only, then the same holds true also for \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\). As application of Theorems 8 and 5, we therefore obtain:
Theorem 11
Consider a FO transition system \({\mathcal {T}}\) without assumptions, but with resets and stratified guarded updates Assume that for each oracle O queried in some update \(\theta \), the corresponding declassification formula \(\delta _O\) is quantifierfree where each predicate occurring in \(\delta _O\) has level less than the level of the left-hand sides in \(\theta \). Assume further that one of the two conditions are met:
1.
All updates are strictly guarded; or
2.
All resets either occur at maximal level or at level 1.
Assume that the initial hypothesis \({{\mathcal {H}}}\) for \({\mathcal {T}}\) is given as a FO formula from the prenex class \(\exists ^*\forall ^*\). Assume that all agents participating in \({\mathcal {T}}\) are stubborn. Then NDA for \({\mathcal {T}}\) with stubborn agents is effectively decidable.
Proof
Under each of the two assumptions, the self-composition \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) can be effectively constructed and satisfies either the assumptions of Theorem 5 or Theorem 8. Therefore for every universal invariant \(\Phi _{\text {NDA}}\), the weakest inductive invariant \(\Psi \) can be effectively computed so that \(\Psi [u]\rightarrow \Phi [u]\) for every is again uniform and leveled. This invariant then holds iff the conjunction of the formula (32) and \(\lnot \Psi [v_0]\) is unsatisfiable. Since both formulas are effectively contained in the prenex class \(\exists ^*\forall ^*\), the claim of the theorem follows. \(\square \)
Example 12
Consider again the FO transition system \({\mathcal {T}}\) from Fig. 1 where all participating agents are stubborn. In order to prove NDA for the arbitrary agent a, it suffices to verify for every program point of the self-compostion \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) the following invariant holds:
Since the self-composition \({{{\mathcal {P}}}}^{(s)}_a({\mathcal {T}})\) is stratified strictly guarded (here even without resets), the iterative strengthening of the invariant terminates with a weakest inductive invariant. This invariant is too complicated to be spelled out here. We argue, however, that throughout all program points 0, 1, 2, 3 of the FO transition system,
holds. The latter property can, e.g., be proven for the original FO transition system \({\mathcal {T}}\). Each of these invariants is already inductive. Together, they imply that
holds for all program points as well — implying that the invariant (34) holds. \(\square \)
We would like to apply the same strategy to certify NDA now for FO transition systems with causal agents. Again assume that the FO transition system \({\mathcal {T}}\) is stratified and guarded. The workflow \({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\), however, is no longer stratified. This is due to the auxiliary predicate \(I\) introduced by \({{{\mathcal {P}}}}^{(c)}_a\). That predicate is queried at updates of all updated predicates \(R,R'\), \(R\in {{\mathcal {R}}_{ state }}\) where a choice predicate is queried. Likewise it is updated by means of formulas which depend on the same predicates. Still, we can apply fixpoint iteration on universal formulas — which, however, is no longer guaranteed to terminate. Thus, we obtain a possibly incomplete method for certifying NDA for agent model \( agent\_model ^{(c)}\). The potential non-termination, however, does not come as a surprise as NDA in general is undecidable for an unbounded number of causal agents [15]. Interestingly, the situation is different when only a fixed bounded number of agents behaves causally, while all others behave stubbornly.
Assume that at most \(t\ge 0\) agents behave causally, while all other agents are stubborn. Our goal is to provide a dedicated self-composition of the given FO transition system \({\mathcal {T}}\) which takes care of the particular agent model, while preserving stratification and guardedness of the transition system. In the case that there are at most t causal agents, the informedness predicate \(I\) may receive only finitely many values. These finitely many values, however, can be encoded into the program points of the transformed FO transition system itself. Updates to \(I\) now, however, show up as assumptions at certain control flow edges.
Let \(y_1,\ldots ,y_t\) denote a sequence of t distinct fresh variables. The initial program point of the self-composition \({{{\mathcal {P}}}}^{c,t}_a(T)\) then is given by \(\langle v_0,\emptyset \rangle \), since no causal agent is informed in the beginning. Now consider the substitution \(\theta \) at an edge \(e=(u,\theta ,v)\) of \({\mathcal {T}}\) possibly modifying predicates \(R_1,\ldots ,R_k\). Let \(\theta _0,\ldots ,\theta _r={{{\mathcal {P}}}}^{(c)}_a\theta \) denote the sequence of substitutions of \({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\) meant to simulate \(\theta \), where the last substitution \(\theta _r\) is the update to the predicate \(I\). Let \(u_{e,1},\ldots ,u_{e,r}\) denote the auxiliary nodes introduced by \({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\) for simulating the sequence of substitutions \({{{\mathcal {P}}}}^{(c)}_a\theta \). Let \(Y\subset Y'\subseteq \{y_1,\ldots ,y_t\}\) where Y is the set of informed causal agents before the execution of \(\theta _0,\ldots ,\theta _r\), and \(Y'\) a possible set of causal agents informed afterwards.
First assume that \(\theta \) does not query a choice predicate, i.e., none of the substitutions \(\theta _j\) mentions the predicate \(I\). Then \({{{\mathcal {P}}}}^{c,t}_a({\mathcal {T}})\) has edges
where \({\bar{z}}_j\) are lists of distinct FO variables of appropriate length and \({\bar{z}}\) is an enumeration of all variables occurring in any of the \({\bar{z}}_j\). Assuming that all agents in Y are already informed, the assumption \(g_{Y.Y'}\) implies that at the new node \(\langle v,Y' \rangle \), (at least) all agents from \(Y'\) are informed.
Finally, assume that \(\theta \) is an update querying a choice predicate C. Then the same construction applies — only that in the substitutions \(\theta _0,\ldots ,\theta _{r-1}\) the literals I(x) and \(\lnot I(x)\) must be replaced with the formulas
respectively. The correctness of the transformation can be proven along the same lines as Theorem 10. Theorems 8 and 5 can still be applied, since no assumptions are introduced inside strongly connected components. Therefore, we finally obtain:
Theorem 12
Consider a FO transition system \({\mathcal {T}}\) and declassification formulas satisfying the same assumptions as in theorem 11, and assume that at most \(t\ge 0\) of the agents participating in \({\mathcal {T}}\) are causal, while all other agents are stubborn. Then NDA for \({\mathcal {T}}\) is effectively decidable. \(\square \)
Example 13
Consider again the FO transition system from Fig. 1, but now with causal agents and the self-composition \({{{\mathcal {P}}}}^{(c)}_a({\mathcal {T}})\) where informedness of agents is maintained via the explicit auxiliary predicate \(I\). Interestingly, the fixpoint iteration for proving the invariant (34) still terminates with a rather complicated inductive invariant. The latter, however, is not weak enough to prove NDA. In fact, this property cannot be guaranteed, as is indicated by the following counterexample:
Intuitively, pc member a has declared conflict with paper p, but has been assigned paper \(p'\). Pc member \(a'\) on the other hand, has declared no conflict and has been assigned both papers p and \(p'\). Since pc members \(a,a'\) share a common paper \(p'\) for which both have received a report, they may start a discussion on paper \(p'\). This discussion can be used by \(a'\) to leak secret information on paper p, i.e., depending on the received report on p, \(a'\) may contribute \(d_1\) or \(d_2\) to the discussion of \(p'\). \(\square \)
11 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 subclasses 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 subclasses 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.
In the second part, we applied the obtained termination results to multi-agent systems encoded as FO transition systems. This formalism subsumes the workflow language as considered in [3] for analyzing noninterference in presence of declassification and agent coalitions (NDA). We indicated how NDA can be naturally encoded as a universal invariant of suitably defined self-compositions of the given FO transition systems [27, 28]. At least for the case of stubborn agents [16], i.e., agents who do not participate in adversarial coalitions and for the case where the number of causal agents is bounded, our novel decidability results translate into decidability of NDA.
Acknowledgements
This work was supported by Shota Rustaveli National Science Foundation of Georgia under the project FR-21-7973.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.