Infinite Descent ist eine zentrale Lebendigkeit-Eigenschaft, die bei der Softwareverifikation verwendet wird, insbesondere bei der Sicherstellung der Programmbeendigung und dem Nachdenken über induktive Eigenschaften. Das Kapitel untersucht die Herausforderungen und Komplexitäten der Verifizierung von Infinite Descent, wobei seine Bedeutung in verschiedenen Verifikationsrahmen und -werkzeugen hervorgehoben wird. Es stellt Cyclone vor, ein hochmodernes Werkzeug, das entwickelt wurde, um die Effizienz der Infinite Descent-Verifikation zu steigern. Zyklon nutzt einen heterogenen Ansatz, der Semi-Entscheidungsverfahren kombiniert, die strukturelle Eigenschaften von geneigten Diagrammen ausnutzen, die abstrakte Darstellung von Infinite Descent-Problemen. Das Kapitel befasst sich mit der Entwicklung dreier neuartiger Algorithmen innerhalb von Cyclone: Trace Manifold, Flat Cycles und Descending Unicycles, die jeweils einzigartige Vorteile hinsichtlich Laufzeit und Abdeckung bieten. Die Leistung von Cyclone wird streng nach dem neuesten Stand der Technik bewertet und zeigt deutliche Laufzeitverbesserungen, manchmal um mehrere Größenordnungen. Das Kapitel behandelt auch die Integration von Cyclone in das Cyclist Prover Framework und seine potenziellen Anwendungen in realen Szenarien, die den Weg für effizientere und effektivere Software-Verifikationsprozesse ebnen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
The Infinite Descent property underpins key verification techniques, such as size-change program termination and cyclic proofs. Deciding whether the Infinite Descent property holds of a given program or cyclic deduction is PSPACE-complete, with several exponential time algorithms in the literature. In this paper, we consider algorithms with better time complexity but which are (necessarily) incomplete. Concretely, we formulate and evaluate a number of alternative algorithms for semi-deciding Infinite Descent. Our aim is to improve average runtime performance by utilising more efficient algorithms for specific subclasses of input. We present Cyclone, a tool integrating these algorithms with an existing (complete) decision procedure. We evaluate Cyclone on a large suite of examples harvested from the Cyclist theorem prover, finding that the incomplete algorithms achieve extremely high coverage and afford substantial runtime improvement in practice. We thus believe that the Cyclone tool will foster broader adoption of techniques based on Infinite Descent and expand their practical applications.
1 Introduction
Infinite Descent is an \(\omega \)-regular liveness property that has important practical applications in the verification of software. For instance, it underpins the size-change framework for checking program termination [15], in which a program’s call-graph is used to produce an abstraction recording when the values manipulated by the program (e.g. numbers) decrease as they are passed between function calls. Infinite Descent then states that along all infinite paths through this call-graph, we can trace a value that (strictly) decreases infinitely often. If the call-graph satisfies this property then we know the program must terminate, since the order used to interpret the decrease of values is well-founded. This technique is used, for example, in the termination checker for the Agda proof assistant [1].
Infinite Descent also plays a crucial role in cyclic proof-theoretical techniques for reasoning about inductive (and coinductive) properties [6, 9‐12, 21, 23]. Instead of using inference rules in which a (co)inductive invariant must be explicitly provided, the invariants can be ‘discovered’ by repeatedly decomposing a goal into subgoals that are either provable or reducible back to the original goal, forming a cycle in the proof. The Infinite Descent condition is then used to justify the soundness of such a cyclic proof graph. In proof-theoretic settings, the notion of ‘decrease’ is usually called ‘progress’, and commonly corresponds to particular logic-specific steps that ‘unfold’ instances of (co)inductive definitions.
Fig. 1.
A cyclic proof that every natural number is either even or odd. The blue trace witnesses the Infinite Descent, with progress marked by the blue circle.
Anzeige
For example, Fig. 1 shows a cyclic proof of the fact that every natural number is either even or odd, in a system for first-order logic with inductive predicates. The natural numbers predicate \(N\) is (inductively) defined via the rules \(N(0)\) and \(N(s(x)) \Leftarrow N(x)\) (where s stands for the successor). The predicates \(E\) and \(O\) denote even and odd numbers, respectively, and are mutually defined via the rules \(E(0)\), \(O(s(x)) \Leftarrow E(x)\) and \(E(s(x)) \Leftarrow O(x)\). The
rule performs a case split on the predicate instance \(N(x)\), guided by the defining rules for \(N\), which substitutes \(0\) and \(s(y)\) for \(x\) in the left- and right-hand premises, respectively. In the latter, \(y\) is a fresh variable (denoting the predecessor of \(x\)) for which we know from the definition of \(N\) that \(N(y)\) must hold. The other steps of the proof unfold the \(E\) and \(O\) predicate instances, and perform substitutions. A cyclic proof has the structure of a tree with ‘backlinks’, i.e. a tree in which some of the leaves (called buds) have an edge to another node (called its companion). In Fig. 1, node 6 is a bud whose companion is (the syntactically equal) node 1. When all buds link to an ancestor node (as in this case), the proof is said to be (in) cycle normal (form). However, this need not be the case in general. The proof satisfies the Infinite Descent property since along the infinite path traversing the cycle, we can trace a value (the instances of the \(N\) predicate) that progresses (i.e. is unfolded by the
rule) infinitely often.
This kind of cyclic reasoning has been employed widely to create both theoretical frameworks for program verification and inductive theorem proving (e.g., [3, 4, 17, 20, 24, 25, 27]), as well the Cypress program synthesis tool [13] and the automatic theorem provers Cyclist [5], Songbird [7], Inductor [22] and CycleQ [14]. Since the problem of deciding the Infinite Descent property is PSPACE-complete [15, 18], in practice these tools all implement one of a number of known algorithms that have worst-case exponential runtimes [8]. Although this worst-case performance is not often encountered ‘in the wild’, these tools still rely on deciding large numbers of problem instances. Therefore any speed up of the Infinite Descent check has the potential to provide significant benefits in practice.
Our goal is to advance the state-of-the-art for deciding Infinite Descent and thus push forward the practical use of automated cyclic reasoning and termination checking. Our approach is to identify more efficient algorithms that only semi-(co)decide Infinite Descent, along with (efficiently decidable) characterisations of the subclass of instances on which they may return a definite answer. The idea is that, since they do not need to uniformly treat all problem instances, these algorithms may utilise particular structure in the input to return an answer more quickly than the full decision procedures. We then heuristically combine these semi-decision procedures into a heterogeneous pipeline, defaulting to a uniform decision procedure in case none of them can return an answer.
In this paper we describe three such algorithms. The first decides an existing criterion, proposed by Brotherston [2], called the Trace Manifold condition. The other two decide novel criteria that we have formulated and call “Flat Cycles” and “Descending Unicycles”, respectively. We analyse the coverage of these algorithms by harvesting a large database of problem instances generated by the test suites of the Cyclist theorem prover, which comprise inductive entailments of First-Order Logic and Separation Logic. Guided by the analysis of these algorithms, we combine and implement them within a new tool dubbed Cyclone [19], which we integrate into Cyclist. We present an evaluation of our tool’s performance on our harvested database, comparing it to the performance of the existing decision procedures. We found that Cyclone demonstrates significant runtime improvements, sometimes of several orders of magnitude.
Anzeige
Paper Outline. Sec. 2 formally defines the Infinite Descent problem, in a general form, and sumarises the existing decision procedures. Sec. 3 describes the database of problem instances that we harvested for evaluating our new algorithms. Sec. 4 then describes our novel semi-decision procedures. In Sec. 5 we present the implementation of our tool, Cyclone, and compare its performance to the existing methods implemented in Cyclist. Finally, Sec. 6 concludes.
2 Infinite Descent for Sloped Graphs
We begin by formally defining the Infinite Descent property in the abstract setting of sloped graphs, following [8], which captures the essence of the Infinite Descent problem in an application-independent way. That is, the formulation of Infinite Descent in size-change termination, or some given cyclic logical proof system, are special instances of the abstract definition we give here.
Infinite Descent tracks the ordering relationship between (abstract) values along paths in a graph. The following definition of sloped graphs thus augments the standard notion of a directed graph by associating with each node, or vertex, a collection of abstract positions, and with each edge a relation assigning (flat or downward) slopes between the positions associated with its end-points.
(Sloped graphs). We assume a set \(\textsf{Pos}\) of positions and a set
of slopes, whose elements are called flat and downward, respectively.
A sloped relation\(R\subseteq \textsf{Pos}\times \textsf{Pos}\times \textsf{S}\) is a partial function from pairs of positions to slopes.
A sloped graph\(SG\) is a tuple \((V,E,Ps,(R_{v,v'})_{(v,v') \in E})\) such that:
(1)
(V, E) is a directed graph with nodes \(V\) and edges \(E\);
(2)
\(Ps: V \rightarrow \wp (\textsf{Pos})\) is a function assigning a set of positions to every node;
(3)
\((R_{v,v'})_{(v,v') \in E}\) is a family of sloped relations \(R_{v,v'} \subseteq Ps(v) \times Ps(v') \times \textsf{S}\) indexed by edges.
We call the quantity \(\max {\{|Ps(v)| \mid v\in V\}}\) the (vertex) width of \(SG\).
Example 1
The cyclic proof shown in Fig. 1 can be abstracted by the sloped graph \(SG= (V,E,Ps,(R_{v,v'})_{(v,v') \in E})\) defined as follows, and depicted in Fig. 2, where we use inductive predicate instances as positions.
Since a sloped graph is a form of directed graph, we also adopt the graph-theoretic notions of (finite and infinite) paths through the graph, which we denote by \((v_i)_{i < \alpha }\) where \(\alpha \le \omega \) is (the ordinal that is) the length of the path.
A trace along a path in a sloped graph selects a position from each node in the path, making sure that each position is related to the next by the sloped relations associated with the edges that are traversed.
Definition 2
(Traces). A trace along a (possibly infinite) path \((v_i)_{i < \alpha }\) in a sloped graph \(SG= (V, E, Ps, (R_{v,v'})_{(v,v') \in E})\) is a (possibly infinite) sequence of positions \(\tau = (p_i)_{i < \alpha }\) such that, for every \(i < \alpha \), both \(p_{i} \in Ps(v_{i})\) and \(R_{v_{i},v_{i+1}} (p_{i},p_{i+1},s)\) for some (necessarily unique) slope \(s\). When
we call \(i\)a progressing point in the trace. We may also write \(\tau (v_i)\) to denote the \(i\)th position, \(p_i\). A trace is decreasing if it has infinitely many progressing points. An infinite path is descending if it has a tail along which there is a decreasing trace.
Definition 3
(Infinite Descent). A sloped graph is said to satisfy Infinite Descent if all of its infinite paths are descending.
The problem of deciding whether a given sloped graph satisfies Infinite Descent is PSPACE-complete [15, 18]. There are two basic approaches for deciding the Infinite Descent property described in the literature.
Automata-theoretic: One approach is to encode the problem as an inclusion between \(\omega \)-automata: a ‘path’ automaton that recognises words corresponding to all infinite paths in the sloped graph and a ‘trace’ automaton that recognises words corresponding to all potential descending traces. A sloped graph satisfies Infinite Descent if and only if the former automaton is included in the latter. The problem can be encoded using \(\omega \)-words over either the vertices or the sloped relations of the sloped graph. We call these encodings the Vertex-Language Automata (VLA) and the Slope-Language Automata (SLA) encodings, respectively.
Ramsey-theoretic: An alternative approach is to compute for each pair of nodes the collection of sloped relations consisting of the compositions of the sloped relations along (finite) paths between the two nodes, with slopes combined according to the ordering
. Once this ‘composition closure’ is computed, checking Infinite Descent amounts to verifying the presence of certain downward slopes in the relations representing loops in the sloped graph. This encoding is an instance of the algebraic path problem and can be solved using the Floyd-Warshall-Kleene (FWK) algorithm [16]. By taking advantage of the specific symmetric nature of the Infinite Descent setting, a so-called order-reduced (OR) optimisation of this procedure is possible [8].
Table 1.
Time complexity bounds for Infinite Descent decision procedures
All of these algorithms exhibit exponential worst-case runtime, but the complexity profile of each method depends, in varying proportions, on two parameters of the sloped graph: the number of nodes \(n\), and the vertex width w. The worst-case complexity bounds are summarised in Table 1. A comprehensive account of these methods and their comparative performance can be found in [8].
3 A Database of Sloped Graphs
In order to support our goal of identifying useful classes of sloped graphs for which Infinite Descent can be (semi-)decided (more) efficiently, we generated a large database of sloped graphs using the Cyclist automated theorem prover [5], which we believe to be representative of problem instances arising in real-world applications. Cyclist implements a generic engine for cyclic proof search, supporting arbitrary (cyclic) logical systems by exposing an API to this engine. It currently features a number of logics with inductively defined predicates, including first-order logic (FOL) and Separation Logic (SL), which come with test suites of representative (valid and invalid) logical entailments. During a search for a cyclic proof of a given entailment, Cyclist runs the Infinite Descent check for each intermediate (partial) candidate proof it encounters. We modified Cyclist to output a JSON representation of the corresponding sloped graphs. (Note that Cyclist also employs a preprocessing procedure for minimizing the proof graphs, which we discuss in Sec. 5.2.)
Table 2.
Aggregated numbers of sloped graphs in our database
Dummy
Fig. 3.
Distribution of various sloped graph metrics
In total, we collected over 77,000 sloped graphs. Table 2 shows the numbers of sloped graphs aggregated by the logic they were generated from and whether or not they satisfy Infinite Descent. We also collated statistics pertaining to various metrics of sloped graphs, namely the number of nodes, edges, buds, and vertex width. Again aggregated by the logic, Fig. 3 shows the density functions of these metrics. Across the database, per graph, the number of nodes is at most 107 and the number of edges is at most 120, with graphs most frequently having around 20 nodes/edges. Additionally, graphs have a vertex width of at most 17, with the most frequent quantity being around 8. We see a maximum of 16 buds in any graph, with most of the graphs having around 2 buds. We observe that the vertex width is not particularly correlated with the number of edges/nodes and, in general, the width is low compared to the number of nodes. In contrast, in both test suites, we can see a high correlation between the number of nodes and edges with the two metrics being almost identical. We also see that, in general, the more nodes/edges in a graph, the more buds. However, the number of buds is generally much lower than the number of nodes. This is not surprising given that the graphs are (proof) trees with (few) backlinks, rather than generally highly connected graphs.
4 Effective Semi-algorithms for Infinite Descent
We now present the novel (incomplete) semi-decision procedures that we developed. Concretely we present the following heuristics, analysing their runtime complexity and coverage (the number of graphs in our database for which it returns a definitive answer, i.e. “yes” or “no”):
Trace Manifold (TM): a criterion from [2], for which we provide a novel algorithm and implementation. This heuristic returns “yes”/“don’t know”.
Flat Cycles (FC): a novel criterion based on the notion of a flat projection of a sloped graph. This heuristic returns “no”/“don’t know”.
Descending Unicycles (DU): a novel criterion based on non-overlapping cycles in a sloped graph. This heuristic returns “yes”/“no”/“don’t know”.
We began by implementing the Trace Manifold criterion, but we found the coverage of this method on our database to be very low. This prompted us to formulate the other two criteria, which have better runtime complexity and verify Infinite Descent on a much larger class of sloped graphs.
4.1 The Trace Manifold Criterion
The Trace Manifold criterion (TM) is a property of basic cycles in a sloped graph, \(SG\), that is a cycle normal tree with backlinks. In such graphs, a basic cycle can be identified with a bud \(B\), being the unique path in the graph leading to \(B\) from its companion, denoted \(\mathcal {R}(B)\). A structural connectivity relation, \(\le _{SG}\), over the buds can also be defined by relating two buds \(B_1\) and \(B_2\) precisely when \(\mathcal {R}(B_1)\) lies along the basic cycle associated with \(B_2\).
A trace manifold comprises a set of traces for basic cycles.
Definition 4
(Trace Manifold). A set of (finite) traces is a trace manifold for a sloped graph \(SG= (V, E, Ps, (R_{v,v'})_{(v,v') \in E})\) when it is of the form
$$\begin{aligned}\begin{gathered} \{ \tau _{S,B} \mid \text {S a strongly connected subgraph of }SG, B\in S \text { is a bud} \} \end{gathered}\end{aligned}$$
and satisfies the following.
(1)
Each \(\tau _{S,B} = p_1 \ldots p_n\) is a trace along the basic cycle of \(B\) such that there is some slope \(s\) for which \((p_n, p_1, s) \in R_{B, \mathcal {R}(B)}\).
(2)
For all \(\tau _{S,B_1}\) and \(\tau _{S,B_2}\), if \(B_1 \le _{SG} B_2\) then \(\tau _{S,B_1}(\mathcal {R}(B_1)) = \tau _{S,B_2}(\mathcal {R}(B_1))\).
(3)
For every strongly connected subgraph, \(S\), of \(SG\) there is a bud \(B\in S\) such that \(\tau _{S,B} = p_1 \ldots p_n\) has a progressing point or
.
The properties of a trace manifold entail that its constituent traces can be combined to yield descending traces for each infinite path.
Proposition 1
(Trace Manifold Criterion [2, Prop. 7.2.3]). If a (cycle normal) sloped graph has a trace manifold, then it satisfies Infinite Descent.
To our knowledge, we are the first to implement a concrete algorithm to decide the trace manifold criterion. Ultimately, however, given its low coverage and potentially exponential runtime, we decided not to include it in Cyclone’s final pipeline.
Algorithm. Firstly, check if the sloped graph, \(SG\), is in cycle normal form, returning “don’t know” if not. Otherwise, compute each possible trace along the basic cycles. Then, for each strongly connected subgraph, containing buds \(B_{1}, \ldots , B_{n}\), check for some possible combination of traces \(\tau _{1}, \ldots , \tau _{n}\) along their respective basic cycles, with at least one trace progressing, satisfying \(\tau _{i}(\mathcal {R}(B_{i})) = \tau _{j}(\mathcal {R}(B_{i}))\) for each pair of buds such that \(B_{i}\le _{SG} B_{j}\). This check succeeds iff a trace manifold exists. So, return “yes” in this case, otherwise return “don’t know”.
Complexity and Practical Runtime Evaluation. The algorithm described above is exponential in both the number of buds and the number of nodes of the sloped graph: quantification over all strongly-connected subgraphs leads to the exponential dependency on the number of buds, and the quantification over all traces following basic cycles leads to the exponential dependency in the number of (sloped graph) nodes. Note that, given the set of buds (information that is provided by Cyclist), checking whether a graph is in cycle normal form takes only polynomial time.
Evaluating the implementation of our algorithm we discovered that, despite its high worst-case complexity, its runtime performance on the instances in our database of sloped graphs is, on average, significantly better than the state-of-the-art complete method (OR). This is because the number of traces in each of these instances is usually fairly small. We observed that the more edges in the input sloped graph, the faster our implementation of TM compared to that of OR. Our implementation was at most 29% slower than OR, and up to 1,970% faster. However, despite its favourable runtime performance it only covered 31.2% of the sloped graphs in our database that satisfy Infinite Descent, and thus only 17.38% of the database overall. Moreover, although 48.4% of graphs in the database are in cycle normal form, TM returns an answer on only 35.9% of these. Interestingly, though, almost all cycle normal graphs in our database satisfying Infinite Descent also satisfy TM.
4.2 Flat Cycles
This section presents a novel linear runtime method for checking if a sloped graph does not satisfy Infinite Descent. For this, we first define the notion of the flat projection graph, which is the underlying directed graph retaining only edges whose associated sloped relation contains no downward slope.
Definition 5
(Flat projection graph). The Flat Projection Graph of a sloped graph \(SG= (V,E,Ps,(R_{v,v'})_{(v,v') \in E})\) is the graph
, where
Proposition 2
(Flat Cycles criterion (FC)). Let \(SG\) be a sloped graph. If
has a cycle then \(SG\) does not satisfy Infinite Descent.
Fig. 4.
Sloped graphs and their Flat Projection graphs (in blue)
Example 2
Fig. 4 shows two examples of sloped graphs: one that does not satisfy the flat cycles criterion and one that does. Fig. 4a presents a sloped graph with two nodes: node 0 with one position, \(p_0\), and node 1 with two positions, \(p_1, p_1^\prime \). Since there is a downward slope in \(R_{1,0}\), \((1,0)\notin E^\rightsquigarrow \) and therefore the flat projection graph of this sloped graph (presented in blue) does not contain a cycle. This, in turn, entails that FC does not yield a decision on this graph. On the other hand, Fig. 4b presents a sloped graph with three nodes: node 0 having one position and nodes 1, 2, having two positions each. Again, \((1,0)\notin E^\rightsquigarrow \) because there is a downward slope in \(R_{1,0}\). However, because there is no downward slope in either \(R_{0,2}\) or \(R_{2,0}\), we get that \((0,2)\in E^\rightsquigarrow \) and \((2,0)\in E^\rightsquigarrow \), thus, there is a cycle in the flat projection graph (presented in blue), which means that the sloped graph satisfies the flat cycles criterion. Indeed, the sloped graph portrayed in Fig. 4b does not satisfy Infinite Descent, as Prop. 2 entails.
While FC may seem like a strong condition, requiring an entire cycle in the graph with no downward slopes on any of its edges, in practice it is very frequent and covers 80.77% of the graphs in the database that do not satisfy Infinite Descent, and thus 35.76% of the entire database.
Algorithm. Algo. 1 checks if a sloped graph satisfies Infinite Descent using the FC criterion. It generates the flat projection graph and checks it for cycles using a depth-first search (DFS). If there is a cycle, we know from Prop. 2 that the sloped graph does not satisfy Infinite Descent and so return “no”. Otherwise, the algorithm returns “don’t know”.
Algorithm 1
Infinite Descent by the Flat Cycles Criterion
Complexity and Practical Runtime Evaluation. The algorithm goes over all edges in the sloped graph (|E| iterations) and for each one it checks, in time quadratic in the vertex width of the input graph, whether its associated sloped relation has no downward slope. If the relation has no downward slope we add the edge to the flat edges set, which can be done in \({\mathcal {O}}(1)\) if we store this set as an adjacency linked list for every node in the graph. Then we perform a DFS on the flat projection graph which has runtime complexity of \({\mathcal {O}}(|V|+|E^\rightsquigarrow |)\). Since \(E^\rightsquigarrow \subseteq E\), in the worst case \(|E^\rightsquigarrow |={\mathcal {O}}(|E|)\), which makes the worst-case runtime \({\mathcal {O}}(|E| \cdot w^2 + |V| + |E|) = {\mathcal {O}}(|V|+|E| \cdot (w^2 + 1))\).
Fig. 5 shows the runtime of checking the criterion as a function of either the number of nodes or the number of edges in the graph. The values in the figure are an average of the runtime among all sloped graphs with each number of nodes/edges. We can see a linear growth in the runtime in both graphs, as expected from the runtime complexity analysis.
Fig. 5.
Flat Cycles Runtime by Nodes and Edges
4.3 Descending Unicycles
Having defined in the previous section a linear-time algorithm that covers a significant amount of the graphs in the database that do not satisfy Infinite Descent, in this section, we present a novel, polynomial-time criterion that covers a significant amount of the graphs that also do satisfy Infinite Descent.
We first identify a class of sloped graphs we call unicycles graphs. We say that a path from cycle c to cycle \(c^\prime \) is any path \(v_0,...,v_n\) such that \(v_0\in c\) and \(v_n\in c^\prime \).
Definition 6
(Unicycles graph). A directed graph \(G=(V,E)\) is a unicycles graph if for every two distinct basic cycles \(c,c^\prime \) in G, if there is a path from c to \(c^\prime \), then there is no path from \(c^\prime \) to c.
Fig. 6.
Unicycles Graphs
Note that a unicycles graph necessarily does not contain any overlapping cycles, i.e., two cycles with some shared node(s). Thus, e.g., the graph in Fig. 4b is not a unicycles graph since there is a path in both directions through the node 0. However, the graph in Fig. 4a is a unicycles graph because it has just one cycle. The graphs in Fig. 6 are unicycles graphs because, in both cases, although there is a path from \(c_1 = 0,1\) to \(c_2 = 2,3\), there is no path from \(c_2\) to \(c_1\).
The key insight is that if a sloped graph is a unicycles graph, then the infinite paths in the sloped graph are of the form \(\pi =v_0,...,v_m,(u_0,...,u_k)^\omega \), with \(u_0,...,u_k\) a basic cycle in the graph. This means that checking Infinite Descent on unicycles graphs amounts to checking whether, for every basic cycle c in the graph, the path \(c^\omega \) has a progressing trace. We next formalize this requirement.
Definition 7
(Simply descending graph). We define the following, given a sloped graph \(SG= (V, E, Ps, (R_{v,v'})_{(v,v') \in E})\).
(1)
The positions graph induced by a path \(\pi = v_{1},\ldots ,v_{m}\) in \(SG\), denoted \(SG^{pos}_{\pi }\), is a directed graph
with a distinguished subset of progressing edges \(Prog_{\pi } \subseteq E_{\pi }\), defined by:
\(V_{\pi } = \{(v_{i}, p) \mid 1 \le i \le \text { m and }p \in Ps(v_{i})\}\)
\(E_{\pi } = \{((v_{i}, p), (v_{i+1}, q)) \mid 1 \le i < \text { m and }\exists s . (p, q, s) \in R_{v_{i},v_{i+1}}\}\)
(2)
A basic cycle c in \(SG\) is said to be descending if \(SG^{pos}_{c}\) has a basic cycle with at least one progressing edge (i.e., an edge in \(Prog_{c}\)).
(3)
We say that \(SG\) is simply descending if every basic cycle in \(SG\) is descending.
Example 3
The graph \(SG\) in Fig. 4a is simply descending because the basic cycle \((0, p_{0}), (1, p'_{1}) \) of \(SG^{pos}_{(0,1)}\) has a progressing edge. The graph \(SG\) in Fig. 4b is not simply descending, because its positions graph \(SG^{pos}_{(0,2)}\) has no progressing edge, and thus its basic cycle 0, 2 is not descending. Fig. 6 illustrates two sloped graphs with the same underlying directed graph. The graph in Fig. 6a is simply descending because both \(c_1 = (0,1)\) and \(c_2 = (2,3)\) are descending cycles. However, the graph in Fig. 6b is not simply descending because \(c_2\) is not descending.
For unicycles graphs, the simply descending criterion is both sound and complete for Infinite Descent.
Proposition 3
(Descending Unicycles criterion (DU)). If \(SG\) is a unicycles sloped graph, then \(SG\) satisfies Infinite Descent iff it is simply descending.
Like the FC criterion, the DU criterion seems to be a strong condition in requiring that cycles in the sloped graph do not overlap. However, again, in practice, this requirement is satisfied in 90.69% of all graphs in our database, which makes for almost complete coverage of the database. However, unlike the FC criterion, it can return both a definite “yes” and a definite “no” answer.
Algorithm 2
Infinite Descent by the Descending Unicycles Criterion
Algorithm. Algo. 2 checks if a sloped graph that is a tree with backlinks satisfies Infinite Descent using the DU criterion. First, it calculates the strongly connected components (SCCs) of the graph, together with the low link of each bud’s destination using Tarjan’s algorithm [26]. Note that a graph has overlapping cycles if and only if there are two buds whose destination nodes have equal low links. That is because two cycles overlap if and only if they form a strongly connected set and because the buds’ destination nodes have the same low link if and only if they are in the same SCC. Thus, if there are duplicates in this backedgesLowLinks list, then the graph is not a unicycles graph and we return a “don’t know”. Otherwise, the graph is a unicycles graph, which means that every strongly connected component is a basic cycle. Then, we go over all SCCs and check if they are descending cycles of \(SG\). If and only if so, by Prop. 3 we get that SG satisfies Infinite Descent. Checking if a cycle c is a descending cycle amounts to running Tarjan’s algorithm on \(SG^{pos}_{c}\) while also checking with each edge if it is progressing. We find a strongly connected component with a progressing edge in \(SG^{pos}_{c}\) if and only if c is a descending cycle in \(SG\). That is because the progressing edge must be a part of a basic cycle and because every basic cycle is a part of a SCC.
Complexity and Practical Runtime Evaluation. Line 1 uses Tarjan’s algorithm, which has a runtime complexity of \({\mathcal {O}}(|V|+|E|)\). It also returns some of the low links that are generated by Tarjan’s algorithm, of which there are \({\mathcal {O}}(|V|)\). Line 2 looks for duplicates in the returned low links list, which is done in O(|V|) (on average) by generating a hash set from the list and comparing its size to the low links list’s size. Finally, Line 4 iterates over all SCCs and for each one checks if it is descending using Tarjan’s algorithm on \(SG^{pos}_{SCC}\). \(SG\) is a unicycles graph, and so in any SCC of \(SG\) the number of nodes is equal to the number of edges. Further, since each edge in a strongly connected component SCC has \({\mathcal {O}}(w^2)\) corresponding edges in \(SG^{pos}_{SCC}\), Tarjan’s algorithm on \(SG^{pos}_{SCC}\) has runtime complexity of \({\mathcal {O}}(|SCC| + w^2 \cdot |SCC|)\). Since the SCCs of a graph are a partition of its nodes, the runtime complexity of the loop in Line 4 is \({\mathcal {O}}(|V| + w^2 \cdot |V|)\). Overall, then, the runtime complexity of Algo. 2 is \({\mathcal {O}}((|V|+|E|)+|V|+(|V| + w^2 \cdot |V|))= O(w^2 \cdot |V| + |E|)\).
Fig. 7.
Descending Unicycles Runtime
Fig. 7 shows the runtime of checking the DU criterion as a function of the number of nodes, edges, and buds, as well as the vertex width of the graph, with each point in the figure averaging the runtime among all sloped graphs with the associated number of nodes/edges/buds or vertex width. Because of the high correlation between the number of nodes and edges in a sloped graph, we plot both metrics in a single graph. In Fig. 7b, we see the highest runtimes around width 10 because the graphs that have the most amount of nodes/edges in our database also all have a width of around 10. The trend in Fig. 7a is only somewhat linear because the algorithm only traverses the positions of nodes in cycles. A clear linear trend is observed in Fig. 7c which plots the runtime as a function of the number of buds in the graph, which, in unicycles graphs, is the number of cycles. This indicates that the algorithm performs what seems to be a constant amount of work for each cycle in the sloped graphs from our database. This implies that cycles have a consistent size, and together with Fig. 7a we can infer that as the size of cyclic pre-proofs grow, so does the number of cycles.
5 The Cyclone Verifier and its Evaluation
Having reported above on the individual runtime performance of our implementations of each of the incomplete methods, we now present our integrated tool, Cyclone, which combines these into a pipeline that defaults to a complete method (specifically, OR) for cases not covered by our new methods. We also present the results of our experimental evaluation, comparing Cyclone with each of the complete decision procedures alone as they are implement in [8]. We implemented each of our new algorithms, as well as Cyclone itself, in C++ and integrated into the Cyclist prover framework [5]. A corresponding artifact, containing our implementation and experimental data, is available on Zenodo [19]. The experiments we report on, both in the current and previous section, were all performed on an Apple M1 CPU with 8GB of RAM, running macOS Sonoma.
5.1 Composing the Methods in Cyclone
Algorithm 3
Cyclone
Fig. 8.
Cyclone Methods Distribution and Runtime
The composition of the methods that Cyclone uses is presented in Algo. 3. As mentioned in sec. 4.1, we do not use the TM method: Cyclone only uses the FC and DU methods. It first applies the FC criterion to try and return a very fast “no”. If FC returns a “don’t know”, it then uses the DU criterion to try and return a (not as) fast “yes” or a “no”. Finally, if DU also returns “don’t know”, Cyclone resorts to using the existing, complete and exponential OR algorithm to obtain a definitive answer.
Fig. 8a shows the distribution of methods from which Cyclone derived its answer when run on our database. Fig. 8b presents the average runtime of the different methods used in Cyclone, aggregated by number of edges, as well as the interquartile ranges. We plot the runtimes only as a function of the number of edges since we observed that the other parameters of the complexity analysis have a high correlation with this parameter. The FC method is considerably faster than the other two, with what appears to be a constant line. The DU method appears to be slower than the FC but is still much faster than OR, which looks at least polynomial. Note that the faster the method the lower its coverage, and recall that FC covers 35.76% of the graphs in the database, whilst DU covers 90.69%. The OR method, which has a complete coverage of the database, is the slowest method. We run the methods in ascending order of runtimes because even when FC returns a “don’t know”, this still happens fast enough that the overhead does not noticeably affect the overall runtime. The same is true for the DU method compared to the runtime of OR.
We did experiment with an implementation that runs the various methods in parallel, rather than the sequential pipeline described above. However we found that, since the graphs in our database are rather small, the system overheads involved in introducing parallelism were detrimental to the overall performance compared to the sequential pipeline.
Fig. 8a shows that Cyclone decides Infinite Descent in polynomial time on around 92% of the sloped graphs in our database. This high coverage, together with the polynomial complexity of our incomplete methods, is what enables the high performance of Cyclone. Furthermore, as mentioned, even on the remaining 8% of graphs, the overhead of running them is so low compared to the runtime of the complete method that the overall performance is unaffected.
Fig. 9.
Methods Runtime Comparison
5.2 Comparison with State-of-the-Art Methods
We now report on our evaluation of Cyclone against the state-of-the-art methods (VLA, SLA, FWK, and OR) for deciding Infinite Descent using the database described in Sec. 3. The figures in this section again present aggregated average runtime of each method by the number of edges, and the interquartile ranges. Additionally, we compare the runtime overhead of each of the existing methods with Cyclone as the baseline.
Fig. 9a plots the runtime of all methods using a logarithmic scale. It shows a clear difference in the various methods’ runtimes and, most importantly, that Cyclone is the fastest among them. The runtime of every method grows somewhat sub-exponentially with the number of edges in the sloped graph. This might be because the sloped graphs in the database do not have many edges, so the exponential trend of the runtime does not yet manifest itself experimentally.
Fig. 9b and Fig. 9c present, respectively, the absolute overhead in milliseconds and the percentage overhead of each complete method with respect to Cyclone. Apart from the SLA method, the average percentage overhead increases as the graph size increases. This shows that the runtime complexity difference of the methods indeed manifests itself in the experimental results. Observe that Cyclone is between around 80% to around 350% faster than the fastest method (OR), between around 480% to around 2200% faster than VLA, between 480% and 43,000% faster than FWK.
Finally, looking at the SLA method we can see a constant line in the runtime. This is because we used a timeout of 3 seconds in our tests, and SLA seems to hit this timeout after a certain size of input. This explains why, in contrast with the other methods, the percentage overhead for SLA decreases as the number of edges increases. The timeout limit notwithstanding, we can still see a tremendous advantage to Cyclone, which is between around \(3 \times 10^4\)% and \(5 \times 10^6\)% faster than the SLA method. These results show that Cyclone significantly improves the practical runtime of the Infinite Descent check on real-world sloped graphs.
As noted in Sec. 3, our database contains the sloped graphs that Cyclist produced directly from concrete cyclic pre-proofs. However, Cyclist also pre-processes each sloped graph before handing it to the Infinite Descent check. This consists of pruning nodes that do not lie along cycles and collapsing non-branching paths, which considerably reduces the size of the graphs whilst maintaining the structure necessary for checking Infinite Descent. We also collected these minimised forms of the sloped graphs generated by Cyclist, and then evaluated Cyclone against the state-of-the-art methods on this preprocessed dataset. Here, Cyclone is still 90% to 170% faster than the best performing other method, which again is the OR method.
6 Conclusion
We introduced Cyclone, an efficient and general tool for deciding the Infinite Descent property, implemented by combining with existing exponential decision procedures two novel, incomplete but polynomial-time algorithms exploiting statistically significant structural properties of sloped graphs. We demonstrated, on real-world data, Cyclone’s superior runtime performance compared to existing approaches. Moreover, the Cyclone tool is open-ended in that it may incorporate additional semi-decision procedures as they are developed.
We evaluated Cyclone on a dataset generated by the Cyclist prover, consisting of graphs corresponding to cyclic pre-proofs from its test suites. To broaden coverage of real-world use cases, we plan to expand the dataset. In particular, since verifying Infinite Descent supports program termination verification via the size-change principle, we aim to create a dataset of termination instances, generated from, e.g. Agda’s termination checker, for future evaluation. We also plan to explore preprocessing methods other than Cyclist’s minimisation, which may better align with our methods and further improve Cyclone’s performance.
Acknowledgments.
This research was partially supported by the Israel Science Foundation (Grant No. 790/21).
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.
rule performs a case split on the predicate instance \(N(x)\), guided by the defining rules for \(N\), which substitutes \(0\) and \(s(y)\) for \(x\) in the left- and right-hand premises, respectively. In the latter, \(y\) is a fresh variable (denoting the predecessor of \(x\)) for which we know from the definition of \(N\) that \(N(y)\) must hold. The other steps of the proof unfold the \(E\) and \(O\) predicate instances, and perform substitutions. A cyclic proof has the structure of a tree with ‘backlinks’, i.e. a tree in which some of the leaves (called buds) have an edge to another node (called its companion). In Fig. 1, node 6 is a bud whose companion is (the syntactically equal) node 1. When all buds link to an ancestor node (as in this case), the proof is said to be (in) cycle normal (form). However, this need not be the case in general. The proof satisfies the Infinite Descent property since along the infinite path traversing the cycle, we can trace a value (the instances of the \(N\) predicate) that progresses (i.e. is unfolded by the
rule) infinitely often.
of slopes, whose elements are called flat and downward, respectively.
, \(R_{3,4} = R_{4,5} = \{(N(y),N(y),\rightsquigarrow )\}\), and \(R_{5,6} = \{(N(y),N(x),\rightsquigarrow )\}\).
we call \(i\) a progressing point in the trace. We may also write \(\tau (v_i)\) to denote the \(i\)th position, \(p_i\). A trace is decreasing if it has infinitely many progressing points. An infinite path is descending if it has a tail along which there is a decreasing trace.
. Once this ‘composition closure’ is computed, checking Infinite Descent amounts to verifying the presence of certain downward slopes in the relations representing loops in the sloped graph. This encoding is an instance of the algebraic path problem and can be solved using the Floyd-Warshall-Kleene (FWK) algorithm [16]. By taking advantage of the specific symmetric nature of the Infinite Descent setting, a so-called order-reduced (OR) optimisation of this procedure is possible [8].
.
, where 
has a cycle then \(SG\) does not satisfy Infinite Descent.
with a distinguished subset of progressing edges \(Prog_{\pi } \subseteq E_{\pi }\), defined by:
