Das Kapitel geht der Verifizierung von Lebenseigenschaften in der Logik erster Ordnung nach, einem entscheidenden Aspekt, um sicherzustellen, dass wünschenswertes Verhalten letztlich bei Systemausführungen auftritt. Traditionelle Methoden beruhen auf gut fundierten Rankings, die aufgrund von Beschränkungen bei der Erfassung fundierter und komplexer Ranking-Funktionen schwierig direkt in Logik erster Ordnung auszudrücken sein können. Die Autoren führen das Konzept impliziter Rankings ein, die die Reduktion und Erhaltung von Ranking-Funktionen kodieren, ohne diese explizit zu definieren. Dieser Ansatz überwindet Hindernisse beim Ausdruck wohlfundierter und komplexer Ranking-Funktionen, wie etwa Kardinalitäten von Mengen und Summen über unbegrenzte Bereiche hinweg. Das Kapitel stellt eine Reihe von Konstrukteuren für implizite Rankings vor, die auf vertrauten Vorstellungen aus der Ordnungstheorie beruhen, die instanziiert und zusammengesetzt werden können, um eine reiche Familie impliziter Rankings auszulösen. Diese Konstruktoren sind besonders leistungsstark für endliche, aber unbegrenzte Bereiche, die in verteilten Protokollen und gleichzeitigen Systemen üblich sind. Die Autoren demonstrieren die Wirksamkeit ihres Ansatzes anhand bemerkenswerter Beispiele, darunter die Verifizierung von Dijkstras selbststabilisierenden Protokollen, die die Einfachheit und Effizienz impliziter Rankings in Liveness Proofs aufzeigen. Das Kapitel diskutiert auch verwandte Arbeiten und schließt mit einer Diskussion über das Potenzial zukünftiger Automatisierung und Erweiterungen des impliziten Ranking-Ansatzes.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Liveness properties are traditionally proven using a ranking function that maps system states to some well-founded set. Carrying out such proofs in first-order logic enables automation by SMT solvers. However, reasoning about many natural ranking functions is beyond reach of existing solvers. To address this, we introduce the notion of implicit rankings — first-order formulas that soundly approximate the reduction of some ranking function without defining it explicitly. We provide recursive constructors of implicit rankings that can be instantiated and composed to induce a rich family of implicit rankings. Our constructors use quantifiers to approximate reasoning about useful primitives such as cardinalities of sets and unbounded sums that are not directly expressible in first-order logic. We demonstrate the effectiveness of our implicit rankings by verifying liveness properties of several intricate examples, including Dijkstra’s k-state, 4-state and 3-state self-stabilizing protocols.
1 Introduction
Liveness properties of a system assert that some desirable behavior eventually happens in all executions of the system. The most common approach to proving liveness properties is based on the notion of a well-founded ranking. Such a proof goes by finding a ranking function f from the set of states of the system to some well-founded set \((A, <)\) such that for any transition of the system from state \(s\) to state \(s'\) where the desired behavior does not yet occur, the ranking is reduced, i.e., \(f(s') < f(s)\). Thus, well-foundedness of A ensures that there is no infinite execution that does not eventually satisfy the property.
Many recent works use first-order logic (FOL) for verifying safety and liveness properties [26, 31, 35‐37, 39, 43, 48]. FOL has been established as a useful tool for modeling and verifying systems, mostly due to the success of automatic solvers that answer complicated satisfiability queries in seconds. One challenge that arises when proving liveness properties in FOL is that well-foundedness is not directly expressible in FOL. Additionally, many common primitives that are useful for defining ranking functions, such as cardinality of sets, and sums over unbounded domains, cannot be directly captured in FOL.
Anzeige
We present an approach that overcomes these hurdles and facilitates carrying out proofs based on ranking functions in FOL. Our approach utilizes the observation that it suffices to encode the reduction in the ranking function without explicitly encoding the ranking function itself. Furthermore, the reduction need not be encoded precisely, but can be soundly approximated. For this purpose, we define the notion of an implicit ranking, which can be soundly used in liveness proofs in place of explicit ranking functions. An implicit ranking consists of a reduction formula, \(\varphi _{<}\), and a conservation formula, \(\varphi _{\le }\). These are two-state first-order formulas for which there exists some ranking function f mapping the states to elements of some well-founded set \((A,<)\) such that whenever states s and \(s'\) satisfy \(\varphi _{<}\) we have \(f(s')<f(s)\) and whenever s, \(s'\) satisfy \(\varphi _{\le }\) we have \(f(s') \le f(s)\). Conservation is needed, for example, in proof rules for verifying liveness under fairness assumptions.
We then introduce recursive constructors for implicit rankings that can be instantiated and composed to induce a rich family of implicit rankings. Our constructors are based on familiar notions from order theory, such as pointwise ordering and lexicographic ordering, which can be used to lift and aggregate orders in various ways, adapted to the first-order setting. A key component of our approach is the introduction of domain-based constructors that use quantification over the domain of a state to express aggregation of rankings. For example we can express a pointwise aggregation of given rankings, or a lexicographic aggregation based on a given order on the elements in the domain. When composed, such aggregations can capture complex ranking arguments that are unattainable by existing methods.
Implicit rankings produced by domain-based constructors are sound for finite, albeit unbounded, domains. Such domains are common when reasoning about distributed protocols, concurrent systems, arrays, etc. where the set of nodes, array indices, etc. is finite but not fixed. In fact, liveness of such systems often depends on the finiteness of the domain. Thus, such constructors allow us to utilize finiteness of the domain in liveness proofs, even though finiteness itself is not definable in FOL.
As notable examples, we use our constructors to produce implicit rankings for the self-stabilization property of Dijkstra’s k-state, 4-state and 3-state protocols [13]. In these examples, domain-based constructors are able to replace reasoning about unbounded sums and set cardinalities in novel ways. We use the implicit rankings within a sound proof rule to verify the examples, where the premises of the rule are discharged automatically by an SMT solver. To the best of our knowledge, this is the first SMT-based verification of the more challenging 3-state and 4-state protocols, and it is simpler than existing proofs for such protocols [1, 3, 8, 12, 14, 19, 20, 23, 25, 34].
Anzeige
Contributions.
We define implicit rankings, which soundly approximate reduction and conservation of some ranking function in FOL, and show how these implicit rankings can be used in liveness proofs (Section 4).
We introduce constructors of implicit rankings based on familiar notions from order theory, including domain-based constructors that are sound for finite but unbounded domains and can sometimes replace reasoning about unbounded summations and set cardinalities (Section 5).
We implement the proposed constructors in a tool for verifying liveness properties of first-order transition systems, and demonstrate the power of our constructors by verifying a set of examples of liveness properties, including Dijkstra’s self-stabilizing protocols (Section 6).
In the next section we present two examples that motivate our approach. Section 3 then provides the necessary background for Sections 4 to 6 and Section 7 discusses related work and concludes the paper.
Full Version. The full version of the paper is available at [27].
2 Motivating Examples
Example 1
As a first motivating example (Figure 1), we consider an abstraction of a self-stabilizing protocol. In a self-stabilizing protocol privileges are initially distributed arbitrarily in a network, but eventually the protocol converges to a stable state where only one machine holds a privilege. The protocol we consider abstracts the movement of privileges in Dijkstra’s k-state protocol [13]. While the abstraction does not enjoy stabilization, it suffices for showing a property that is used in the proof of stabilization for Dijkstra’s protocol.
In this protocol, the network consists of a finite number of machines, arranged in a ring, with one machine, called the bottom machine (\(\textsf{bot}\)), being distinguished. Every machine i has a field \(i.\textsf{next}\) which directs to its right-hand neighbor in the ring. At any moment any machine may be privileged or not. Initially, privileges are assigned arbitrarily, with the guarantee that at least one machine is privileged. At each iteration, an arbitrary privileged machine is scheduled, the scheduled machine loses its privilege and its right-hand neighbor becomes privileged (whether it was already privileged or not). The property we wish to prove is that machine \(\textsf{bot}\) is eventually scheduled: \(\lozenge (\textsf{skd}= \textsf{bot})\). In the original protocol, the steps of machine \(\textsf{bot}\) are different from all other machines (this difference is lost in the abstraction) and, in particular, they take the state of the network closer to stabilization.
Next, we describe a ranking function for proving the liveness property. To present the ranking function we denote the number of machines by n and think of the machines as indexed by \(0,1,\ldots ,n-1\) according to their order in the ring, with \(\textsf{bot}=0\). Now, a natural ranking function is: \(\textrm{Rk}=\sum _{i\ne 0 : \textsf{priv}(i)} n-i\). Intuitively, the value \(n-i\) can be seen as the number of steps required for the privilege of machine i to reach machine 0 (if no other privileges are present). We can now verify that in any transition from s to \(s'\), if the eventuality does not occur in either \(s\) or \(s'\), the rank is reduced. Indeed, for any transition, if \(\textsf{skd}= 0\) the eventuality is satisfied in \(s\); otherwise, \(\textsf{skd}\) loses its privilege, decreasing \(\textrm{Rk}\) by \(n-\textsf{skd}\), and \(\textsf{skd}+1\) gains a privilege, (possibly) increasing \(\textrm{Rk}\) by \(n-(\textsf{skd}+1)\), ultimately decreasing \(\textrm{Rk}\) by 1 (or more, if \(\textsf{skd}+1\) was already privileged).
Fig. 1.
Toy Stabilization
Fig. 2.
Binary Counter
While this ranking function is natural, it is not clear how to reason about it with existing automated solvers due to the unbounded sum operation which is not directly expressible in FOL (without induction). Next, we show how we can express this ranking argument in FOL by an implicit ranking which encodes a sound approximation of the reduction in the ranking function. To do this, we show that we can replace reasoning about set cardinalities and unbounded sums by reasoning about other aggregations that are expressible in FOL.
To avoid combining arithmetic reasoning with quantifiers, we use an uninterpreted sort to model the machines, and instead of relying on numbers, we model the ring structure with a strict order on machines, \(\textsf{lt}\), such that \(\textsf{bot}\) is minimal in that order, and the next field corresponds to the successor function in the order \(\textsf{lt}\), except for the maximal element which points to bot.
Now, we observe that in our model, the expression \(n-i\) used in the ranking function above for a privileged machine i is the cardinality of the set of machines that are greater or equal to i in the order \(\textsf{lt}\). Further, we can sum over all machines by pushing the condition on i into the set definition. Thus, \(\textrm{Rk}= \sum _i |\{j : \textsf{priv}(i) \wedge i\ne 0 \wedge (\textsf{lt}(i,j)\vee i=j)\}|\). In order to express reduction in the sum, we recall that in a transition, the summands are unchanged for all machines except for \(\textsf{skd}\), \(\textsf{skd}+1\); the contribution of \(\textsf{skd}+1\) to the sum after the transition is smaller than the contribution of \(\textsf{skd}\) before the transition and the contribution of \(\textsf{skd}\) to the sum after the transition is 0 (because it loses its privilege) and therefore, smaller or equal to that of \(\textsf{skd}+1\) before the transition. Therefore we can use an adaption of a pointwise argument which “permutes” \(\textsf{skd}\) and \(\textsf{skd}+1\) to capture the reduction in the sum over all machines.
Next, we need to express reduction (or conservation) in the summands (either of the same machine i or of different machines) along transitions. The summands are cardinalities of sets of machines j. Thus, we observe that it suffices to show strict set inclusion. This amounts to a pointwise argument over all machines j, showing reduction (or conservation) in the binary predicate \(\alpha (i,j)=\textsf{priv}(i) \wedge i\ne 0 \wedge (\textsf{lt}(i,j)\vee i=j)\) that defines membership of j in the set of i. The reduction in the binary predicate, the pointwise reduction and the permuted-pointwise reduction, can all be encoded in FOL. Thus, the overall approximation of the reduction in the ranking function can be expressed (and hence verified automatically) by the following first-order formula, where unprimed symbols represent the pre-state of a transition and primed variables represent the post-state:
As a second motivating example (Figure 2), we look at a binary counter implemented in an array, taken from [24]. For simplicity of the presentation, we consider a version of the counter that counts down. The counter is implemented by an array \(a[0],\ldots ,a[n-1]\) with \(a[0]\) as the most significant bit and \(a[n-1]\) as the least significant bit, initialized with all 1s. A pointer \(\textsf{ptr}\) traverses the array starting at index \(n-1\) (the lsb) until it sees the first 1, replacing at each step any 0 it sees with a 1. When reaching the first cell with a 1, it sets that cell to a 0 and returns \(\textsf{ptr}\) to index \(n-1\). We wish to prove that eventually the array holds all 0s: \(\lozenge (\forall x. a[x]=0)\).
To find a ranking function, we notice that the reduction in the counter value happens between states of the program where \(\textsf{ptr}=n-1\). Such states partition the execution to “intervals”. For a state inside an interval, we can derive the value of the counter at the beginning of the interval (i.e., when \(\textsf{ptr}\) was last \(n-1\)) by \(a_{\textsf{old}}[i]=0 \iff a[i]=0 \vee i > \textsf{ptr}\). Within an interval, the counter values stored by \(a_{\textsf{old}}\) do not change but \(\textsf{ptr}\) is reduced; and when a new interval starts, the value of \(a_{\textsf{old}}\) is reduced (and \(\textsf{ptr}\) is set back to \(n-1\)). This lends itself to a ranking function in the form of a lexicographic pair \(\textrm{Rk}= (\textrm{val}(a_{\textsf{old}}), \textsf{ptr})\).
Unfortunately, it is not clear how to encode the value of the counter in FOL. In fact, most existing techniques for encoding ranking functions in FOL are limited to polynomial ranking functions, while the counter requires an exponential ranking function. Fortunately, we realize that a reduction in the counter value corresponds to a lexicographic reduction in the sequence of bits stored in the array representing the counter based on the order on array indices.
To encode the ranking argument in FOL we model the indices of the array, as in Example 1, by an uninterpreted index sort and a strict order \(\textsf{lt}\) on it, with the maximal index acting as \(n-1\). The content of the array is modeled using a unary relation \(a(\cdot )\) that records the cells with value 1. Then, \(a_{\textsf{old}}\) is recorded by \(a_{\textsf{old}}(i) =a(i) \wedge (\textsf{lt}(i,\textsf{ptr})\vee i=\textsf{ptr})\). With this encoding, reduction in \(\textsf{ptr}\) is measured by the order on indices \(\textsf{lt}\) and reduction in \(a_{\textsf{old}}\) is measured lexicographically, based on the same order \(\textsf{lt}\) on indices, where for every index i, the values of cell i are ordered by implication on the derived predicate \(a_{\textsf{old}}(i)\). Overall, the reduction in rank can be encoded in FOL by the formula:
Section 4 formally defines the notion of an implicit ranking which the reduction formulas above exemplify. The crux of our work is in Section 5, where we present constructors of implicit rankings. As we show in Section 6, the implicit rankings for both motivating examples can be built using our constructors.
3 Preliminaries
First-Order Logic. We consider uninterpreted FOL with equality, without theories. For simplicity, we present our results for a single-sorted version of FOL. The extension of the results to many-sorted logic, which we use in practice, is natural. A first-order signature \(\varSigma \) contains relation, constant and function symbols. A term t over \(\varSigma \) is a variable x, a constant c, the application of a function on a sequence of terms \(f({\textbf{t}})\) or an if-then-else term \(\textrm{ite}(\alpha ,t_1,t_2)\). Formulas \(\alpha \) over \(\varSigma \) are defined recursively: atomic formulas are either \(t_1=t_2\) or \(r({\textbf{t}})\) where r is a relation symbol. Non-atomic formulas are built using connectives \(\lnot ,\wedge ,\vee ,\rightarrow \) and quantifiers \(\forall ,\exists \). We write \(\alpha ({\mathbf {x_1}},\ldots ,{\mathbf {x_k}})\) to denote that the free variables in \(\alpha \) are contained in \({\mathbf {x_1}}, \ldots ,{\mathbf {x_k}}\). Given sequences of terms \({\mathbf {t_1}},\ldots , {\mathbf {t_k}}\) we then use the notation \(\alpha ({\mathbf {t_1}},\ldots ,{\mathbf {t_k}})\) to denote the formula obtained from \(\alpha \) by substituting each \({\mathbf {x_j}}\) with \({\mathbf {t_j}}\). For a signature \(\varSigma \) we use subscripts and superscripts \(\ddag \) to denote disjoint copies of \(\varSigma \) defined by \(\varSigma \ddag = \{a\ddag \mid a\in \varSigma \}\), assumed to satisfy \(\varSigma \cap \varSigma \ddag = \emptyset \). For a formula \(\alpha \) over \(\varSigma \), we denote by \(\alpha \ddag \) the formula over \(\varSigma \ddag \) obtained by substituting each symbol \(a\in \varSigma \) with \(a\ddag \in \varSigma \ddag \).
First-order formulas are evaluated over pairs of structures and assignments. A structure for \(\varSigma \) is a pair \(s=(\mathcal {D},\mathcal {I})\) where \(\mathcal {D}\) is a non-empty set called the domain, and \(\mathcal {I}\) is an interpretation that maps each relation, constant and function symbol to an appropriate construct over \(\mathcal {D}\). We denote by \(\textrm{struct}(\varSigma ,\mathcal {D})\) the set of all structures over \(\mathcal {D}\). An assignment \(v\) from a sequence of variables \({\textbf{x}}\) to a domain \(\mathcal {D}\) is a function \(v: {\textbf{x}} \rightarrow \mathcal {D}\). We denote the set of all assignments from \({\textbf{x}}\) to \(\mathcal {D}\) by \(\textrm{assign}({\textbf{x}},\mathcal {D})\). We denote the concatenation of two sequences of variables \({\textbf{x}}\), \({\textbf{y}}\) by \({\textbf{x}}{\cdot }{\textbf{y}}\). For two assignments \(u,v\) without shared variables, we denote by \(u{\cdot }v\) the disjoint union of \(u\) and \(v\). We call a pair \((s,v)\) of a structure and an assignment an a-structure. For a domain \(\mathcal {D}\) and a sequence of variables \({\textbf{x}}\) we denote the set of all a-structures by \(\mathrm {a\text{- }struct}(\varSigma ,{\textbf{x}}, \mathcal {D})\). For a formula \(\alpha \) and an a-structure \((s,v)\) we write \((s,v)\models \alpha \) to denote that \((s,v)\) satisfies \(\alpha \).
Transition Systems in First-Order Logic. We consider transition systems given by a first-order specification \(\mathcal {T}= (\varSigma ,\iota ,\tau )\) where \(\varSigma \) is a signature, \(\iota \) is a closed formula over \(\varSigma \) that specifies initial states, and \(\tau \) is a formula over a double signature \(\varSigma \uplus \varSigma '\) that specifies transitions, where the symbols in \(\varSigma \) represent the pre-state and the symbols in \(\varSigma '\) represent the post-state of a transition. A trace of \(\mathcal {T}\) is an infinite sequence of structures \((s_i)_{i=0}^\infty \) over the same domain such that \(s_0\) is an initial state and for all \(i\in \mathbb {N}\), there is a transition from \(s_i\) to \(s_{i+1}\).
Well-Founded Partial Orders. A binary relation \(\le \) on a set A is a partial order if it is reflexive, antisymmetric and transitive. For a partial order we write \(a_1 < a_2\) for \(a_1\le a_2\) and \(a_1 \ne a_2\). A partial order \(\le \) is called well-founded if there is no sequence \(a_0,a_1,\ldots \) such that \(a_{i+1} < a_i\) for all \(i\in \mathbb {N}\). We then refer to \(\le \) as a wfpo for short1. If \(\le \) is a partial order on A and A is finite, then \(\le \) is a wfpo.
4 Expressing Ranking in First-Order Logic
In this section we introduce the notion of implicit ranking. To motivate our definition, we start by considering the way rankings are typically used.
4.1 Using Ranking for Liveness Proofs
Well-founded rankings are useful for proving liveness properties of transition systems. A typical proof rule that uses rankings is based on two notions: a conservation of the ranking, corresponding to \(\le \), and a reduction in the ranking, corresponding to <. As an example, we examine proving liveness properties of the form \(\mathcal {P}= \square \lozenge r \rightarrow \lozenge q\). A transition system \(\mathcal {T}=(\varSigma ,\iota ,\tau )\) satisfies \(\mathcal {P}\) if every trace of \(\mathcal {T}\) that satisfies r infinitely often eventually satisfies q (r can be understood as a fairness assumption). We can prove such a property by finding a ranking function f from states of the system to a set A with a wfpo \(\le \) and a formula \(\phi \), and validating the following premises: (i) \(\iota \wedge \lnot q \rightarrow \phi \) (ii) \(\phi \wedge \tau \wedge \lnot q' \rightarrow \phi '\) (iii) \( \phi \wedge \tau \wedge \lnot q' \rightarrow \varphi _{\le }\) (iv) \(\phi \wedge \tau \wedge \lnot q' \wedge r \rightarrow \varphi _{<}\), where \(\varphi _{\le },\varphi _{<}\) are formulas that encode conservation and reduction of f. (i) and (ii) assert that \(\phi \) holds in all states in a trace as long as q does not hold. (iii) guarantees that in every transition that does not visit q we have conservation of f. (iv) states that in every transition following a visit to r we have a reduction in f. If all premises are valid, r cannot be visited infinitely often without eventually satisfying q, as that would induce an infinitely decreasing chain in f. We use a similar proof rule for more general liveness properties in our evaluation (Section 6).
The structure of the proof rule above reveals that for soundness, \(\varphi _{\le }\) and \(\varphi _{<}\) do not need to precisely capture conservation and reduction in the ranking. Instead, because \(\varphi _{\le },\varphi _{<}\) appear only positively, it suffices that they underapproximate them, such that whenever a pair of states satisfies \(\varphi _{\le }\), the value of f is conserved between them, and whenever a pair of states satisfies \(\varphi _{<}\), the value of f is reduced between them. The implication in the other direction is not needed for soundness. This observation is key for encoding complex ranking arguments in FOL. It allows flexibility in encoding conservation and reduction, which is crucial in cases where these relations (as well as the ranking function itself) are not directly expressible in FOL, but their underapproximations are.
4.2 Implicit Ranking
This section formalizes the notion of an implicit ranking — a pair of formulas \(\varphi _{\le },\varphi _{<}\) which, for every domain \(\mathcal {D}\), encode underapproximations of conservation and reduction of some implicitly defined ranking function on structures with domain \(\mathcal {D}\). For compositionality, we generalize this concept to pairs of a-structures.
Notation. The definition of an implicit ranking uses formulas that reason about a pair of a-structures. To that end, given a signature \(\varSigma \) and a sequence of variables \({\textbf{x}} = ({x_{i}})_{i=1}^m\), we consider a double signature \(\varSigma _0\uplus \varSigma _1\) and two copies of the variables \({\textbf{x}}_b = ({x_{b,i}})_{i=1}^m\) for \(b \in \{0, 1\}\). Intuitively, \(\varSigma _0\) and \({\textbf{x}}_0\) represent a “lower ranked” a-structure and \(\varSigma _1\) and \({\textbf{x}}_1\) represent a “higher ranked” a-structure. For a term t with variables \({\textbf{x}}\), we denote by \(t_b\) the term obtained by substituting \(\varSigma _b\) for \(\varSigma \) and \({\mathbf {x_b}}\) for \({\textbf{x}}\). With abuse of notation, we consider a structure \(s= (\mathcal {D},\mathcal {I})\) for \(\varSigma \) as a structure for \(\varSigma _b\) where \(\mathcal {I}(a_b) = \mathcal {I}(a)\) for every \(a_b \in \varSigma _b\) and an assignment to \({\textbf{x}}\) as an assignment to \({\mathbf {x_b}}\) by defining \(v(x_{b,i}) = v(x_i)\). For a formula \(\varphi \) over \(\varSigma _0\uplus \varSigma _1\) with free variables \({\mathbf {x_0}},{\mathbf {x_1}}\) and a-structures \((s_0,v_0),(s_1,v_1)\in \mathrm {a\text{- }struct}(\varSigma ,{\textbf{x}},\mathcal {D})\), we write \((s_0,v_0),(s_1,v_1)\models \varphi \) to denote satisfaction of \(\varphi \) when for \(b \in \{0,1\}\), the interpretation of \(\varSigma _b\) is taken from \(s_b\), and the assignment to \({\mathbf {x_b}}\) is taken from \(v_b\).
Definition 1
(Implicit Ranking). Let \(\varphi _{\le },{\varphi _{<}}\) be two formulas over \(\varSigma _0\uplus \varSigma _1\). We say that \(\textrm{Rk}=({\varphi _{\le }},{\varphi _{<}})\) is an implicit ranking with parameters \({\textbf{x}}\), if the free variables in \(\varphi _{\le }\) and \(\varphi _{<}\) are confined to \({{\textbf{x}}_0},{\mathbf {x_1}}\) and for any domain \(\mathcal {D}\), there exist a set A, a wfpo \(\le \) on A and a function \(f: \mathrm {a\text{- }struct}(\varSigma ,{\textbf{x}},\mathcal {D}) \rightarrow A\), such that:
For an implicit ranking \(\textrm{Rk}\) and a domain \(\mathcal {D}\), we call \((A,\le )\) a ranking range for \(\mathcal {D}\) and f a ranking function for \(\mathcal {D}\). If \({\textbf{x}}\) is empty, we call \(\textrm{Rk}\) a closed implicit ranking. If the existence of \(A,\le \) and f is ensured only for finite domains \(\mathcal {D}\), we call \(\textrm{Rk}\) an implicit ranking for finite domains.
The formulas \(\varphi _{\le },\varphi _{<}\) encode relations between a-structures, which means that they let us compare specific elements in one state with possibly different elements in another state. Technically, this is achieved by the free variables in \(\varphi _{\le }\) and \(\varphi _{<}\). In proof rules, we only need to compare structures and thus only allow the use of closed implicit rankings. The use of free variables is needed for the construction of these rankings. In Section 5 we introduce constructors that create new implicit rankings from existing rankings, some of which eliminate free variables.
Definition 1 ensures that for each domain \(\mathcal {D}\), the formulas \(\varphi _{\le }\) and \(\varphi _{<}\) underapproximate conservation and reduction of some ranking function over a-structures. The ranking function f and the corresponding ranking range are not explicitly encoded. As explained above, this allows us to find such formulas even if the exact conservation and reduction of f are not readily expressible in FOL. For example, for a function f that maps \(s\) to the number of elements in \(\mathcal {D}\) that satisfy a predicate \(\alpha (x)\), there is no formula that precisely captures the conservation of f, but it can be approximated, say, by the formula \(\forall x. \alpha _0(x)\rightarrow \alpha _1(x)\).
Closed implicit rankings can be used in proof rules such as the one above by substituting \(\varSigma '\) (the post-state signature) for \(\varSigma _0\) and \( \varSigma \) (the pre-state signature) for \(\varSigma _1\). While implicit rankings ensure reduction/conservation in a possibly different function for each domain, they are sound to use as all states along a trace of a transition system share a domain. In the case of implicit rankings for finite domains, soundness is guaranteed for systems where the domain is finite in each trace, but still unbounded.
5 Constructions of Implicit Rankings
We introduce several constructors for implicit rankings, that can be instantiated and composed to create a rich family of implicit rankings. Our constructors essentially encode standard constructions of partial orders. Each constructor has its own arguments, which may themselves be implicit rankings. Some constructors only construct implicit rankings for finite domains. These are called finite-domain constructors. For other constructors, whether the constructed implicit ranking is for arbitrary or finite domains is inherited from the implicit rankings used as arguments for the constructor. We provide the following guarantees.
Theorem 1
All constructors defined in this section are sound in the sense that (i) if the arguments of a constructor satisfy their assumptions, then the output of the constructor is an implicit ranking (for finite domains if the constructor is finite-domain), and (ii) for constructors that receive implicit rankings as arguments, if at least one of the arguments is an implicit ranking for finite domains, so is the constructed implicit ranking.
Due to space considerations we defer soundness proofs to [27]. We give only the crux of the proofs: the definitions of ranking range and ranking function for the constructed implicit ranking given these notions for the arguments of the constructor.
5.1 Base Constructors
We start by introducing two non-recursive constructors, which are used as the base in recursive constructions of implicit rankings.
Binary Constructor. The first constructor we define captures a binary ranking function, mapping each a-structure \((s,v)\) to 0 or 1 (ordered \(0 \le 1\)) by checking whether \((s,v)\) satisfies a formula \(\alpha \). In this case, reduction is obtained if \(\alpha \) holds in the higher-ranked a-structure and does not hold in the lower-ranked a-structure. Conservation also includes the case where \(\alpha \) holds in both or in neither.
Constructor 1
The binary constructor receives a formula \(\alpha ({\textbf{x}})\) over \(\varSigma \). It returns an implicit ranking \(\textrm{Bin}(\alpha )=(\varphi _{\le },\varphi _{<})\) with parameters \({\textbf{x}}\) defined by:
Continuing with Example 1, for \(\alpha (i,j)=\textrm{priv}(i) \wedge \textrm{lt}(i,j)\), \(\textrm{Bin} (\alpha )\) is an implicit ranking with parameters i, j, capturing reduction and conservation in the ranking between a pair of machines \((i_1,j_1)\) in the higher-ranked structure and a potentially different pair \((i_0,j_0)\) in the lower-ranked structure. The need for comparing different pairs in different structures is demonstrated in Example 1.
Position-in-Order Constructor. The second base constructor, which is a finite-domain constructor, utilizes an already existing (possibly derived) partial order in the system itself, building on the observation that a partial order over a finite domain is always well-founded. The order is defined by a single signature formula \(\ell ({\mathbf {y_0}},{\mathbf {y_1}})\), which allows comparing two (tuples of) elements. To guarantee soundness we must verify that \(\ell ({\mathbf {y_0}},{\mathbf {y_1}})\) defines a strict order, and that it is immutable, i.e., does not change between the ranked structures , encoded by:
If \(s_0,s_1\models \textrm{order}(\ell )\) the interpretation of \(\ell \) in \(s_0\) coincides with its interpretation in \(s_1\) and both define a strict partial order on the set \(\textrm{assign}({\textbf{y}},\mathcal {D})\), where \(\mathcal {D}\) is the domain of \(s_0\) and \(s_1\). Then, if \(\mathcal {D}\) is finite, this order is a wfpo. The position-in-order constructor uses \(\ell \) to create an implicit ranking that compares the valuation of the same term (or sequence of terms) \({\textbf{t}}\) in the two structures. The term may include free variables, allowing to compare valuations under different assignments in the two structures. The underlying ranking function maps an a-structure to its interpretation of \(\ell \) together with the valuation it assigns to \({\textbf{t}}\).
Constructor 2
The position-in-order constructor receives a formula \(\ell ({\mathbf {y_0}},{\mathbf {y_1}})\) over \(\varSigma \) and a sequence of terms \({\textbf{t}}({\textbf{y}})\) over \(\varSigma \) with \(|{\textbf{t}}|=|{\textbf{y}}|\). It returns an implicit ranking for finite domains \(\textrm{Pos}({\textbf{t}},\ell )=(\varphi _{\le },\varphi _{<})\) with parameters \({\textbf{y}}\) defined by:
Continuing with Example 2, define \(\ell (i_0,i_1) = \textrm{lt}(i_0,i_1)\), and \(t = \textrm{ptr}\). Then \(\textrm{Pos}(t,\ell )\) is a closed implicit ranking for finite domains, where the ranking is based on the position of the pointer in the different structures.
5.2 Constructors for Aggregation of Finitely Many Rankings
We now present constructors which receive as input a finite number of implicit rankings and create an implicit ranking that mimics aggregation of the underlying ranking ranges and functions. These constructors are based on standard ways to lift partial orders on sets to a partial order on their Cartesian product.
Pointwise Constructor. For partially-ordered sets \(A_1,\ldots ,A_m\) with partial orders \(\le _1,\ldots ,\le _m\) respectively, the pointwise partial order \(\le _{\text {pw}}\) on the set \(A_1\times \cdots \times A_m\) is defined by \((a_1,\ldots ,a_m)\le _{\text {pw}} (b_1,\ldots ,b_m) \iff \bigwedge _i a_i\le _i b_i\). If the orders \(\le _1,\ldots ,\le _m\) are wfpos then so is \(\le _{\text {pw}}\). The following constructor encodes this in FOL to aggregate rankings. A corresponding ranking function is defined by \(f(s,v) = (f_1(s,v),\ldots ,f_m(s,v))\), where \(f_i\) is a ranking function to \(A_i\).
Constructor 3
The pointwise constructor receives implicit rankings \(\textrm{Rk}^i=(\varphi _{\le }^{i},\varphi _{<}^{i})\) for \(i=1,\ldots ,m\), each with parameters \({\textbf{x}}\). It returns an implicit ranking \(\textrm{PW}(\textrm{Rk}^1,\ldots ,\textrm{Rk}^m) = ({\varphi _{\le }},{\varphi _{<}})\) with parameters \({\textbf{x}}\) defined by:
Lexicographic Constructor. A different partial order on \(A=A_1\times \cdots \times A_m\) can be defined by the lexicographic ordering: \((a_1,\ldots ,a_m)\le _{\text {lex}} (b_1,\ldots ,b_m) \iff \bigvee _i (a_i <_i b_i \wedge \bigwedge _{j<i} (a_j \le _j b_j)) \vee (\bigwedge _i a_i \le _i b_i)\). Again, if \(\le _i\) are all wfpos, then so is \(\le _{\text {lex}}\). The Lexicographic Constructor encodes this idea in FOL. A corresponding ranking function is defined as for the pointwise constructor.
Constructor 4
The lexicographic constructor receives implicit rankings \(\textrm{Rk}^i=(\varphi _{\le }^{i},\varphi _{<}^{i})\) for \(i=1,\ldots ,m\), each with parameters \({\textbf{x}}\). It returns an implicit ranking \(\textrm{Lex}(\textrm{Rk}^1,\ldots ,\textrm{Rk}^m) = ({\varphi _{\le }},{\varphi _{<}})\) with parameters \({\textbf{x}}\) defined by:
5.3 Constructors for Domain-Based Aggregations of Rankings
We now turn to present constructors that encode domain-based aggregations of rankings. As demonstrated in Example 1, such aggregations can sometimes replace summations and cardinalities of sets in ranking arguments. These are constructors that receive as input an implicit ranking \((\varphi _{\le },\varphi _{<})\) with parameters \({\textbf{x}}\), partitioned to \({\textbf{x}} = {\textbf{y}} {\cdot }{\textbf{z}}\). and return an implicit ranking with parameters \({\textbf{z}}\), for which the conservation and reduction depend on the aggregation of the results of \(\varphi _{\le }\) and \(\varphi _{<}\) for different values of \({\textbf{y}}\) in the domain. This is established by quantifying over \({\textbf{y}}\). To do so, we use generalizations of the partial-order constructions we saw in Section 5.2 to sets of functions. Due to the nature of these constructions, the soundness of the produced rankings depends on the finiteness of the domain, so these constructors are finite-domain constructors.
Domain-Pointwise Constructor. For a partially-ordered set \((A, \le _A)\) and a set Y, we can lift \(\le _A\) to a pointwise partial order on the set of functions \(Y\rightarrow A\): for any \(a,b\in Y\rightarrow A\) we have \(a\le _{\text {pw}} b \iff \forall y\in Y. a(y)\le _A b(y)\). If the order \(\le _A\) is a wfpo and Y is finite then \(\le _{\text {pw}}\) is a wfpo. In our case the set Y is the set of assignments to \({\textbf{y}}\) over some finite domain. The next constructor encodes this idea in FOL in a straight-forward way: conservation of the aggregated ranking occurs when we have conservation of the input ranking for all values of \({\textbf{y}}\), and reduction is achieved when, additionally, there is some value of \({\textbf{y}}\) for which we have reduction of the input rank. A corresponding ranking function to \(\textrm{assign}({\textbf{y}},\mathcal {D})\rightarrow A\) is defined by \(f(s,v)=\lambda u\in \textrm{assign}({\textbf{y}}, \mathcal {D}). f_A(s,u{\cdot }v)\) where \(f_A\) is a ranking function to A.
Constructor 5
The domain-pointwise constructor receives an implicit ranking \(\textrm{Rk}^\circ =(\varphi _{\le }^{\circ },\varphi _{<}^{\circ })\) with parameters \({\textbf{x}} = {\textbf{y}}{\cdot }{\textbf{z}}\). It returns an implicit ranking for finite domains \(\textrm{DomPW}(\textrm{Rk}^{\circ },{\textbf{y}}) = ({\varphi _{\le }},{\varphi _{<}})\) with parameters \({\textbf{z}}\) defined by:
Next we demonstrate how DomPW can be used to approximate set cardinalities.
Example 5
For a formula with one free variable \(\alpha (x)\), if we take \(\textrm{Rk}^{\circ }=\textrm{Bin}(\alpha )\), the implicit ranking for finite domains \(\textrm{Rk}= \textrm{DomPW}(\textrm{Rk}^{\circ },x)=(\varphi _{\le },\varphi _{<})\) approximates the cardinality of the set of elements that satisfy \(\alpha \): if structures \(s_0,s_1\) are such that \(s_0,s_1\models \varphi _{<}\), we have that the set of elements that satisfy \(\alpha \) in \(s_0\) is a strict subset of that in \(s_1\), and so we have reduction in cardinality. This does not capture cardinality precisely, and we can encode a more precise approximation using Const. 6.
Example 6
Taking \(\textrm{Rk}^{\circ } = \textrm{Bin}(\textrm{priv}(i)\wedge \textrm{lt}(i,j))\) from Example 3, the implicit ranking for finite domains \(\textrm{DomPW}(\textrm{Rk}^\circ ,j)=(\varphi _{\le },\varphi _{<})\) aggregates over j but still has i as a parameter. This lets us compare cardinalities of the sets of machines associated with two different machines described by \(i_0\) and \(i_1\).
Domain Permuted-Pointwise Constructor. The following constructor is a relaxation of Const. 5, based on the notion of a permuted pointwise order, meant to capture cases where two functions are almost pointwise-ordered but some permutation of the inputs is required. For a set Y, a partially-ordered set A, and two functions \(a,b\in Y\rightarrow A\), we say that \(a \le _{\text {perm}} b\) if there exists a bijection \(\sigma \) on Y such that \(a \le _{\text {pw}} b\circ \sigma \). The result, \(\le _{\text {perm}}\), is a preorder on \(Y\rightarrow A\). It induces a partial order on the quotient set of \(Y\rightarrow A\) w.r.t. \(\equiv _{\text {perm}}\) in the usual way. If \((A,\le _A)\) is a wfpo and Y is finite, \(\le _{\text {perm}}\) is a wfpo on the quotient set of \(Y\rightarrow A\) . In our case \(Y = \textrm{assign}({\textbf{y}}, \mathcal {D})\) and a ranking function \(f_A\) to A can be lifted to a ranking function to the quotient set of \(\textrm{assign}({\textbf{y}}, \mathcal {D}) \rightarrow A\) by defining \(f(s,v)= [\lambda u\in \textrm{assign}({\textbf{y}}, \mathcal {D}). f_A(s,u{\cdot }v)]_{\equiv _{\text {perm}}}\).
The above order is not directly first-order definable — we cannot capture the existence of a permutation \(\sigma \) as this would require second order quantification. Instead, the permuted-pointwise constructor under-approximates and encodes only the cases where \(\sigma \) is composed of transpositions of at most a constant number k of pairs of elements \({\mathbf {y^1_{\scriptstyle \rightarrow }}},{\mathbf {y^1_{\scriptstyle \leftarrow }}},\ldots ,{\mathbf {y^k_{{\scriptstyle \rightarrow }}}},{\mathbf {y^k_{\scriptstyle \leftarrow }}}\) as follows: \(\sigma ({\mathbf {y^i_{\scriptstyle \rightarrow }}})={\mathbf {y^i_{\scriptstyle \leftarrow }}}\) and \(\sigma ({\mathbf {y^i_{\scriptstyle \leftarrow }}})={\mathbf {y^i_{\scriptstyle \rightarrow }}}\) for \(i=1,\ldots ,k\) and \(\sigma ({\textbf{y}})={\textbf{y}}\) for any other \({\textbf{y}}\). To ensure that \(\sigma \) is a well-defined permutation we require that for every \(i\ne j\) we have \({{\textbf{y}}^i_{\scriptstyle \rightarrow }}\ne {{\textbf{y}}^j_{\scriptstyle \rightarrow }}\),\({{\textbf{y}}^i_{\scriptstyle \leftarrow }}\ne {{\textbf{y}}^j_{\scriptstyle \leftarrow }} \) and \( {{\textbf{y}}^i_{\scriptstyle \rightarrow }}\ne {{\textbf{y}}^j_{\scriptstyle \leftarrow }}\). We can then capture \(\sigma ({\textbf{y}})\) for any \({\textbf{y}}\) by a term \({\textbf{y}}_\sigma \) (see below), and encode reduction or conservation according to \(\sigma \) by comparing \({\textbf{y}}\) to \({\textbf{y}}_\sigma \) with the input implicit ranking. (Notably, this is the only constructor that uses the input implicit ranking to compare different elements.) While this is only an approximation, we have found it captures several interesting cases, such as the one needed to verify Example 1.
Constructor 6
The domain permuted-pointwise constructor receives an implicit ranking \(\textrm{Rk}^\circ =(\varphi _{\le }^{\circ },\varphi _{<}^{\circ })\) with parameters \({\textbf{x}} = {\textbf{y}}{\cdot }{\textbf{z}}\), and \(k\in \mathbb {N}\). It returns an implicit ranking for finite domains \(\textrm{DomPerm}(\textrm{Rk}^\circ ,{\textbf{y}},k)=({\varphi _{\le }},{\varphi _{<}})\) with parameters \({\textbf{z}}\) defined by:
Next, we demonstrate how DomPerm can approximate sums over unbounded sets and weighted set cardinalities. We expand on the relation to sums in [27].
Example 7
Continuing with Example 6, taking \(\textrm{Rk}^{\circ } = \textrm{DomPW}(\textrm{Bin}(\textrm{priv}(i)\wedge \textrm{lt}(i,j)),j)\), \(\textrm{Rk}= \textrm{DomPerm}(\textrm{Rk}^{\circ },i,1)\) is an implicit ranking that captures the reduction argument described in Example 1. In particular, the aggregation captured by the permuted-pointwise constructor replaces an unbounded summation. The reduction formula listed in Example 1 is slightly simplified compared to \(\textrm{Rk}\) produced by \(\textrm{DomPerm}\) above: it includes only the nontrivial disjuncts of the \(\textrm{ite}\) expressions, and it uses \(\textrm{skd},\textrm{skd}+1\) in place of the existential quantifier.
Example 8
Consider a ranking function \(|\{x\mid \alpha (x)\}|+2|\{x\mid \beta (x)\}|\), where \(\alpha \) and \(\beta \) are two predicates, and consider the case where conservation of ranking between states \(s_0,s_1\) holds due to ‘mixing’ of the predicates, for example “exchanging” one element \(x^0\) that satisfies \(\beta \) in \(s_0\) with two elements \(x^1,x^2\) that satisfy \(\alpha \) in \(s_1\). We can use the DomPerm constructor to capture such a ranking argument. We first add to the signature of the transition system an enumerated sort type with three values: \(\textrm{type}_\alpha ,\textrm{type}_\beta ^1,\textrm{type}_\beta ^2\). We then define the unified predicate \(\gamma (x,ty)=(ty=\textrm{type}_\alpha \wedge \alpha (x))\vee ( (ty=\textrm{type}_\beta ^1 \vee ty=\textrm{type}_\beta ^2 )\wedge \beta (x) )\). This can be understood as introducing one copy of the domain for \(\alpha \) and two copies for \(\beta \), and interpreting each of \(\alpha \) and \(\beta \) over the copies relevant to them. Finally, we consider \(\textrm{Rk}= \textrm{DomPerm}(\textrm{Bin}(\gamma ),(x,ty),2)=(\varphi _{\le },\varphi _{<})\). To see that the aforementioned pair of states indeed satisfies the resulting conservation formula, i.e., \((s_0,s_1)\models \varphi _{\le }\), consider the permutation defined by \({\mathbf {y^1_{\scriptstyle \leftarrow }}}=(x^0,\textrm{type}^1_\beta ), {\mathbf {y^2_{\scriptstyle \leftarrow }}}=(x^0,\textrm{type}^2_\beta ), {\mathbf {y^1_{\scriptstyle \rightarrow }}}=(x^1,\textrm{type}_\alpha ), {\mathbf {y^2_{\scriptstyle \rightarrow }}}=(x^2,\textrm{type}_\alpha )\).
Remark 1
Our decision to focus on permutations obtained by transpositions in our first-order encoding was motivated by examples such as Example 8. There are of course other classes of permutations that can be encoded in first-order logic and would also result in a sound approximation of \(\le _{\text {perm}}\).
Note that Const. 5 (domain-pointwise) can be understood as a special case of Const. 6 obtained by considering the degenerate case \(k=0\).
Domain-Lexicographic Constructor. The following constructor is an analog of Const. 4, where instead of aggregation based on the order of indices of the given rankings, we aggregate based on a partial order on \(\textrm{assign}({\textbf{y}},\mathcal {D})\). To that end we rely on an already-existing order in the system, encoded by a single signature formula \(\ell ({\mathbf {y_0}},{\mathbf {y_1}})\), and axiomatized as in Const. 2.
For a partially-ordered set A with a partial order \(\le _A\) and a set Y with a wfpo \(\le _Y\), the set of functions \(Y\rightarrow A\) can be ordered by the lexicographic partial order: for any \(a,b\in Y\rightarrow A\) we have \(a\le _{\text {lex}}~b \iff a(y) \le _A b(y)\) for all minimal elements of the set \(\{y\in Y \mid a(y)\ne b(y)\}\) (for \(a\ne b\), this set is not empty, because \(\le _{Y}\) is a wfpo). Equivalently, for every \(y\in Y\) such that \(a(y)\not \le _A b(y)\) there exists \(y^*\) such that \(y^* <_Y y\) with \(a(y^*) <_A b(y^*)\). Additionally, if \(\le _A\) is a wfpo and Y is finite, \(\le _{\text {lex}}\) is a wfpo. The constructor encodes this in a straight-forward way: the set Y is \(\textrm{assign}({\textbf{y}}, \mathcal {D})\) and \(<_Y\) is given by \(\ell \). A corresponding ranking function can be defined by the interpretation of \(\ell \) as in Const. 2 combined with \(\lambda u\in \textrm{assign}({\textbf{y}}, \mathcal {D}). f_A(s,u{\cdot }v)\) as in Const. 5.
Constructor 7
The domain-lexicographic constructor receives an implicit ranking \(\textrm{Rk}^\circ =(\varphi _{\le }^{\circ },\varphi _{<}^{\circ })\) with parameters \({\textbf{x}} = {\textbf{y}}{\cdot }{\textbf{z}}\), and a formula \(\ell ({\mathbf {y_0}},{\mathbf {y_1}})\) over \(\varSigma \). It returns an implicit ranking for finite domains \(\textrm{DomLex}(\textrm{Rk}^\circ ,{\textbf{y}}, \ell )=({\varphi _{\le }},{\varphi _{<}})\) with parameters \({\textbf{z}}\) defined by:
Continuing with Example 2, define a formula \(\alpha (i)\) which is set to true if the array holds a 1 in index i, and take \(\textrm{Rk}^{\circ } = \textrm{Bin}(\alpha )\). Take, as in Example 4, \(\ell (i_0,i_1) = \textrm{lt}(i_0,i_1)\). Then, \(\textrm{Rk}= \textrm{DomLex}(\textrm{Rk}^{\circ },i,\ell )\) captures lexicographic reduction of values in the array, akin to reduction in a binary counter. Compared to the formula given above, the reduction formula in Example 2 is simplified by the fact that the order given by \(\ell \) is total, which need not be the case in general.
Note that Const. 5 (domain-pointwise) can be understood as a special case of Const. 7 obtained by considering the degenerate case \(\ell ({\mathbf {y_0}},{\mathbf {y_1}}) = \textrm{false}\).
6 Implementation and Evaluation
To explore the power of the implicit rankings defined by our constructors we implemented a deductive verification procedure for liveness properties of the form \((\bigwedge _i \forall {\textbf{x}}. \square \lozenge r_i(\textbf{x})) \rightarrow \square (p \rightarrow \lozenge q)\) where \(r_i\) are parameterized fairness assumptions, based on a proof rule given in [27]. Our implementation, available at [28], is based on the Z3 [32] Python API. It takes as input a first-order transition system, a liveness property, a closed implicit ranking defined using the constructors of Section 5 and the other formulas required for applying the proof rule. Given the above, we automatically construct the implicit ranking formulas \(\varphi _{<},\varphi _{\le }\) defined by the constructors and use Z3 to validate the premises of the rule. Some of the domain-based constructors create formulas with quantifier alternations, which may be challenging for solvers. We thus allow the user to provide hint terms for the existential quantifiers in the declaration of such constructors. We replace the existential quantification with disjunction over formulas substituted with these terms in the solver queries (this is sound since the implicit ranking formulas appear only positively in the proof rule and in recursive constructors).
Results. We evaluate our tool on a suite of examples from previous works, listed below. We use Z3 version 4.12.2.0, run on a laptop running Windows with a Core-i7 2.8 GHz CPU. All examples are successfully verified within 10 minutes. Below we describe the examples. For each, we note whether the validation of the premises required user-provided hint terms for the existential quantifiers introduced by the constructors. In all examples we use finite-domain constructors, which assume a finite (but unbounded) semantics for the domain of the relevant sorts. In some examples, such as our two motivating examples, there are no fairness assumptions, in which case we use \(\square \lozenge \textrm{true}\) as a fairness assumption; this amounts to assuming totality of the transition relation, which indeed holds in these examples. Some of the more complicated examples additionally require some abstraction techniques. We expand more on each example and these technical details in the full version of the paper [27].
Toy Stabilization (Example 1). The ranking argument described in Section 2 is captured by an implicit ranking defined by DomPerm(DomPW(Bin)).
Binary Counter (Example 2). The ranking argument described in Section 2 is captured by an implicit ranking defined using Lex(DomLex(Bin),Pos).
Token Ring. A mutual exclusion protocol [15] where a token moves around a ring, allowing its holder to enter the critical section. We show that every machine that tries to enter the critical section eventually does. We use an implicit ranking defined by DomLex(Lex(Bin,Bin,Bin)) capturing the linear movement of the token along the ring and changes in local state of the token’s holder.
Leader Ring. The Chang-Roberts algorithm for leader election in a ring [5], with first-order modeling and invariants based on [17, 38]. The liveness property is that eventually a leader is elected. We use an implicit ranking defined by Lex(DomPW(Bin),DomLex(Bin)), where DomPW(Bin) is used to track the cardinality of the set of machines that did not yet send their id, and DomLex(Bin) tracks the movement of messages around the ring.
SAT Backtracking. We verify termination of a naive backtracking search algorithm for solving boolean satisfiability. The implicit ranking is given by Lex(DomLex(Bin),PW(DomPW(Bin),DomPW(Bin))) keeping track of the current assignment that is reduced lexicographically when we change assignment, and the number of steps required until progressing to the next assignment which corresponds to the number of variables that are yet to be assigned true, and those that are yet to be assigned false.
SAT Backjumping. Termination of an abstraction of the CDCL algorithm for solving boolean satisfiability [2, 30], taken from [33]. The algorithm non-deterministically applies decisions, unit propagations, backjumping and learning. We use an implicit ranking, based on the proof in [33] defined by \(\mathrm {Lex(\textrm{Rk}^1,\textrm{Rk}^2)}\) where \(\textrm{Rk}^1 = \mathrm {DomLex(DomPW(Bin)))}\) tracks for each decision level the number of assignments made in it, and \(\textrm{Rk}^2 = \mathrm {DomPW(Bin)}\) tracks the number of assigned variables.
Self-Stabilization Protocols. We verify several self-stabilizing protocols [13]. In these protocols, a set of machines is organized in a line/ring. Each machine holds some local value(s). Privileges are assigned to machines according to relations between a machine’s values and its neighbors’ values. In every transition a privileged machine changes its local values, such that it loses its privilege and a new privilege may be created for one of its neighbors. The protocols differ in how the privileges are defined and updated. For each protocol we show that eventually a unique privilege is present (stabilization) and that starting with a unique privilege, every machine gets a privilege infinitely often (fairness).
Dijkstra’s k-State Protocol. In this protocol a designated machine \(\textrm{bot}\) can introduce new values into the ring. We prove stabilization by proving three lemmas (based on [19, 23]): (1) machine \(\textrm{bot}\) is eventually scheduled, (2) if \(\textrm{bot}\) is scheduled infinitely often then eventually \(\textrm{bot}\) holds a unique value in the ring and (3) if \(\textrm{bot}\) holds a unique value in the ring eventually there is a unique privilege in the ring. The implicit ranking required for properties (1) and (3) is the same and has structure DomLex(Bin), tracking the movement of privileges towards \(\textrm{bot}\) according to the ring order. The implicit ranking for property (2) has structure DomPW(Bin), aggregating over values to capture the distance between \(\textrm{bot}\)’s value and a new value. Fairness is proven similarly to (1).
Dijkstra’s 4-State Protocol. In this protocol two kinds of privileges can be derived for every machine. The different privileges move in different directions. We base our proof on [12]. The implicit ranking for proving stabilization is given by a lexicographic pair \(\textrm{Lex}(\textrm{Rk}^1,\textrm{Rk}^2)\) where \(\textrm{Rk}^1\) has structure DomPerm(Bin), capturing the number of privileges of both kinds. \(\textrm{Rk}^2\) has structure DomPerm(PW(DomPW(Bin),DomPW(Bin))) which captures a bound on the number of moves required from all machines until a privilege is lost. For this implicit ranking we used simple hint terms as described above, replacing existential quantification with instantiation of \(\textrm{skd},\mathrm {skd.next}\) or \(\mathrm {skd.prev}\). The structure of implicit ranking we use for fairness is \(\textrm{Lex}(\textrm{Rk}^1,\textrm{Rk}^2,\textrm{Rk}^3)\) with each \(\textrm{Rk}^i\) tracking a movement of some privilege in some direction using \(\mathrm {DomLex(Bin)}\).
Ghosh’s 4-State Protocol. A simplification of Dijkstra’s 4-state protocol [20]. The implicit ranking we use is an appropriate modification of the above.
Dijkstra’s 3-State Protocol. The implicit ranking we use for proving stabilization is a direct encoding of the ranking function given in [25] (See also [14]) This ranking is a 4-argument lexicographic ranking \(\textrm{Lex}(a,b,c,d)\). a captures a weighted sum of set cardinalities by \(\textrm{DomPerm}(\textrm{Bin})\) with \(k=4\) as in Example 8. This generates premises with 18 existential quantifiers requiring complicated hints to validate. b and c are \(\textrm{DomPerm}(\textrm{Bin})\) capturing set cardinalities and d captures the number of steps until reduction in either a, b, or c, encoded using composition of DomPerm and DomPW. The ranking for fairness is similar.
7 Related Work and Concluding Remarks
Numerous approaches for liveness verification have been proposed in the literature, including abstraction techniques [6, 23], liveness to safety reductions [4, 10, 35, 36], rich proof structures [11, 16, 39, 47], and more [21, 42]. Our work considers verification based on the classical notion of ranking functions [18, 44]. Many proof rules based on ranking functions have been suggested, e,g., [7, 15, 29, 31, 41]. As explained in Section 4.1, our constructions of implicit rankings can be used in any rule that requires conservation and reduction of rank. In contrast to [9, 22, 40, 45, 46, 48] which automate the search for ranking functions, we focus on expanding the class of ranking functions that can be used and leave automation for future work. We now turn to expand on the most relevant recent works.
The closest work to ours is [31], which uses relational rankings or fixed-size lexicographic tuples of them as ranking functions in liveness proofs for first-order transition systems. Relational rankings count the number of elements that satisfy some predicate, and their reduction and conservation are measured approximately in a pointwise fashion. Relational rankings can be captured by our constructors, specifically \(\textrm{DomPW}(\textrm{Bin})\), but our constructors induce a richer family of rankings and offer more expressiveness, sometimes, at the expense of more complex quantifier structure. On the other hand, [31] does not assume finiteness, but proves that the set considered is finite at any time. Generalizing our finite-domain constructors to this setting is not trivial, and is a subject for future work. The proof rule of [31] also allows modular temporal reasoning. The definition of implicit ranking we offer can also be used in such a proof rule.
The approach of [48] focuses on automating the search for a ranking function for protocols modeled in FOL. They automatically synthesize integer-valued polynomial ranking functions from integer variables that appear in the protocol specification, fairness variables and cardinalities of sets defined by predicates (some of which are user-provided). Similarly to our domain-based aggregations, they assume finiteness of certain domains. While we use the assumption implicitly, they introduce integer variables that bound the finite cardinalities. In both [31] and [48], only rankings that are polynomial in the cardinality of the domain can be used, which cannot capture Example 2. Additionally, their domain-based aggregations, which are limited to cardinalities of sets, cannot be recursively composed, which is needed for examples such as Example 1.
The approach of [35, 36] is based on a liveness-to-safety reduction that uses a dynamic finite abstraction to reduce liveness to acyclicity of traces. The reduction is encoded via a monitor that augments the original system. Liveness is established by showing an arbitrary monitored state called the saved state is never revisited. While very general, the approach is difficult to use since one has to find an invariant of the augmented system that justifies that the current state is never equal to the saved state. Our implicit rankings can be understood as a natural way to describe such two-state invariants instead of reasoning about an augmented system. This also makes them more amenable to automation.
Acknowledgement
We thank Neta Elad and Eden Frenkel for helpful discussions. The research leading to these results has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [759102-SVIS]). This research was partially supported by the Israeli Science Foundation (ISF) grant No. 2117/23.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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 license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license 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.
This is a different (weaker) notion from a partial-well-order (an antisymmetric well-quasi-order), which requires no infinite decreasing chains and no infinite antichains.
