Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction

Abstract

Transition invariants are a popular technique for automated termination analysis. A transition invariant is a covering of the transitive closure of the transition relation of a program by a finite number of well-founded relations. The covering is usually established by an inductive proof using transition predicate abstraction. Such inductive termination proofs have the structure of a finite automaton. These automata, which we call transition automata, offer a rich structure that has not been exploited in previous publications. We establish a new connection between transition automata and the size-change abstraction, which is another widespread technique for automated termination analysis. In particular, we are able to transfer recent results on automated complexity analysis with the size-change abstraction to transition invariants.

1 Introduction

The last decade has seen considerable interest in automated techniques for proving the termination of programs. Notably, the Terminator termination analyzer [14] has been able to analyze device drivers with several thousand lines of code. The analysis in [14] uses the termination criterion suggested by Rybalchenko and Podelski in [25] (for a discussion of earlier work that implicitly used the same principle we refer the reader to [6]): In order to show the well-foundedness of a relation $R$, it is sufficient to find a finite number of well-founded relations $R_1, \ldots , R_k$ with

where $R^+$ denotes the transitive closure of $R$.

An essential difficulty in using the above criterion lies in establishing the condition (*), as reasoning about the transitive closure $R^+$ usually requires induction. For this reason, not only the above criterion but also an inductive argument for establishing (*) was suggested in [25]. The inductive argument was further developed in [26], where the use of transition predicate abstraction (TPA) has been suggested for establishing condition (*). TPA is the basis for the termination analysis in Terminator. The starting point of our research are the inductive termination proofs with TPA, which have the structure of finite automata (as already observed in [26]). These automata, which we call transition automata, offer a rich structure that has not been exploited in previous publications. It is precisely this automaton structure, which allows us to connect inductive termination proofs with TPA to the size-change abstraction, and transfer recent results on automated complexity analysis.

We contrast our approach with the fascinating line of work [6, 30, 32], which aims at bounding the height of the relation $R$ in terms of the height of the relations $R_1,\ldots ,R_k$. In order to derive such bounds, [6, 30] replace Ramsey’s theorem, which has been used to prove (*) in [25], by more fine-grained Ramsey-like arguments. In this paper, we show that inductive termination proofs with TPA do not need to rely on Ramsey’s theorem and can be analyzed solely by automata-theoretic techniques.

Size-change abstraction (SCA), introduced by Ben-Amram, Lee and Jones in [22], is another wide-spread technique for automated termination analysis. SCA has been employed for the analysis of functional [22, 23], logical [31] and imperative [3, 10] programs and term rewriting systems [9], and is implemented in the industrial-strength systems ACL2 [23] and Isabelle [20]. Recently, SCA has also been used for resource bound and complexity analysis of imperative programs [34]. SCA is attractive because of several strong theoretical results on termination analysis [22], complexity analysis [12, 33] and the existence of ranking functions [5, 33]. The success of SCA has also inspired generalizations to richer classes of constraints [4, 5, 7]. The connection between TPA and SCA has been the subject of previous research [19], which contains first results but does not exploit the automaton structure of inductive termination proofs. In this paper, we make the following contributions:

Result 1: Our main result (Theorem 7) makes it possible to transfer recent results on automated complexity analysis with the size-change abstraction [12] to transition automata. In particular, we obtain a complete and effective characterization of asymptotic complexity analysis with transition automata. This result holds the potential for the design of new automated complexity analyzers, for example, by extracting complexity bounds from the inductive termination proofs computed by Terminator. We illustrate our result in the following. We consider the programs $P_1$ and $P_2$ given by Examples 1 and 2 in Fig. 1. One can model the transition relation of $P_1$ by the predicate $x' = x - 1 \wedge y' = N \vee x' = x \wedge y' = y - 1$ and the transition relation of $P_2$ by the predicate $x' = x - 1 \wedge y' = y \vee x' = x \wedge y' = y - 1$. The two relations $R_1$ and $R_2$ given by the predicates $x' < x$ resp. $y' < y$ are a transition invariant for both programs; we give an inductive proof which establishes condition (*) for both programs in Sect. 3. For motivation of our results we state here the relation to [6]: With the program invariant $x \le N \wedge y \le N$ (which can be computed by standard techniques such as Octagon analysis [24]), the result of [6] allows us to obtain the quadratic bound $O(N^2)$ on the complexity of both programs from the transition invariant given by the relations $R_1$ and $R_2$. However, this bound is imprecise for $P_2$, which has linear complexity. There is no hope in improving the bound for $P_2$, because the result of [6] just relies on $R_1$ and $R_2$. In this paper, we demonstrate that the inductive termination proof offers more structure. We show that just by analyzing the automaton structure of the proof we can deduce the linear bound O(N) for $P_2$.

Fig. 1.

The ? in the condition represents non-deterministic choice.

Result 2: Following [26] we examine a first termination criterion based on the universality of transition automata and show that the universality of the transition automaton implies the termination of the program under analysis (Theorem 2). We then show that transition automata admit a more general termination criterion based on the definition of an associated Büchi-automaton (Theorems 1 and 3). This more general termination criterion has the advantage that fewer predicates are needed for the termination proof (Example 7). We finally show that this new criterion is in fact the most general termination criterion admitted by transition automata (Theorem 4).

Result 3: We connect transition automata to the size-change abstraction in Sect. 6. In particular, we show how to transfer several results from the size-change abstraction to transition automata, demonstrating that techniques from SCA are applicable for the analysis of inductive termination proofs with transition predicate abstraction. This is of fundamental interest for understanding the relationship of both termination principles, because transition invariants have been suggested in [25] as a generalization of size-change termination proofs (and indeed later work has formally established that every size-change termination proof can be mimicked by a transition invariant termination proof [19]).

Organization of the Paper. Section 2 gives the basic definitions. Section 3 reviews transition predicate abstraction as introduced in [26]. Section 4 introduces transition automata and gives termination criteria. Section 5 reviews the size-change abstraction. Section 6 defines ‘canonical’ programs for transition automata and transfers results from the size-change abstraction to transition automata. Section 7 concludes.

2 Basic Definitions

We use $\circ$ to denote the usual product of relations, i.e., given two relations $B_1, B_2 \subseteq A\times A$ we define $B_1 \circ B_2 = \{(a_1,a_3) \mid \text { there is an } a_2 \in A\text { with } (a_1,a_2) \in B_1 \text { and } (a_2,a_3) \in B_2\}$. Let $B\subseteq A\times A$ be a relation. $B$ is well-founded if there is no infinite sequence of states $a_1a_2\cdots$ with $(a_i,a_{i+1}) \in B$ for all i. The transitive closure of $B$ is defined by $B^+ = \bigcup _{i \ge 1} B^i$, where $B^0 = \{(a,a) \mid a\in A\}$, $B^{i+1} = B^i \circ B$. Let $B\subseteq A\times A$ be a well-founded relation. For every element $a\in A$ we inductively define its ordinal height $\left||a \right||_B$ by setting $\left||a \right||_B= \sup _{(a,b) \in B} \left||b \right||_B+ 1$, where $\sup$ over the empty set evaluates to 0. We note that $\left||\cdot \right||_B$ is well-defined because $B$ is well-founded. We define the ordinal height of relation $B$ as $\left||B \right|| = \sup _{a\in A} \left||a \right||_B+ 1$.

2.1 Automata

A finite automaton $A= \langle Q, \varSigma , \delta , \iota , F\rangle$ consists of a finite set of states, a finite alphabet $\varSigma$, a transition relation $\delta : \varSigma \rightarrow \mathbf {2}^{Q\times Q}$, an initial state $\iota \in Q$, and a set of final states $F\subseteq Q$. Automaton $A$ is deterministic if for every $\tau \in Q$ and $a\in \varSigma$ there is at most one $\tau ' \in Q$ such that $(\tau ,\tau ') \in \delta (a)$. We also write $\tau \xrightarrow {a} \tau '$ for $(\tau ,\tau ') \in \delta (a)$. We extend the transition relation to words and define $\delta (w) = \delta (a_1) \circ \cdots \circ \delta (a_l)$ for every $w= a_1\cdots a_l \in \varSigma ^*$. A run of $A$ is a finite sequence $r= \iota \xrightarrow {a_1} \tau _1 \xrightarrow {a_2} \tau _2 \cdots \xrightarrow {a_l} \tau _l$. $r$ is accepting if $\tau _l \in F$. Automaton $A$ accepts a finite word $w\in \varSigma ^*$ if there is an accepting run $r= \iota \xrightarrow {a_1} \tau _1 \xrightarrow {a_2} \tau _2 \cdots \xrightarrow {a_l} \tau _l$ such that $w= a_1\cdots a_l$. We denote by $\mathcal {L}(A) = \{ w\in \varSigma ^* \mid A\text { accepts } w \}$ the language of words accepted by $A$. Automaton $A$ is universal if $\mathcal {L}(A) = \varSigma ^*$.

A Büchi automaton $A= \langle Q, \varSigma , \delta , \iota \rangle$ consists of a finite set of states, a finite alphabet $\varSigma$, a transition relation $\delta : \varSigma \rightarrow \mathbf {2}^{Q\times \{ \ge ,{>} \} \times Q}$, and an initial state $\iota \in Q$. We also write $\tau \xrightarrow [d]{a} \tau '$ for $(\tau ,d,\tau ') \in \delta (a)$. A run of $A$ is an infinite sequence $r= \iota \xrightarrow [d_1]{a_1} \tau _1 \xrightarrow [d_2]{a_2} \tau _2 \cdots$. $r$ is accepting if $d_i = \>$ for infinitely many i. Automaton $A$ accepts an infinite word $w\in \varSigma ^\omega$ if there is an accepting run $r= \iota \xrightarrow [d_1]{a_1} \tau _1 \xrightarrow [d_2]{a_2} \tau _2 \cdots$ such that $w= a_1a_2\cdots$. We denote by $\mathcal {L}(A) = \{ w\in \varSigma ^\omega \mid A\text { accepts } w \}$ the language accepted by $A$. Automaton $A$ is universal if $\mathcal {L}(A) = \varSigma ^\omega$.

Remark

We use this slightly unusual presentation of automata in order to conveniently represent the connection between automata and the size-change abstraction later on. In particular, this connection is the reason for using the symbols $\{\ge ,>\}$ instead of $\{0,1\}$ for (non-)accepting transitions.

2.2 Programs

A program $P= \langle St , I , \varSigma , \rho \rangle$ consists of a set of states $St$, a set of initial states $I \subseteq St$, a finite set of transitions $\varSigma$, and a labeling function $\rho : \varSigma \rightarrow \mathbf {2}^{ St \times St }$, which maps every transition $a\in \varSigma$ to a transition relation $\rho (a) \subseteq St \times St$. We extend the labeling function $\rho$ to finite words over $\varSigma$ and set $\rho (\pi ) = \rho (a_1) \circ \rho (a_2) \circ \cdots \circ \rho (a_l)$ for a finite word $\pi = a_1a_2\cdots a_l$. A computation of $P$ is a (finite or infinite) sequence $s_1 \xrightarrow {a_1} s_2 \xrightarrow {a_2} \cdots$ such that $s_1 \in I$ and $(s_i,s_{i+1}) \in \rho (a_i)$ for all i. Program $P$ terminates if there is no infinite computation of $P$. A relation $T \subseteq St \times St$ is a transition invariant for $P$ if $(\bigcup _{a\in \varSigma } \rho (a))^+ \subseteq T$. For a finite computation $s_1 \xrightarrow {a_1} s_2 \xrightarrow {a_2} \cdots s_{l+1}$ we call l the length of the computation.

Fig. 2.

Pictures of proof structures/transition automata.

Variables and Predicates. A common program model is to consider some finite set of variables $Var$ and define the set of states $St = Var \rightarrow \alpha$ as the mappings from $Var$ to some domain $\alpha$. Sets of states can then be described by predicates over $Var$ and transition relations by predicates over $Var \cup Var '$, where $Var '$ denotes the set of primed versions of the variables in $Var$. Given a predicate $p$ over $Var$, we write $\sigma \models p$ for $\sigma \in St$ if $p$ is true when each variable $x \in Var$ is replaced by $\sigma (x)$; given a predicate $p$ over $Var \cup Var '$, we write $\sigma ,\varsigma \models p$ for $\sigma ,\varsigma \in St$ if $p$ is true when each variable $x \in Var$ is replaced by $\sigma (x)$ and each variable $x' \in Var '$ is replaced by $\varsigma (x)$. Given a set of predicates $Pred$ over $Var$, we write $Rel ( Pred ) = \{ \sigma \in St \mid \sigma \models p\text { for all } p\in Pred \}$ for the states which satisfy all predicates in $Pred$. Given a set of predicates $Pred$ over $Var \cup Var '$, we write $Rel ( Pred ) = \{ (\sigma ,\varsigma ) \in St \times St \mid \sigma ,\varsigma \models p\text { for all } p\in Pred \}$ for the pairs of states which satisfy all predicates in $Pred$. We will also write $Rel _\alpha ( Pred )$ in case we want to highlight the domain $\alpha$.

Example 3

We now express the two programs from Fig. 1 in the above notation. For both programs, we consider the set of variables $Var = \{x,y\}$ and treat N as a symbolic constant. We choose the domain $\alpha = \omega$ according to the type nat of x and y. For both programs we model each branch of the if-statement as one transition. We set $P_i = \langle \{x,y\} \rightarrow \alpha , Rel _\alpha ( \{x = N, y = N\} ), \{a_1,a_2\}, \rho _i \rangle$, for $i = 1,2$, where we define the labeling functions $\rho _i$ using $C = \{x> 0, y > 0\}$:

$$\begin{aligned} \rho _1(a_1) \,{=}\, Rel _\alpha (C\cup \{ x' \,{=}\, x - 1, y' \,{=}\, \mathbf {N} \} ), \rho _1(a_2) \,{=}\, Rel _\alpha (C\cup \{ x' \,{=}\, x, y' \,{=}\, y - 1 \} ),\\ \rho _2(a_1) \,{=}\, Rel _\alpha (C\cup \{ x' \,{=}\, x - 1, y' \,{=}\, \mathbf {y} \} ), \rho _2(a_2) \,{=}\, Rel _\alpha (C\cup \{ x' = x, y' = y - 1 \} ), \end{aligned}$$

3 Transition Predicate Abstraction

In this section, we review the definitions and results from [26] in order to motivate our generalizations in Sect. 4. The development in [26] also considers fairness requirements, which are not relevant for this paper and therefore left out.

Abstract-Transition Programs. We fix some program $P= \langle St , I , \varSigma , \rho \rangle$. We split up the definition of abstract-transition programs (see Definition 3 of [26]) into two parts: proof structures and proof labelings. A proof structure is a finite automaton $A= \langle Q, \varSigma , \delta , \iota , \_ \rangle$, where $\delta (a) \subseteq Q\times (Q\setminus \{ \iota \})$ for all $a\in \varSigma$. For the moment, we ignore the acceptance condition; we will use it later on. A proof labeling $rel : Q\rightarrow \mathbf {2}^{ St \times St }$ maps every state $\tau \in Q$ of a proof structure to a transition relation $rel (\tau ) \subseteq St \times St$. A proof labeling is inductive if

$$\begin{aligned} rel (\iota ) = Id _ St ,&\quad \quad \text { and } \\ rel (\tau ) \circ \rho (a) \subseteq rel (\tau '),&\quad \quad \text { for all } (\tau ,\tau ') \in \delta (a) \text { and for all } a\in \varSigma , \end{aligned}$$

where $Id _ St$ is the identity relation over $St$. An abstract-transition program $P^\# = (A, rel )$ is a pair of a proof structure $A$ and an inductive proof labeling.

Abstract-transition program are constructed from a fixed finite set of transition predicates that describe transition relations (see Sect. 4 of [26]). The resulting abstract-transition programs have the following properties:

• (P1) The proof structure is a deterministic automaton (see Sect. 5.1 of [26]).

• (P2) For every word $a_1a_2\cdots a_n$ with $\rho (a_1a_2\cdots a_n) \ne \emptyset$ there is a run $\iota \xrightarrow {a_1} \tau _1 \xrightarrow {a_2} \tau _2 \cdots \xrightarrow {a_n} \tau _n$ of $A$ (see Lemma 1 from [26]).

• (P3) Every state $\tau \in Q\setminus \{ \iota \}$ is reachable from $\iota$ (the reader can check that the abstraction algorithm of [26] starts from the initial state $\iota$ and adds only states which are reachable from $\iota$).

We now state the core theorem of [26]; for illustration purposes, we also state its proof, which is based on condition (*), in the notation of this paper:

Theorem 1

(Theorem 1 of [26]). Let $P^\# = (A, rel )$ be an abstract program with property (P2). Then, $\bigcup _{\tau \in Q\setminus \{ \iota \}} rel (\tau )$ is a transition invariant for $P$. If $rel (\tau )$ is well-founded for every state $\tau \in Q\setminus \{ \iota \}$, then $P$ terminates.

Proof

For the first claim, we consider some $(s,s') \in \rho (a_1a_2\cdots a_n)$ for some word $a_1a_2 \cdots a_n$ with $n \ge 1$. By property (P2) we have that there is a run $\iota \xrightarrow {a_1} \tau _1 \xrightarrow {a_2} \tau _2 \cdots \xrightarrow {a_n} \tau _n$ of $A$. By the definition of an inductive proof labeling we have $\rho (a_1a_2\cdots a_n) \subseteq rel (\tau _n)$. Thus, we get that $(s,s') \in rel (\tau _n)$. Hence, we get $(\bigcup _{a\in \varSigma } \rho (a))^+ \subseteq \bigcup _{\tau \in Q\setminus \{ \iota \}} rel (\tau )$. The second claim then directly follows from the first claim based on condition (*). $\square$

Example 4

We will define an abstract-transition program for $P_1$. Let $A_1$ be the proof structure from Fig. 2. Let $rel _1$ be the proof labeling defined by $rel _1(\tau _1) = Rel _\alpha ( \{ x' < x \})$ and $rel _1(\tau _2) = Rel _\alpha ( \{ x' = x, y' < y \})$, where $\alpha = \omega$. It is easy to verify that $rel _1$ is inductive. Hence, $P_1^\# = (A_1, rel _1)$ is an abstract-transition program. Moreover, $rel _1(\tau _1)$ and $rel _1(\tau _2)$ are well-founded due to the predicates $x' < x$ and $y' < y$. The abstraction algorithm of [26] precisely computes $P_1^\#$ when called with the set of predicates $Pred = \{x'< x, x' = x, y' < y \}$.

Example 5

We will define an abstract-transition program for $P_2$. Let $A_2$ be the proof structure from Fig. 2. Let $rel _2$ be the proof labeling defined by $rel _2(\tau _1) = Rel _\alpha ( \{ x' < x \})$ and $rel _2(\tau _2) = Rel _\alpha ( \{ y' < y \})$, where $\alpha = \omega$. It is easy to verify that $rel _2$ is inductive. Hence, $P_2^\# = (A_2, rel _2)$ is an abstract-transition program. Moreover, $rel _2(\tau _1)$ and $rel _2(\tau _2)$ are well-founded due to the predicates $x' < x$ and $y' < y$. The abstraction algorithm of [26] precisely computes $P_2^\#$ when called with the set of predicates $Pred = \{x'< x, y' < y \}$.

Remark

The above proof of Theorem 1 only relies on property (P2). However, properties (P1) and (P3) explain the requirement that every non-initial state needs to be labelled by a well-founded relation: by (P3) every state $\tau \in Q\setminus \{ \iota \}$ is reachable by some word $a_1a_2\cdots a_n$; by (P1) the word $a_1a_2\cdots a_n$ necessarily reaches $\tau$; hence, $\tau$ needs to be labelled by some well-founded relation. In this paper, we will generalize Theorem 1 of [26] to non-deterministic proof structures; for such proof structures it will make sense to also consider proof labelings where not every state is labelled by some well-founded relation.

Remark

We further note that we can w.l.o.g. strengthen property (P2) to property (P2’): For every word $a_1a_2\cdots a_n$ there is a run $\iota \xrightarrow {a_1} \tau _1 \xrightarrow {a_2} \tau _2 \cdots \xrightarrow {a_n} \tau _n$ of $A$. We show the following: Let $P^\# = (A, rel )$ be an abstract-transition program with property (P2). Then we can extend $P^\#$ to some abstract-transition program $(A', rel ')$ with property (P2’). Further, if $rel (\tau )$ is well-founded for every non-initial state $\tau$, then $rel '(\tau )$ is well-founded for every non-initial state $\tau$.

We extend $A$ to $A'$ by adding a sink state $\tau _\emptyset$, which has self-loops for every $a\in \varSigma$; for every state $\tau$ and $a\in \varSigma$ we add an $a$-transition from $\tau$ to $\tau _\emptyset$ if $\tau$ does not have a $a$-successor. We extend $rel$ to $rel '$ by setting $rel '(\tau _\emptyset ) = \emptyset$. It is easy to see that (P1)–(P3) ensure that $rel '$ is inductive and that $(A', rel ')$ has property (P2’). Further $rel '(\tau _\emptyset ) = \emptyset$ is well-founded; hence, the second claims holds.

Invariants. An invariant for a program $P= \langle St , I , \varSigma , \rho \rangle$ is a set $Inv \subseteq St$ such that (1) $I \subseteq Inv$ and (2) $\{\sigma \in St \mid \text {there is a } \sigma ' \in Inv \text { with } (\sigma ',\sigma ) \in \rho (a) \} \subseteq Inv$ for all $a\in \varSigma$. For example, $Inv = Rel _\alpha (\{x \le N, y \le N\})$ is an invariant for $P_1$ and $P_2$. Invariants can be used to strengthen the transition relations of a program by restricting the transition relations to states from the invariant: Given an invariant $Inv$ for $P$ we define $P_ strengthen = \langle St , I , \varSigma , \rho _ strengthen \rangle$, where $\rho _ strengthen (a) = \rho (a) \cap ( Inv \times Inv )$ for all $a\in \varSigma$. Clearly, $P$ and $P_ strengthen$ have the same computations. However, working with $P_ strengthen$ for termination resp. complexity analysis is often beneficial because of the restricted transition relations. Indeed, strengthening the transition relation is often necessary to find a termination proof. For example, the Terminator termination analyzer [14] alternates between strengthening the transition relation and constructing a transition invariant. Similarly, complexity analyzers from the literature commonly employ invariant analysis as a subroutine either before or during the analysis [1, 2, 16,17,18, 29, 34]. The problem of computing invariants is orthogonal to the development in this paper. In our examples on complexity analysis we assume that appropriate invariants – such as $Inv = Rel _\alpha (\{x \le N, y \le N\})$ for $P_1$ and $P_2$ – can be computed by standard techniques such as Octagon analysis [24].

4 Transition Abstraction

In this section, we take another view on the result of [26] that we presented in the last section. On the one hand we aim at generalizing the termination analysis of [26] to non-deterministic proof structures. On the other hand we do not only want to reason about a single proof labeling but all possible proof labelings; to this end we will define a minimal inductive proof labeling. We fix a program $P= \langle St , I , \varSigma , \rho \rangle$ for the rest of this section.

A transition automaton $A= \langle Q, \varSigma , \delta , \iota , F\rangle$ is a finite automaton, where $\delta (a) \subseteq Q\times (Q\setminus \{ \iota \})$ for all $a\in \varSigma$ and $F\subseteq Q\setminus \{ \iota \}$. We point out that a transition automaton is a proof structure with final states.

Let $A= \langle Q, \varSigma , \delta , \iota , F\rangle$ be a transition automaton. We define a proof labeling $rel _ min : Q\rightarrow \mathbf {2}^{ St \times St }$ which precisely follows the structure of $A$: We set $rel _ min (\iota ) = Id _ St$, and for each $\tau \in Q\setminus \{\iota \}$ we set

$$\begin{aligned} rel _ min (\tau ) = \bigcup _{\text {word } \pi \text { with } (\iota ,\tau ) \in \delta (\pi )} \rho (\pi ), \end{aligned}$$

i.e., $rel _ min (\tau )$ is the union of the transition relations along all words with a run from the initial state to $\tau$.

We now state the central definition of this section:

Definition 1

(Transition Abstraction). A transition automaton $A$ is a transition abstraction of program $P$ if $rel _ min (\tau )$ is well-founded for each $\tau \in F$.

The notion of transition automata is motivated by Theorem 2, which extends the termination criterion of [26] to non-deterministic proof structures. Proposition 3 below states that Theorem 2 indeed is an extension of Theorem 1 of [26].

Theorem 2

Let $A$ be a transition automaton that is a transition abstraction of program $P$. If $A$ is universal, then $P$ terminates.

Proof

(Sketch). The theorem can be proved in the same way as Theorem 1 of [26] whose proof we presented in Sect. 3 based on an application of condition (*); we will later give a proof purely based on automata-theoretic techniques. $\square$

We first show that $rel _ min$ is the minimal inductive proof labeling:

Proposition 1

$rel _ min$ is inductive.

Proof

We consider some $(\tau ,\tau ') \in \delta (a)$. We consider some word $\pi$ with $(\iota ,\tau ) \in \delta (\pi )$. Then, $\pi a$ is a word with $(\iota ,\tau ') \in \delta (\pi a)$. Hence, $\rho (\pi a) \subseteq rel _ min (\tau ')$. Because this holds for all such words $\pi$, we get $rel _ min (\tau ) \circ \rho (a) \subseteq rel _ min (\tau ')$. $\square$

Proposition 2

Let $rel : Q\rightarrow \mathbf {2}^{ St \times St }$ be some inductive proof labeling. Then, $rel _ min (\tau ) \subseteq rel (\tau )$ for all $\tau \in Q$.

Proof

We note that $rel _ min (\iota ) = rel (\iota ) = Id _ St$. We will show that for all non-empty words $\pi$ that $(\iota ,\tau ) \in \delta (\pi )$ implies $\rho (\pi ) \subseteq rel (\tau )$. The proof proceeds by induction on the length of the word. For the induction start, we consider a word $\pi = a$ consisting of a single letter: Because $rel$ is inductive, we have $\rho (a) = Id _ St \circ \rho (a) = rel (\iota ) \circ \rho (a) \subseteq rel (\tau )$ for all $(\iota ,\tau ) \in \delta (a)$. For the induction step, we consider a word $\pi = \pi 'a$ with non-empty $\pi '$: We fix some $(\iota ,\tau ) \in \delta (\pi 'a)$. There is some $(\tau ,\tau ') \in \delta (a)$ with $(\tau ',\tau ) \in \delta (a)$ and $(\iota ,\tau ') \in \delta (\pi ')$. By induction assumption we have $\rho (\pi ') \subseteq rel (\tau ')$. Because $rel$ is inductive, we have $rel (\tau ') \circ \rho (a) \subseteq rel (\tau )$. Thus, $\rho (\pi 'a) = \rho (\pi ') \circ \rho (a) \subseteq rel (\tau )$. $\square$

With Proposition 2 we are now able to relate transition automata to the abstract-transition programs presented in the last section:

Proposition 3

Let $A= \langle Q, \varSigma , \delta , \iota , \_ \rangle$ be a proof structure with property (P2’). Let $rel$ be an inductive proof labeling such that $rel (\tau )$ is well-founded for every state $\tau \in Q\setminus \{ \iota \}$. With the set of final states $F= Q\setminus \{ \iota \}$, the proof structure $A$ is a transition abstraction of program $P$; further, $A$ is universal.

Proof

By Proposition 2 we have $rel _ min (\tau ) \subseteq rel (\tau )$ for all $\tau \in Q$. Hence, $A$ is a transition automaton. By property (P2’), the automaton $A$ has a run for every word; with $F= Q\setminus \{ \iota \}$ each such run is accepting. Hence, $A$ is universal. $\square$

Example 6

In Examples 4 and 5 we have argued that $P_1^\# = (A_1, rel _1)$ and $P_2^\# = (A_2, rel _2)$ are abstract-transition programs for $P_1$ resp. $P_2$. We now consider $A_1$ and $A_2$ as transition automata, defining the final states by $F= \{\tau _1,\tau _2\}$. By Proposition 3, $A_1$ and $A_2$ are transition abstractions for $P_1$ resp. $P_2$ and Theorem 2 can be applied.

We now define a transition automaton for program $P_1$ that is different from the transition automaton $A_1$ considered in Example 6:

Example 7

Let $A_3$ be the automaton from Fig. 2 with the set of final states $F= \{\tau _1,\tau _2\}$. We now argue that the transition automaton $A_3$ is a transition abstraction of $P_1$. In order to reason about the well-foundedness of $rel _ min (\tau _1)$ and $rel _ min (\tau _2)$, which are required by the definition of transition abstraction, we make use of Proposition 2 as a proof principle: it is sufficient to define an inductive proof labeling $rel _3$ and argue that $rel _3(\tau _1)$ and $rel _3(\tau _2)$ are well-founded.

We define $rel _3$ by setting $rel _3(\tau _1) = Rel _\alpha ( \{ x' < x \} )$ and $rel _3(\tau _2) = Rel _\alpha ( \{ y' < y \} )$ with $\alpha = \omega$. It is easy to verify that $rel _3$ is inductive. Moreover, $rel _3(\tau _1)$ and $rel _3(\tau _2)$ are well-founded due to the predicates $x' < x$ and $y' < y$. We conclude that $A_3$ is a transition abstraction of $P_1$. We observe that automaton $A_3$ (resp. $A_3'$) is not universal, and Theorem 2 cannot be applied.

Remark

We relate $A_3$ to the abstraction algorithm of [26]. We extend $A_3$ to the automaton $A_3'$ by adding a non-final state $\tau _ true$; we add an $a_1$-transition from $\tau _2$ to $\tau _ true$ and self-loops to $\tau _ true$ for $a_1$ and $a_2$. We set $rel _3(\tau _ true ) = Rel _\alpha ( \{ true \} ) = St \times St$ (note that $St \times St$ is not well-founded). The abstraction algorithm of [26] will exactly compute the abstract-transition program $P_3^\# = (A_3', rel _3)$ when called with the set of predicates $Pred = \{x'< x, y' < y \}$; we work with automaton $A_3$ instead of $A_3'$ because it has one state less and is easier to represent.

Remark

In the next subsection, we will establish the more general criterion of factor-termination, which is satisfied by automaton $A_3$ (resp. $A_3'$). Hence, we obtain a new termination proof for the program $P_1$, which has the advantage to use fewer predicates than the termination proof in Example 4: we contrast the set of predicates $Pred = \{x'< x, y' < y \}$ used in Example 7 with the set $Pred = \{x'< x, x' = x, y' < y \}$ used in Example 4.

4.1 Factor Termination

In this section, we introduce the criterion of factor-termination. We first introduce the criterion and then argue that factor-termination is a more general termination criterion than universality. Finally, we state that factor-termination is in fact the most general termination criterion based on transition abstraction.

The intuition behind the criterion of factor-termination is as follows: Given a transition automaton $A= \langle Q, \varSigma , \delta , \iota , F\rangle$, we directly use the well-foundedness of the relations $rel _ min (\tau )$, for final state $\tau \in F$. We check for every infinite word $\pi \in \varSigma ^\omega$ if there is a $\tau \in F$ and a factorization $\pi = \pi _0 \pi _1 \pi _2 \cdots$ into finite words $\pi _i$ such that $A$ has a run from $\iota$ to $\tau$ on $\pi _i$ for all $i \ge 1$. Such a factorization implies that there cannot be an infinite sequence of states $s_1 s_2 \ldots$ with $(s_i,s_{i+1}) \in \delta (\pi _i) \subseteq rel _ min (\tau )$ because this would contradict the well-foundedness of $rel _ min (\tau )$.

We implement the above idea with Büchi-automata. We fix some transition automaton $A= \langle Q, \varSigma , \delta , \iota , F\rangle$ for which we will define a Büchi-automaton $\mathcal {F}(A)$, which is composed of Büchi-automata $A_\tau$, for every $\tau \in F$, and an additional initial state $\kappa$. $\mathcal {F}(A)$ can non-deterministically wait in $\kappa$ a finite amount of time before moving to one of the automata $A_\tau$. Each $A_\tau$ checks for a factorization with regard to $\tau \in F$. We first formally define the automata $A_\tau$ and then $\mathcal {F}(A)$.

We start with an intuition for the construction of $A_\tau$. We take a copy of $A$ where all copied transitions are non-accepting. We obtain $A_\tau$ by adding additional accepting transitions that allow the automaton $A_\tau$ to move back to the initial state whenever it could move to $\tau$. The additional transitions allow $A_\tau$ to guess the beginning of a new factor; the Büchi-condition guarantees that an accepting run factorizes an infinite word into infinitely many finite words.

Formally, we define $A_\tau = \langle Q\times \{ \tau \}, \varSigma , \delta _\tau , (\iota , \tau ) \rangle$, where for all $a\in \varSigma$ we set

$$\begin{aligned} \delta _\tau (a) \,{=}\, \{ ((\tau ',\tau ),\ge ,(\tau '',\tau )) \mid (\tau ',\tau '') \,{\in }\, \delta (a)\} \cup \{ ((\tau ',\tau ),>,(\iota ,\tau )) \mid (\tau ',\tau ) \,{\in }\, \delta (a)\}. \end{aligned}$$

We state the main property of the automata $A_\tau$:

Proposition 4

$A_\tau$ accepts $\pi \in \varSigma ^\omega$ iff there is a factorization $\pi = \pi _1 \pi _2 \cdots$ into finite words $\pi _i$ such that $A$ has a run from $\iota$ to $\tau$ on $\pi _i$ for all i.

Proof

Let $r$ be an accepting run of $A_\tau$ on $\pi$. Hence, we can factor $\pi = \pi _1 \pi _2 \cdots$ into finite words $\pi _i$ such that the accepting transitions of $r$ exactly correspond to the last letters of the words $\pi _i$. We observe that the only accepting transitions are of shape $((\tau ',\tau ),>,(\iota ,\tau ))$ for $(\tau ',\tau ) \in \delta (a)$ (we denote this condition by (#)). Further, automaton $A_\tau$ mimics $A$ on the non-accepting transitions. Hence, on each word $\pi _i$ the run $r$ mimics a run of $A$ except for the last transition; however, the condition (#) guarantees that $A$ can move to $\tau$ with the last letter of $\pi _i$. $\square$

The factorization automaton is the Büchi-automaton $\mathcal {F}(A) = \langle G,\varSigma ,\varGamma ,\kappa \rangle$, where the set of states $G= (Q\times F) \cup \{\kappa \}$ consists of pairs of an automaton state and a final state plus a fresh initial state $\kappa$. We define the transition relation $\varGamma$ by $\varGamma (a) = \varGamma _1(a) \cup \varGamma _2(a) \cup \varGamma _3(a)$ for all $a\in \varSigma$, where

$$\begin{aligned} \varGamma _1(a) = \bigcup _{\tau \in F} \delta _\tau (a), \varGamma _2(a) = \{ (\kappa ,\ge ,\kappa ) \},\hbox { and }\varGamma _3(a) = \{ (\kappa ,\ge ,(\iota ,\tau )) \mid \tau \in F\}. \end{aligned}$$

The factorization automaton $\mathcal {F}(A)$ can be understood as the disjoint union of the initial state $\kappa$ and the Büchi-automata $A_\tau$; the state $\kappa$ allows $\mathcal {F}(A)$ to wait in $\kappa$ a finite amount of time before moving to the initial state of some $A_\tau$.

Fig. 3.

On the left: Automata $\mathcal {F}(A_1)$ and $\mathcal {F}(A_3)$, which have the same states and transitions except for the dashed transitions which only belong to $\mathcal {F}(A_1)$. On the right: Automaton $\mathcal {F}(A_2)$. Bold arrows denote accepting transitions.

Example 8

We draw the factor-automata of $A_1$, $A_2$ and $A_3$ in Fig. 3.

We are now able to formally state our new termination criterion: Transition automaton $A$ satisfies the factor-termination criterion if $\mathcal {F}(A)$ is universal. This notion is justified by Theorem 3 below:

Theorem 3

Let $A= \langle Q, \varSigma , \delta , \iota , F\rangle$ be a transition automaton and let $P= \langle St , I , \varSigma , \rho \rangle$ be a program such that $A$ is a transition abstraction of $P$. If $A$ satisfies the factor-termination criterion, then $P$ terminates.

Proof

We assume that $\mathcal {F}(A)$ is universal and that $P$ does not terminate. Then there is an infinite computation $t= s_1 \xrightarrow {a_1} s_2 \xrightarrow {a_2} \cdots$ of $P$. We consider the associated word $\pi = a_1a_2 \cdots$. Because $\mathcal {F}(A)$ is universal, the word $\pi$ is accepted by some run $r$. Word $\pi = \pi _a \pi _b$ can be split in a finite prefix $\pi _a$ and an infinite suffix $\pi _b$ such that $\mathcal {F}(A)$ stays in $\kappa$ while reading $\pi _a$ before leaving $\kappa$ and then reading $\pi _b$. We further see that while reading $\pi _b$, $\mathcal {F}(A)$ stays within $A_\tau$ for some $\tau \in F$. By Proposition 4, there is a factorization $\pi _b = \pi _1 \pi _2 \cdots$ such that $A$ has a run on each $\pi _j$ from $\iota$ to $\tau$. We split $t$ into corresponding subcomputations

$$\begin{aligned} t_j = s_{i_j} \xrightarrow {a_{i_j}} \cdots s_{i_{j+1}-1} \xrightarrow {a_{i_{j+1}-1}} s_{i_{j+1}} \end{aligned}$$

with $\pi _j = a_{i_j}\cdots a_{i_{j+1}-1}$. Hence, we have $(s_{i_j},s_{i_{j+1}}) \in \rho (\pi _j) \subseteq rel _ min (\tau )$ for all j. This gives us an infinite sequence $s_{i_1}s_{i_2}\ldots$ with $(s_{i_j},s_{i_j+1}) \in rel _ min (\tau )$. However, this results in a contradiction, because $rel _ min (\tau )$ is well-founded by the assumption that $A$ is a transition abstraction of $P$. $\square$

Next, we show that the universality of a transition automaton $A$ implies the factor-termination of $A$; the proof uses the fundamental fact that a Büchi-automaton is universal iff it accepts all ultimately-periodic words:

Lemma 1

Let $A$ be a transition automaton. If $A$ is universal, then $A$ satisfies the factor-termination criterion.

Proof

We assume that $A$ is universal. We will show that $\mathcal {F}(A)$ accepts all ultimately-periodic words. Let u, v be two finite words over $\varSigma$ and consider the ultimately-periodic word $uv^\omega$. Since $A$ is universal there is an accepting run of $A$ ending in some final state $\tau \in F$. We will use this run to construct an accepting run of $\mathcal {F}(A)$. In order to accept $uv^\omega$, the automaton $\mathcal {F}(A)$ reads the word u staying in the initial state $\kappa$ and moving to $(\iota ,\tau )$ with the last letter of u (we tacitly assume here that the length of u is at least one; however this is without loss of generality as we can consider the word uv instead of u); $\mathcal {F}(A)$ then reads the word v, mimicking the accepting run of $A$ in $A_\tau$, and moving to state $(\iota ,\tau )$ with the last letter of v; $A_\tau$ then reads the next occurrence of v in the same way; we note that the last transition, with which the automaton returns to the initial state $(\iota ,\tau )$, is accepting; thus the constructed run on $uv^\omega$ is accepting. $\square$

Remark

The combination of Theorem 3 and Lemma 1 provides an alternative proof of Theorem 2. We highlight that the proof of Lemma 1 proceeds purely by automata-theoretic techniques and does not make use of condition (*); in particular, Ramsey’s theorem is not needed to prove Theorem 1 of [26].

We now establish that factor-termination is a strictly more general termination criterion than universality:

Example 9

Let $A_3$ be the automaton from Example 7, where we have established that $A_3$ is a transition abstraction of $P_1$ and that $A_3$ is not universal. We have drawn $\mathcal {F}(A_3)$ in Fig. 3. It remains to argue that $\mathcal {F}(A_3)$ is universal.

We show that $\mathcal {F}(A_3)$ is universal by a case distinction: Assume a word contains infinitely many $a_1$. $\mathcal {F}(A_3)$ waits for the first $a_1$ and moves to $(\iota ,\tau _1)$ just before the first $a_1$; with the first $a_1$, $\mathcal {F}(A_3)$ moves to $(\tau _1,\tau _1)$; then $\mathcal {F}(A_3)$ again waits for the next $a_1$, moving to $(\iota ,\tau _1)$ just before the next $a_1$, and so on. An infinite word that does not contain infinitely many $a_1$, only contains $a_2$ from some point on; $\mathcal {F}(A_3)$ accepts such a word by waiting in the initial state $\kappa$ until there are only $a_2$ left and then moves to $(\iota ,\tau _2)$; $\mathcal {F}(A_3)$ then can stay in $(\iota ,\tau _2)$ while continuing to read the letters $a_2$.

We finally state that factor-termination is the most general termination criterion based on transition abstraction:

Theorem 4

Let $A$ be a transition automaton that does not satisfy the factor-termination criterion. Then there is a program $P$ such that $A$ is a transition abstraction of $P$, but $P$ does not terminate.

We prove Theorem 4 (see Corollary 2) and further results in Sect. 6 based on the close relationship of factorization automata and the size-change abstraction. We first introduce the size-change abstraction in the next subsection.

5 Size-Change Abstraction

Size-change abstraction (SCA) can be seen as an instantiation of (transition-) predicate abstraction with a restricted class of predicates: a size-change predicate over some set of variables $Var$ is an inequality $x \triangleright y'$ with $x,y \in Var$, where $\triangleright$ is either > or $\ge$ (recall that $y' \in Var '$ denotes the primed version of y). A size-change relation (SCR) is a set of size-change predicates over $Var$. A size-change system (SCS) $S= \langle Var , \varSigma , \lambda \rangle$ consists of a set of variables $Var$, a finite set of transitions $\varSigma$ and a labeling function $\lambda$, which maps every transition $a\in \varSigma$ to a SCR $\lambda (a)$ over $Var$.

The SCA methodology requires an abstraction mechanism that abstracts programs to SCSs. Various static analyzes have been proposed in the literature which perform such an abstraction [3, 9, 10, 20, 22, 23, 31, 34]. In this paper, we are not concerned with how to abstract programs to SCSs (and thus we do not describe an abstraction mechanism for programs). Rather, we will use results on the strength of SCA [12, 21] for the analysis of transition automata.

Results on the strength of SCA directly interpret SCSs as (abstract) programs, which can be seen as ‘most general programs’ that satisfies all the size-change predicates. We now state the interpretation of SCSs as programs for which we make use of the variable mappings and predicate interpretations defined in Sect. 3. An SCS $S= \langle Var , \varSigma , \lambda \rangle$ defines a program $\mathcal {P}_\alpha (S) = \langle St , St , \varSigma , \rho \rangle$, where $St = Var \rightarrow \alpha$ and $\rho (a) = Rel _\alpha (\lambda (a))$ for all $a\in \varSigma$; the program $\mathcal {P}_\alpha (S)$ is parameterized by some domain $\alpha$ that we require to be well-founded.

We will build on theoretical results for SCA which have been obtained by automata-theoretic techniques (we refer the interested reader to [13] for an overview). We begin by stating the syntactic termination criterion of [22]. Let $S= \langle Var , \varSigma , \lambda \rangle$ be an SCS. We define the Büchi-automaton $DESC (S) = \langle D, \varSigma , \mu , \kappa \rangle$, where the set of states $D= Var \cup \{\kappa \}$ consists of the variables and a fresh initial state $\kappa$, the alphabet $\varSigma$ is the same as the alphabet of $S$, the transition relation $\mu$ is defined by $\mu (a) = \mu _1(a) \cup \mu _2(a) \cup \mu _3(a)$ for all $a\in \varSigma$, where $\mu _1(a) = \lambda (a)$, $\mu _2(a) = \{(\kappa ,\ge ,\kappa )\}$ and $\mu _3(a) = \{(\kappa ,\ge ,x) \mid x \in Var \}$. Intuitively the automaton $DESC (S)$ waits a finite amount of time in the initial state $\kappa$ and then starts to trace a chain of inequalities $x_1 \triangleright _1 x_2 \triangleright _2 x_3 \cdots$ between the variables of $S$. The Büchi-acceptance condition ensures that $\triangleright _i = \>$ infinitely often. Now we are ready to define the syntactic termination criterion of [22]: SCS $S$ has infinite descent if $DESC (S)$ is universal. This criterion is sound and complete:

Theorem 5

([21, 22]).$S$ has infinite descent iff $\mathcal {P}_\alpha (S)$ terminates over all domains $\alpha$. Moreover, if $S$ does not have infinite descent, then $\mathcal {P}_\alpha (S)$ does not terminate for some domain $\alpha < \omega$ (i.e., $\mathcal {P}_\alpha (S)$ does not terminate when variables take values in some initial segment $\alpha = [0,N]$ of the natural numbers).

While the original motivation for studying SCA has been termination analysis, we recently extended the theoretical results on SCA to complexity analysis:

Theorem 6

([12]). Let $S$ be an SCS that is size-change terminating. Then there effectively is a rational number $z\ge 1$ such that the length of the longest run of $\mathcal {P}_{[0,N]}(S)$ is of asymptotic order $\varTheta (N^z)$ for natural numbers N.

Our result provides a complete characterization of the complexity bounds arising from SCA and gives an effective algorithm for computing the exact asymptotic bound of a given abstract program. The proof of Theorem 6 proceeds by rephrasing the question of complexity analysis for SCSs as a question about the asymptotic behaviour of max-plus automata. The main induction of the proof relies on the Factorization Forest Theorem [28], which is a powerful strengthening of Ramsey’s Theorem for finite semigroups that offers a deep insight into their structure (see [11] for an overview).

6 Canonical Programs for Transition Automata

In this section, we will relate transition abstraction and SCA. We will describe the extraction of a size-change system $S= \mathcal {S}(A)$ from a transition automaton $A$. We will argue that the associated program $\mathcal {P}_\alpha (S)$ is canonical for $A$. We will prove three results that justify the use of the word ‘canonical’:

• 1. We show that the criterion of factor-termination for $A$ agrees with the criterion of infinite descent for $S$ (Corollary 1).

• 2. We show that $A$ is a transition abstraction of $\mathcal {P}_\alpha (S)$ for all domains $\alpha$ (Proposition 5). This result allows us to establish that factor-termination is the most general termination criterion (Corollary 2).

• 3. If $A$ is a transition abstraction for some program $P$, then every run of $P$ can be mimicked by a run of $\mathcal {P}_\alpha (S)$, where the domain $\alpha$ depends on $P$ and needs to be chosen appropriately (Lemma 3). This result allows us to transfer the result on complexity analysis for SCSs (see Theorem 6) to transition automata (Theorem 7).

6.1 Extracting Size-Change Systems from Transition Automata

We fix some transition automaton $A= \langle Q, \varSigma , \delta , \iota , F\rangle$. Let $\mathcal {F}(A) = \langle G,\varSigma ,\varGamma ,\kappa \rangle$ be the associated factorization automaton, where $G= Q\times F\cup \{\kappa \}$ and $\varGamma (a) = \varGamma _1(a) \cup \varGamma _2(a) \cup \varGamma _3(a)$ for all $a\in \varSigma$. We extract the associated size-change system from $\mathcal {F}(A)$ and define $\mathcal {S}(A) = \langle Var , \varSigma , \lambda \rangle$ by setting $Var = Q\times F$ and $\lambda (a) = \varGamma _1(a)$ for all $a\in \varSigma$ (i.e., $\mathcal {S}(A)$ is obtained from automaton $\mathcal {F}(A)$ by restriction to the non-initial states).

Example 10

We consider the transition automaton $A_2$. We have drawn $\mathcal {F}(A_2)$ in Fig. 3. We now state the size-change system extracted from $\mathcal {F}(A_2)$: We have $\mathcal {S}(A_2) = \langle \{\iota ,\tau _1,\tau _2\} \times \{\tau _1,\tau _2\}, \{a_1,a_2\}, \lambda \rangle$, where $\lambda$ is given by

• $\lambda (a_1) = \{ (\iota ,\tau _1) \ge (\tau _1,\tau _1)', (\tau _1,\tau _1) \ge (\tau _1,\tau _1)', (\tau _2,\tau _2) \ge (\tau _2,\tau _2)',$ $\quad \; \quad \quad (\iota ,\tau _1)> (\iota ,\tau _1)', (\tau _1,\tau _1)> (\iota ,\tau _1)', (\tau _2,\tau _2) > (\iota ,\tau _2)'\}$,

• $\lambda (a_2) = \{ (\tau _1,\tau _1) \ge (\tau _1,\tau _1)', (\iota ,\tau _2) \ge (\tau _2,\tau _2)', (\tau _2,\tau _2) \ge (\tau _2,\tau _2)',$ $\quad \quad \quad \quad (\tau _1,\tau _1)> (\iota ,\tau _1)', (\iota ,\tau _2)> (\iota ,\tau _2)', (\tau _2,\tau _2) > (\iota ,\tau _2)'\}$.

Example 11

We consider the transition automaton $A_3$. We have drawn $\mathcal {F}(A_3)$ in Fig. 3. We now state the size-change system extracted from $\mathcal {F}(A_3)$. We have $\mathcal {S}(A_3) = \langle \{\iota ,\tau _1,\tau _2\} \times \{\tau _1,\tau _2\}, \{a_1,a_2\}, \lambda \rangle$, where $\lambda$ is given by

• $\lambda (a_1) = \{ (\iota ,\tau _1) \ge (\tau _1,\tau _1)', (\tau _1,\tau _1) \ge (\tau _1,\tau _1)', (\iota ,\tau _2) \ge (\tau _1,\tau _2)',$ $\quad \; \quad \quad (\tau _1,\tau _2) \ge (\tau _1,\tau _2)', (\iota ,\tau _1)> (\iota ,\tau _1)', (\tau _1,\tau _1) > (\iota ,\tau _1)'\}$,

• $\lambda (a_2) = \{ (\tau _1,\tau _1) \ge (\tau _1,\tau _1)', (\iota ,\tau _1) \ge (\tau _2,\tau _1)', (\tau _2,\tau _1) \ge (\tau _2,\tau _1)',$ $\quad \; \quad \quad (\tau _1,\tau _2) \ge (\tau _1,\tau _2)', (\iota ,\tau _2) \ge (\tau _2,\tau _2)', (\tau _2,\tau _2) \ge (\tau _2,\tau _2)',$ $\quad \; \quad \quad (\tau _1,\tau _1)> (\iota ,\tau _1)', (\iota ,\tau _2)> (\iota ,\tau _2)', (\tau _2,\tau _2) > (\iota ,\tau _2)'\}$.

We comment on the intuition behind the definition of the SCS $S= \mathcal {S}(A)$. The underlying idea has been to obtain a close correspondence between $DESC (S)$ and $\mathcal {F}(A)$. Indeed, $DESC (S)$ and $\mathcal {F}(A)$ are almost identical, the only difference is that the initial state of $DESC (S)$ allows moving to every state, whereas the initial state of $\mathcal {F}(A)$ only allows moving to the initial states of the components $A_\tau$. However, this difference does not change the set of accepted words, as we prove in the next lemma:

Lemma 2

Let $S= \mathcal {S}(A)$ be the SCS extracted from $A$. Then $\mathcal {L}(\mathcal {F}(A)) = \mathcal {L}( DESC (S))$.

Proof

We recall $DESC (S) = \langle D, \varSigma , \mu , \kappa \rangle$, where $D= Var \cup \{\kappa \}$ and $\mu (a) = \mu _1(a) \cup \mu _2(a) \cup \mu _3(a)$ for all $a\in \varSigma$. We see that both automata have the same set of states $G= D= Q\times F\cup \{\kappa \}$. From the definition of $\mathcal {F}(A)$ and $DESC (S)$ we further have that $\varGamma _1(a) = \mu _1(a)$, $\varGamma _2(a) = \mu _2(a)$ and $\varGamma _3(a) \subseteq \mu _3(a)$ for all $a\in \varSigma$.

Thus, we get $\mathcal {L}(\mathcal {F}(A)) \subseteq \mathcal {L}( DESC (S))$ because every run of $A$ is also a run of $DESC (S)$. We now show $\mathcal {L}(\mathcal {F}(A)) \supseteq \mathcal {L}( DESC (S))$: Let $\pi$ be some word accepted by $DESC (S)$ and let $r$ be an accepting run of $DESC (S)$ on $\pi$. We can choose some factorization $\pi = \pi _1\pi _2$ such that the last transition in $r$ when reading $\pi _1$ is accepting. We note that after reading $\pi _1$, $DESC (S)$ must be in some state $(\iota ,\_)$ because accepting transition always move to some state where the first component is $\iota$. We further note that while reading $\pi _2$, $DESC (S)$ only uses transitions from $\mu _1$, because there is no transition returning to $\kappa$. Hence, the accepting run $r$ of $DESC (S)$ can be mimicked by $\mathcal {F}(A)$ as follows: $\mathcal {F}(A)$ waits in the initial state $\kappa$ while reading $\pi _1$ and then moves to the state $(\iota ,\_)$ with the last letter of $\pi _1$. After that $\mathcal {F}(A)$ follows the accepting run of $DESC (S)$ on $\pi _2$, which can be done because of $\varGamma _1 = \mu _1$. $\square$

As immediate corollary we get the equivalence of the termination conditions:

Corollary 1

$A$ has factor termination iff $S$ has infinite descent.

6.2 Factor-Termination Is the Most General Termination Criterion

We consider the size-change system $S= \mathcal {S}(A)$ extracted from transition automaton $A$. Our next result is that $A$ is a transition abstraction for the program $\mathcal {P}_\alpha (S)$ associated to $S$. The crucial insight is that $S$ exactly implements the minimal requirements to satisfy the condition of transition abstraction: the inequalities of $S$ exactly follow the transition relation of $A$, where strict inequalities ensure that the value of variable $(\iota ,\tau )$ decreases iff $A$ visits an accepting state $\tau$.

Proposition 5

$A$ is a transition abstraction of $\mathcal {P}_\alpha (S)$ for all domains $\alpha$.

Proof

Let $\alpha$ be some well-founded domain. We will show that $A$ is a transition abstraction of $\mathcal {P}_\alpha (S)$ using Proposition 2 as proof principle. For this we define a size-change relation $T_\tau$ for each $\tau \in Q\setminus \{\iota \}$. We set $T_\tau = \{(\iota ,\tau ') \ge (\tau ,\tau ') \mid \tau ' \in F\} \cup T^ dec _\tau$, where $T^ dec _\tau = \{ (\iota ,\tau ) > (\iota ,\tau ) \}$, if $\tau \in F$, and $T^ dec _\tau = \emptyset$, otherwise. It is easy to check that we have $Rel _\alpha (T_\tau ) \circ Rel _\alpha (\lambda (a)) \subseteq Rel _\alpha (T_{\tau '})$ for all $(\tau ,\tau ') \in \delta (a)$. We now apply Proposition 2 and get $rel _ min (\tau ) \subseteq Rel _\alpha (T_\tau )$ for all $\tau \in Q$.

It remains to argue that the relations $rel _ min (\tau )$ are well-founded for all $\tau \in F$. This follows from $rel _ min (\tau ) \subseteq Rel _\alpha (T_\tau )$ and the fact that $Rel _\alpha (T_\tau )$ is well-founded due to the predicate $T^ dec _\tau$, which ensures the decrease of variable $(\iota ,\tau )$. $\square$

We are now in a position to prove Theorem 4, i.e., that factor termination is the most general termination criterion for transition abstraction:

Corollary 2

Let $A$ be a transition automaton that does not satisfy the factor-termination criterion. Then $A$ is a transition abstraction of $\mathcal {P}_\alpha (S)$ for all domains $\alpha$, but $\mathcal {P}_\alpha (S)$ does not terminate for some $\alpha < \omega$.

Proof

From Corollary 1 we get that $S$ does not satisfy the infinite descent criterion because $A$ does not satisfy the factor-termination criterion. By Theorem 5 we know that the program $\mathcal {P}_\alpha (S)$ does not terminate for some $\alpha < \omega$ because $S$ does not size-change terminate. We have that $A$ is a transition abstraction of $\mathcal {P}_\alpha (S)$ by Proposition 5. $\square$

6.3 Complexity Analysis with Transition Automata

Let $A= \langle Q, \varSigma , \delta , \iota , F\rangle$ be a transition automaton and $P= \langle St , I , \varSigma , \rho \rangle$ be a program such that $A$ is a transition abstraction of $P$. Let $S= \mathcal {S}(A) = \langle Var , \varSigma , \lambda \rangle$ be the SCS extracted from $A$. We will show that every run of $P$ can be mimicked by a run of $\mathcal {P}_\alpha (S)$, where the domain $\alpha$ depends on $P$ and needs to be chosen appropriately. We first introduce the machinery necessary to define $\alpha$.

We define the height of a transition abstraction as the maximum of the heights of the well-founded relations $rel _ min (\tau )$, i.e., we set

$$\begin{aligned} height (A,P) = \max _{\tau \in F} \left|| rel _ min (\tau ) \right||. \end{aligned}$$

We set $height ^\bullet (A,P) = height (A,P) + 1$; we work with $height ^\bullet (A,P)$, which differs from $height (A,P)$ by plus one for technical convenience; however, the difference of plus one is not important for our results on asymptotic complexity analysis.

We introduce another auxiliary definition. For every pair $(\tau ',\tau ) \in Q\times F$ we define a relation $Succ _P(\tau ',\tau ) \subseteq St \times St$ by setting

$$\begin{aligned} Succ _P(\tau ',\tau ) = \bigcup _{\text {word } \pi \text { with } (\tau ',\tau ) \in \delta (\pi )} \rho (\pi ). \end{aligned}$$

We note that $Succ _P(\iota ,\tau ) = rel _ min (\tau )$ for all $\tau \in F$.

For every pair $(\tau ',\tau ) \in Q\times F$ we define a function $rank _{\tau ',\tau }: St \rightarrow height ^\bullet (A,P)$ that maps a state $s\in St$ to an ordinal below $height ^\bullet (A,P)$, by setting

$$\begin{aligned} rank _{\tau ',\tau }(s) = \sup _{(s,s') \in Succ _P(\tau ',\tau )} \left||s' \right||_{ rel _ min (\tau )} + 1, \end{aligned}$$

where the $\sup$ over the empty set evaluates to 0. The following proposition is immediate from the definitions:

Proposition 6

We have $rank _{\iota ,\tau }(s) = \left||s \right||_{ rel _ min (\tau )}$ for all $s\in St$.

Proof

Let $s\in St$ be some state. From the definition of $Succ _P$ we get $Succ _P(\iota ,\tau ) = rel _ min (\tau )$. Thus, we get $rank _{\iota ,\tau }(s) = \sup _{(s,s') \in Succ _P(\iota ,\tau )} \left||s' \right||_{ rel _ min (\tau )} + 1 =$ $\sup _{(s,s') \in rel _ min (\tau )} \left||s' \right||_{ rel _ min (\tau )} + 1 = \left||s \right||_{ rel _ min (\tau )}$. $\square$

For every $s\in St$ we define a valuation $\sigma _s: Q\times F\rightarrow height ^\bullet (A,P)$ by setting $\sigma _s(\tau ',\tau ) = rank _{\tau ',\tau }(s)$.

Lemma 3

Let $\alpha = height ^\bullet (A,P)$. For all pairs of states $(s,s') \in \rho (a)$, where $a\in \varSigma$, we have $(\sigma _s,\sigma _{s'}) \in Rel _\alpha (\lambda (a))$.

Proof

Let $a\in \varSigma$ be some transition and let $(s,s') \in \rho (a)$ be a pair of states in the associated transition relation.

We consider an inequality $(\tau ,\tau '') \ge (\tau ',\tau '')' \in \lambda (a)$. By definition of $\lambda (a)$ we have $(\tau ,\tau ') \in \delta (a)$. From this we get $\{(s,s')\} \circ Succ _P(\tau ',\tau '') \subseteq Succ _P(\tau ,\tau '')$ because for every word $\pi$ such that $(\tau ',\tau '') \in \delta (\pi )$ we have that $(\tau ,\tau '') \in \delta (a\cdot \pi )$ and thus $(s',s'') \in \rho (\pi )$ implies $(s,s'') \in \rho (a\cdot \pi )$. Hence, we get $\sigma _s(\tau ,\tau '') = rank _{\tau ,\tau ''}(s) = \sup _{(s,s'') \in Succ _P(\tau ,\tau '')} \left||s'' \right||_{ rel _ min (\tau '')} + 1 \ge$ $\sup _{(s',s'') \in Succ _P(\tau ',\tau '')} \left||s'' \right||_{ rel _ min (\tau '')} + 1 = rank _{\tau ',\tau ''}(s') = \sigma _{s'}(\tau ',\tau '')$.

We consider an inequality $(\tau ',\tau ) > (\iota ,\tau )' \in \lambda (a)$. By definition of $\lambda (a)$ we have $(\tau ',\tau ) \in \delta (a)$. From this we get $(s,s') \in \rho (a) \subseteq Succ _P(\tau ',\tau )$. From Proposition 6 we have $rank _{\iota ,\tau }(s') = \left||s' \right||_{ rel _ min (\tau )}$. Hence, we get $\sigma _s(\tau ',\tau ) = rank _{\tau ',\tau }(s) = \sup _{(s,s'') \in Succ _P(\tau ',\tau )} \left||s'' \right||_{ rel _ min (\tau )} + 1 > \left||s' \right||_{ rel _ min (\tau )} = rank _{\iota ,\tau }(s') = \sigma _{s'}(\iota ,\tau )$. $\square$

We immediately obtain the following corollary:

Corollary 3

Let $\alpha = height ^\bullet (A,P)$. Let $s_1 \xrightarrow {a_1} s_2 \xrightarrow {a_2} \cdots$ be a computation of $P$. Then, $\sigma _{s_1} \xrightarrow {a_1} \sigma _{s_2} \xrightarrow {a_2} \cdots$ is a computation of $\mathcal {P}_\alpha (S)$.

Finally, we are in a position to transfer Theorem 6:

Theorem 7

Let $A$ be a transition automaton that satisfies the factor-termination termination criterion. Let $S= \mathcal {S}(A)$. Let $z$ be the rational number obtained from Theorem 6 for $S$.

Let $P= \langle St , I _N, \varSigma , \rho \rangle$ be a program whose set of initial states $I _N$ is parameterized by natural number $N \in \mathbb {N}$, such that $A$ is a transition abstraction of $P$ and $height (A,P) = O(N)$. Then, the length of the longest computation of $P$ is of asymptotic order $O(N^z)$.

Moreover, $A$ is a transition abstraction for $\mathcal {P}_{[0,N]}(S)$ and the length of the longest computation of $\mathcal {P}_{[0,N]}(S)$ is of asymptotic order $\varTheta (N^z)$.

Proof

By Proposition 5, $A$ is a transition abstraction of $\mathcal {P}_{[0,N]}(S)$ for all $N \in \mathbb {N}$. From Theorem 6 we have that the longest computation of $\mathcal {P}_{[0,N]}(S)$ is of asymptotic order $\varTheta (N^z)$.

Because of $height (A,P) = O(N)$, we can find some $a,b \in \mathbb {N}$ such that $height (A,P) \le a \cdot N + b$ for all $N \in \mathbb {N}$. By Corollary 3, for every computation of $P_N$ there is a computation of $\mathcal {P}_{[0,a \cdot N + b]}(S)$ of equal length. Hence, the longest computation of $P_N$ is of asymptotic order $O((a \cdot N + b)^z) = O(N^z)$. $\square$

We highlight that Theorem 7 gives a complete characterization of the complexity bounds obtainable with transition abstraction and provides an effective algorithm for computing these complexity bounds.

Theorem 7 allows us to derive the precise complexity for $P_1$ and $P_2$:

Example 12

We consider the size-change system $S= \mathcal {S}(A_2)$, which we have extracted in Example 10 from transition automaton $A_2$. Theorem 6 allows us to derive that $\mathcal {P}_{[0,N]}(S)$ has complexity $\varTheta (N)$. In Example 5 we defined an abstract-transition program $(A_2, rel _2)$ for $P_2$; the inductive proof labeling $rel _2$ in conjunction with the invariant $Inv = Rel _\alpha (\{x \le N, y \le N\})$ implies that $height (A_2,P_2) = N$. Hence, we can apply Theorem 7 and infer that $P_2$ has complexity O(N), which is the precise asymptotic complexity of $P_2$.

We consider the size-change system $S= \mathcal {S}(A_3)$, which we have extracted in Example 11 from transition automaton $A_3$. Theorem 6 allows us to derive that $\mathcal {P}_{[0,N]}(S)$ has complexity $\varTheta (N^2)$. In Example 4 we defined an abstract-transition program $(A_1, rel _1)$ for $P_1$; the inductive proof labeling $rel _1$ in conjunction with the invariant $Inv = Rel _\alpha (\{x \le N, y \le N\})$ implies that $height (A_1,P_1) = N$. Hence, we can apply Theorem 7 and infer that $P_2$ has complexity $O(N^2)$, which is the precise asymptotic complexity of $P_2$.

7 Future Directions and Conclusion

In this paper, we have established a new connection between transition automata and the size-change abstraction. Our results suggest that all tools which implement termination analysis with transition invariants based on an inductive argument (such as Terminator) can be retro-fitted to be complexity analyzers, which is an interesting direction for further research: While this paper has investigated what information can be extracted from a fixed proof (i.e., from a fixed set of transition predicates), there is also the question of what strategy for predicate selection gives the best results. We have seen that the predicates $x' < x$ and $y' < y$ allow inferring the linear complexity of $P_2$; these predicates are simple and can be extracted from the if- resp. else branch of $P_2$ by simple heuristics. On the other hand, the predicate $x'+y' < x+y$ allows establishing the linear complexity of $P_2$ using a single predicate; this predicate, however, is more complex and requires more complicated heuristics for extraction. Finding the right balance in predicate selection is an interesting topic for future research.

Ranking function construction is an alternative technique for termination proofs: [33] states a complete construction for deterministic size-change systems. [8, 15] describes practical but incomplete constructions for general programs based on transition predicate abstraction. [15] states an example which has a transition invariant but no lexicographic ranking function over linear expressions; it is interesting to better understand the connection between the different termination proof techniques and investigate under which conditions ranking functions can be constructed.

Our results on transition abstraction and the previous results on size-change abstraction heavily rely on automata-theoretic techniques. We speculate that the study of the automaton structure of other inductive proofs, such as cyclic proofs [27], might also yield interesting results.