Existence of sets that are regular but not computable

A regular set is called computable if one can construct a finite-state automaton to recognise it. Given a finite alphabet $\Sigma$, a rational transition system is a tuple $(I, T)$ comprised of a regular set $I\subseteq\Sigma^*$ as the initial states and a rational relation $T\subseteq\Sigma^*\times\Sigma^*$ as the transition relation. We will use $T^k$ to denote the rational relation formed by composing $T$ for $k$ times, and $T^*$ to denote the reflexive and transitive closure of $T$. In this way, $T^*(I)$ will represent the reachability set of system $(I,T)$, i.e., the set of words that can be reached from the words in $I$ through a finite number of transitions.
It is clear that $T^k(I)$ is regular and computable for any $0\le k<\infty.$ It however may be less obvious that the reachability set $T^*(I)$ is not necessarily regular. To see this, consider a system $\Sigma\equiv\{a,b\}$, $I\equiv\{(ab)^n:n\ge 1\}$ and $T\equiv\{(xbay, xaby): x,y\in \Sigma^*\}.$ Then $T^*(I) \cap a^*b^* =\{a^nb^n:n\ge1\}$ is a well-know non-regular set, which implies that $T^*(I)$ is non-regular as well. On the other hand, there are rational transition systems of which the reachability sets are guaranteed to be regular, such as pushdown systems. In fact, the reachability relation of a pushdown system is regular and poly-time computable [12]. Surprisingly, $T^*(I)$ it is not necessarily computable even when it is regular. Namely, given a regular language $A$ and a rational transition system $(I, T)$, it is undecidable to check where $T^*(I)=A$ even though the former is known to be a regular set. This post will try to present a self-contained argument about the existence of such systems.
Subword ordering. Our argument would centre around a reflexive and transitive relation called "a subword of": given $x,y\in\Sigma^*$, $x\preceq y$ holds iff $x$ can be obtained by removing some segments from $y.$
Lemma. (Higman) A set is finite if all elements in it are mutually incomparable w.r.t. $\preceq.$
Proof. For $x,y\in\Sigma^*$, let $x\sim y$ iff there are distinct alphabets $a_1,...,a_n$ in $\Sigma$ such that both $x$ and $y$ match $a_1^+a_2^+...a_n^+.$ It is clear that $\sim$ is an equivalence relation splitting $\Sigma^*$ into $\binom{N}{1}1! + \binom{N}{2}2! + ... + \binom{N}{N} N!$ classes where $N=|\Sigma|$, and two words are comparable iff they are in the same class. ☐
Given a set $X\subseteq \Sigma^*$, define the upward closure of $X$ as $uc(X)\equiv\{w:\exists w'\in X.\ w'\preceq w\}.$ We say $X$ is upward closed iff $X=uc(X).$ Higman's lemma tells us that every upward closed set have a finite representation.
Lemma 1. Every upward closed set is regular.
Proof. Note that for any $X\subseteq\Sigma^*$, elements in $min(X)\equiv\{w\in X: \forall w'\in X.\ w'\not\preceq w\}$ are mutually incomparable. It follows from Higman's lemma that $min(X)$ is finite. Also, $X$ is upward closed iff $X=uc(X)=\bigcup_{w\in min(X)}wc(w)$, which implies $X$ is regular since $min(X)$ is finite and $uc(w)$ is regular for every $w\in\Sigma^*.$ ☐
Another consequence of Higman's lemma is that every increasing (in the sense of set inclusion) sequence of upward closed sets is finite.
Lemma 2. If $X_0\subseteq X_1\subseteq X_2\subseteq...$ and $X_i=uc(X_i)$ for all $i\ge0$, then there exists a finite $n$ such that $X_k=X_n$ for all $k\ge n.$
Proof. Let $X\equiv \bigcup_{i\ge 0} X_i.$ Since $min(X)$ is finite by Higman's lemma, there exists $n$ such that $X_k\cap min(X)=\emptyset$ for all $k\ge n.$ But this means $X_k\subseteq X_n$ for all $k\ge n.$ ☐
Lemma 3. For every infinite sequence of words $w_0,w_1,...\in \Sigma^*$, there exists $i<j$ such that $w_i\preceq w_j.$
Lemma 4. For any sets $X_0,X_1,...\subseteq\Sigma^*$, $uc(\bigcup_{i\ge 0}X_i)=\bigcup_{i\ge 0}uc(X_i).$
Lossy channel systems. We briefly introduce the concept of lossy channel systems. A channel system with $n$ queues are like a pushdown system with $n$ stacks except that it uses FIFO queues instead of FILO stacks. Channel systems are more powerful than pushdown systems, because they only need one queue to simulate Turing machines while pushdown systems need two stacks. A lossy channel system is a channel system where contents in the queues can be spontaneously lost. Technically, the capability of losing data can be introduced to a channel system by adding a non-deterministic self loop to each control state that removes an arbitrary alphabet from the queues.
Note that channel systems (lossy or not) can be expressed as rational transition systems where a configuration with n queues is encoded as a word in form of [control state]#[contents of the 1st queue]#...#[contents of the nth queue]#. We can define a subword ordering $\preceq_L$ over the configurations of a channel system as follows:

$c$#$w_1$#$...$#$w_n$# $\preceq_L$ $c'$#$w_1'$#$...$#$w_n'$#$\quad$ iff $\quad c=c'$ and $w_i\preceq w_i'$ for $i=1,...,n.$

Since the number of control states is finite, Lemma 1~3 also holds for $\preceq_L.$
Lossy channel systems enjoy many good properties. Among them, two properties are of particular interest for our establishment:
Fact 1. If $u\rightarrow^* w$ then $u\rightarrow^* w'$ for all $w'\preceq w.$ It follows that the complement of the reachability set is upward closed w.r.t. $\preceq_L.$
Fact 2. For any set of configurations $C$, the set $pre^*(C)\equiv\{w:\exists w'\in C.\ w\rightarrow^* w'\}$ of its predecessors is upward closed w.r.t. $\preceq_L.$
Theorem 1. The reachability set of a lossy channel system is regular.
Proof. This theorem is an immediate consequence of Fact 1, Lemma 1, and the fact that regular sets are closed under complementation. ☐
Given a system $(I, T)$ and a regular set $B\subseteq\Sigma^*$, the reachability problem asks whether $T^*(I)\cap B \neq\emptyset$, i.e., words in $B$ are reachable from words in $I$ through a finite number of transitions.
Theorem 2. The reachability problem of a lossy channel system is decidable.
Proof. Historically, this result was first proved in [6] using backward analysis as follows. Define the backward transition function $pre(C)\equiv\{w:\exists w'\in C.\ w\rightarrow w'\}$, which would preserve regularity when the forward transition relation is regular. Given a regular set $B$ of the bad configurations, let $X_0\equiv B$ and $X_{n+1}\equiv X_n\cup pre(X_n)$ for $n\ge 0$. Define $X\equiv\bigcup_{i\ge 0}X_i$. Note that $X$ is the set of configurations backward reachable from $B$, and thus is upward closed by Fact 2. By Lemma 4, we can construct another sequence $X_0',X_1',...$ converging to $X$ by defining $X_n'\equiv uc(X_n).$ Each $X_{n+1}'$ can be computed from $X_n'$ for $n\ge0.$ Hence, by Lemma 2, the fixed point $X$ can be computed within a finite number of steps. Since $T^*(I)\cap B\neq\emptyset$ if and only if $X\cap I\neq\emptyset$, the reachability problem is decidable. ☐
Remark. The above proof actually gives an algorithm to construct the reachability set. However, the algorithm relies on Higman’s Lemma for termination and thus the time complexity is not primitive recursive [8,9].

Now we proceed to show that the reachability set of a lossy channel system, albeit regular, is not computable. Given a system $(I,T)$ and a word $w$, the recurrent state problem asks whether there exists an infinite trace from $I$ that visits $w$ infinitely often.
Theorem 3. [6] The recurrent state problem is undecidable for lossy channel systems.

To solve the recurrent state problem it suffices to check $w \in T^*(I)$ and $w \in T^*(\{w\})$. Hence, if these two questions are decidable then so is the recurrent state problem, leading to a contradiction with Theorem 3. Therefore, we can conclude that there exists no procedure that computes a finite-state automaton (or any symbolic representation allowing effective membership query) for $T^*(I)$.
Corollary. There exists a regular transition system $(I,T)$ such that $T^*(I)$ is regular but not computable.
Remark. Does the above corollary holds when $T$ is length-preserving? I didn't find any result about this at the time I was writing this post.

Discussion. The proof of Theorem 2 relies on properties of the subword ordering (or a well-quasi-ordering in general) to assert that backward search always terminates. In fact, reachability can be shown both r.e. and co-r.e. whenever a regular proof exists: just launch two procedures at the same time, one enumerating all possible counter-examples and one enumerating all possible proofs. It is clear that exactly one of the two procedures will terminate. (Here a counterexample is an execution path from $I$ to $B$, and a proof is a regular set $P$ satisfying the following three proof rules: i) $I\subseteq P$, ii) $T(P)\subseteq P$, and iii) $P\cap B=\emptyset.$) In particular, reachability is decidable for a transition system whenever the set of reachable configurations is regular.
More generally, the above argument works whenever a "regular" symbolic proof exists and the one-step image $T(X)$ or pre-image $T^{-1}(X)$ can be computed effectively from $X$. The "regularity" here refers to the existence of any finitary representations that are computable and closed under complement and intersection. This argument has been applied to prove decidability results for transition systems such as Petri nets and lossy counter systems [10]. See [11] for a general discussion on this kind of proof techniques.

References and further reading

1. Transitive Closures of Regular Relations for Verifying Infinite-state Systems, 2000.
2. Unreliable Channels are Easier to Verify than Perfect Channels, 1996.
3. On-the-fly Analysis of Systems with Unbounded, Lossy FIFO Channels, 2005.
4. Effective Lossy Queue Languages, 2001.
5. Undecidable Problems in Unreliable Computations, 2003.
6. Undecidability of Verifying Programs with Unreliable Channels, 1996.
7. Verifying Systems with Infinite but Regular State Spaces, 1998.
8. Post Embedding Problem is not Primitive Recursive, 2007.
9. The Ordinal Recursive Complexity of Lossy Channel Systems, 2008.
10. Lossy Counter Machines Decidability Cheat Sheet, 2010.
11. A unified approach for studying the properties of transitions systems, TCS, 1982.
12. On the regular structure of prefix rewriting. TCS, 1992.

A note on parallelizable functions

Yesterday I was accidentally asked that what kind of problems can be benefited the most from distributed computing frameworks such as MapReduce. I responded immediately that any problem that can be tackled by divide-and-conquer strategies should fit in the framework. However, on second thought, I found the answer missing the point because it remains unclear as to what kind of problems are solvable by divide and conquer. For example, sorting can be done in this way because sort(a++b) can be obtained from sort(a) and sort(b). How about the Boolean function is_sorted? The value of is_sort(a++b) can not be determined merely from the return values of is_sort(a) and is_sort(b). So there must be some characteristics that tell sort and is_sort apart.
Let's call a function parallelizable if it can be computed by divide and conquer. It is possible to "lift" a non-parallelizable function to a parallelizable one, such that the output of the original function can be obtained from that of the lifted function. In the above example, function is_sort can be made parallelizable by augmenting its return value with additional information max(s) and min(s) for input list s, since $a$$+\!\!+$$b$ is sorted in ascending order if and only if $a$ and $b$ are sorted in ascending order and $\max(a)\le \min(b)$. This parallelization is also effective because it reduces the time complexity from linear to logarithmic in appropriate computation models. So here we can ask several interesting questions: 1) What functions are parallelizable? 2) Is it always possible to lift a non-parallelizable function to a parallelizable one? 3) Do parallelizable functions always have efficient parallel implementations?

Homomorphism and Parallelism

After a brief survey, I found the rough ideas in my mind actually fall into a popular line of research over a long period of time. Particularly, there is a well-known result connecting homomorphisms with functions that admit divide-and-conquer imple-mentations.
Definition. A function $f : [A]\rightarrow B$ is $\odot$-homomorphic for operator $\odot:B\times B\rightarrow B$ if $f(s$$+\!\!+$$t) = f(s)\odot f(t)$ for any lists $s$ and $t$ on $[A]$, the set of finite lists of type $A.$
Note that the definition implies that $\odot$ is associative on $B$, since $+\!\!+$ is associative on $[A].$ Also, $f([\ ])$ is a unit of $\odot$ if $f$ is defined on $[\ ]$, which is a unit of $+\!\!+$ on $[A]$.
The First Homomorphism Theorem. ([1]) A function $f : [A]\rightarrow B$ can be computed by divide and conquer if and only if it is $\odot$-homomorphic for some $\odot$ on $B$.
It is clear that the $\odot$ operator captures the semantic of "combine" in a divide-and-conquer algorithm. In MapReduce, the conquer phase is done by a mapper and the combine phase by a reducer. However, as MapReduce does not specify the order of reduction, the $\odot$ operator (i.e. the reducer) has to be commutative for the outcome to be deterministic [2].
The above theorem tells us that a function is parallelizable iff it is homomorphic. Interestingly, it turns out that any non-homomorphic function can be trivially lifted to a homomorphism using a trick called "tupling". For example, this trick would lift $is\_sort: [Num]\rightarrow Bool$ to a function $is\_sort': [Num]\rightarrow [Num]\times Bool$ that is $\odot$-homomorphic with respect to $(s, a)\odot (t, b) \equiv (s$$+\!\!+$$t,\ is\_sort(s$$+\!\!+$$t))$. The parallel implementation based on this lift is clearly no better than its sequential counterpart. Similarly, $sort:[Num]\rightarrow[Num]$ is $\odot$-homomorphic when $\odot$ is defined by $s \odot t \equiv sort'(s$$+\!\!+$$t)$, where $sort'$ can be any sorting algorithm such as insertion sort, though the resulted parallel algorithm is inefficient and useless. Therefore, finding an efficient parallel implementation for a function, parallelizable or not, amounts to finding a $\odot$ operator with low computation costs. (To be continued)

References

1. Bird, Richard S. "An introduction to the theory of lists." 1987.
2. Chen, Y. F., et al. "Commutativity of Reducers." 2015.

DFA as proof for (recurrent) unreachability

Is this post we discussed how to prove unreachability problem $f^*(I)\cap B=\emptyset$ in an infinite-state transition system. In particular, we used the L* learning algorithm to learn a regular inductive invariant. In order to answer membership queries, we put a restriction that the transition relation $f$ is length-preserving, such that it is decidable to check whether a given configuration is reachable. Is putting this restriction the only way to make learning a proof possible? In this post, we shall discuss an elegant learning framework that can be applied to prove not only unreachability (aka. safety verification) but also recurrent unreachability (aka. liveness verification). We begin with briefly recapitulating the definitions.

Learning to prove unreachability for non-length-preserving systems

Given a finite set $\Sigma$ and a binary relation $f:\Sigma^* \to \mathcal P(\Sigma^*)$, define $F:\mathcal P(\Sigma^*) \to \mathcal P(\Sigma^*)$ by $F(S):= \bigcup_{v\in S}f(v).$ A binary relation is called regular if it can be accepted by an FA over $(\Sigma\cup\{\epsilon\})\times(\Sigma\cup\{\epsilon\}).$ Given two regular sets $I$ and $B$ and a regular relation $f$, the unreachability problem $(I,F,B)$ asks whether $B$ is unreachable from $I$ through $F$, namely, $F^*(I)\cap B=\emptyset.$ A proof for unreachability is a set $P\subseteq \Sigma^*$ satisfying $I\subseteq P$, $f(P)\subseteq P$, and $P\cap B=\emptyset.$ Such a set exists iff $B$ is unreachable from $I$.
Suppose we want to find a proof using the L* learning algorithm. In order to make membership queries decidable, Vardhan [1] proposed to learn, instead of the set of configurations, the set of configuration-witness pairs, where a witness refers to the number of steps needed to reach a configuration from the initial configurations. More precisely, in Vardhan's framework, the proof we aim to learn is a regular subset $W$ of $\Omega:=(\Sigma\cup\{\bot\})\times\{0,1\}$ ($\bot$ is the padding symbol). Each word in $W$ encodes a pair $(c,n)$ such that $c$ is a configuration and $c\in F^n(I)$. We shall use $[c,n]$ to denote the encoding of $(c,n).$ Now, given $I,f,B$, we shall consider an unreachability problem for $I',f',B'$ such that
$\begin{eqnarray*}
I' & := & \{[c,0]: c\in I\};\\
f'(S) &:=& \{[f(c),n+1]: [c,n]\in S\};\\
B' &:= & \{[c,n]:c\in B, n\ge 0\}.
\end{eqnarray*}$
Note that if the sets $I,f,B$ are regular then so are the sets $I',f',B'$.
It is straightforward to learn a proof for unreachability problem $(I',F',B')$ using L*: membership query is decidable thanks to the presence of witness, and equivalence query can be answered as we did before, aiming to find an inductive invariant as an over-approximation. After L* learns a proof for the new problem, we obtain a proof for the original problem by projection. However, note that the transformation from configurations to configuration-witness pairs doesn't preserve regularity. Hence, the transformed problem $(I',F',B')$ doesn't necessarily have a regular proof even when the original problem $(I,F,B)$ does (in which case the problem is decidable). In particular, our previous technique guarantees to terminate when $F^*(I)$ is regular, while the technique presented here doesn't.  It would be interesting to characterise the classes for which this technique is effective, namely, the classes where regularity of $F^*(I)$ implies that of $F'^*(I')$.

Learning to prove recurrent unreachability for length-preserving systems

The notion of "learning configuration-witness pairs instead of configurations" can also be applied to learn proofs for recurrent unreachability. Given $I,f,B$ as before, we say $B$ is recurrently reachable from $I$ iff there exists $w\in I$ such that the trace $f*(w)$ visited $B$ infinitely often. To prove recurrent unreachability, a witness needs to make it decidable to check whether a configuration is visited i.o. from $I$. This doesn't look possible as a single witness would then need to encode an infinite amount of information. (Recall that a witness for reachability only needs to encode a finite path.) For length-preserving systems, however, a counterexample to recurrent reachability is a lasso-shaped path and hence has a finite encoding. In fact, we can apply the well-known liveness-to-safety reduction for regular model checking to translate a recurrent reachability problem to a unreachability problem. More precisely, given a length-preserving transition system $(I,T,F)$ over alphabet $\Sigma$, we can specify a unreachability problem $(I',T',B')$ over alphabet $\Sigma\times\Sigma$ where
$I' := F\times F$,
$T' := \{((u,v),(u,w)) : u\in\Sigma^* \wedge |u|=|v| \wedge (v,w) \in T\}$, and
$B' := (T^*(I) \cap F)\times(T^*(I) \cap F)$.
Observe that $B'$ is reachable from $I'$ in $(I',T',B')$ iff $F$ can be visited infinitely often from $I$ in $(I,T,F)$. Even though $B'$ is in general not computable, the unreachability problem is still amenable to the automata learning method introduced in our last post. To see this, suppose that the learner has made an equivalence query for a candidate proof $P$. If either $T'(P)\subseteq P$ or $I'\subseteq P$ fails, a counterexample for the query can be computed as before. To check whether $P ∩ B = ∅$, we first check whether there is some $y \in P \cap (F\times F)$. If no such $y$ exists, then $P$ is a proof for the unreachability problem. Otherwise, we proceed to check whether $y \in T'^*(I')$, which is decidable since $T'$ is length-preserving. If $y \in T'^*(I')$, then $y$ is a witness for the fact that $B'$ is reachable from $I'$. Otherwise, we can use $y$ as a counterexample for the equivalence query.

DFA as proof for unreachability

Preliminaries. Given a finite set $\Sigma$ and a binary relation $f:\Sigma^* \to \mathcal P(\Sigma^*)$, we would use $F$# to denote the set function $\mathcal P(\Sigma^*) \to \mathcal P(\Sigma^*)$ defined by $F(S):= \bigcup_{v\in S}f(v).$ Also,$$F^0(S):= S;\quad F^{n+1}(S):= F(F^n(S))\cup F^n(S);\quad F^*(S):= \bigcup\nolimits_{n\ge 0} F^n(S).$$Intuitively, $F^*(S)$ is the set reachable from $S$ by applying $f$ to $S$ finitely many times. A binary relation is called regular if it can be recognised by a finite automaton over alphabet $(\Sigma\cup\{\epsilon\})\times(\Sigma\cup\{\epsilon\}).$
Unreachability analysis. Suppose $I$ and $B$ are two regular sets and $f$ is a regular relation. The unreachability problem $(I,F,B)$ asks whether $B$ is unreachable from $I$ through $F$, namely, $F^*(I)\cap B=\emptyset$. In software verification, many safety properties of a software can be modelled as (un)reachability problems [1] for an infinite state system. Particularly, the semantics of a program is modelled by a binary relation over configurations $\Sigma^*.$ If we let $I$ and $B$ denote the sets of the initial and the bad configurations, respectively, then $F^*(I)\cap B=\emptyset$ means that the execution of the program would never go wrong.
Tractability. Given $(I,F,B)$, $F^*(I)$ is not necessarily regular even though $F^n(S)$ is regular for all $n\ge0.$ Also, most interesting properties about $F^*(S)$ are undecidable. This fact is not surprising as the transition relation of a Turing Machine is regular*. To make the verification problem more tractable, we assume that $f$ is length-preserving, i.e., $w\in f(u)$ only if $|w|=|u|$, which weakens the expressive power of the transition system $(I,f)$ from a Turing machine to a linear-bounded automaton (LBA), which is only allowed to work with the amount of space occupied by the input string. Membership of $F^*(I)$ becomes decidable with the length-preserving restriction, but unreachability remains undecidable, as $LBA\cap DFA=LBA$ and checking emptiness of LBA is undecidable. This follows from the fact one can encode a given TM $T$ as an LBA $A$ such that $L(A)$ consists of precisely the halting runs of $T$.
Remark. While a regular transition system is as powerful as a TM (which can compute functions like $f(w)=w\#w$), not all transition systems are regular. For example, transition systems induced by higher-order pushdown automata allow transitions like $w \to w\#w$ and are thus not regular.
Regular proof synthesis. While the problem is undecidable, we can given a positive answer to it as long as we can find a proof . Such a proof can be a set $S$, called an inductive invariant, that satisfies $B\cap S=\emptyset$ and $F^*(I)\subseteq S.$ Recall that in this post we introduced L*, an algorithm that can learn a DFA by querying the target language. Below, we try to construct a teacher for L* to learn a regular proof for unreachability problem $(I,F,B).$ Upon a membership queries for word $w$, the teacher checks if $I$ is reachable from $w$ through $f^{-1}$. This check is decidable thanks to the assumption that $f$ is length-preserving, which guarantees that a word is only reachable from a finite number of words. Upon an equivalence query for DFA $A$, the teacher performs the following 4 steps in turn:

Step 1. If $\exists w\in I\setminus L(A)$ then return $w$.  // check that $I\subseteq L(A)$)
Step 2. If $\exists w\in L(A)\cap B$ then halt and report "reachable" if $Mem(u)=yes$; return $w$ otherwise.  // check that $L(A)$ doesn't overlap $B$
Step 3. If there exist $u\in L(A)$ and $w\in f(u)\setminus L(A)$, then return $w$ if $Mem(u)=yes$ and return $u$ otherwise.  // check that $L(A)$ is inductive
Step 4. Halt and report "unreachable".

If a candidate DFA $A$ passes Step 1-3, then $L(A)$ is clearly an inductive invariant. Observe that each counterexample falls in the symmetric difference of $L(A)$ and $F^*(I).$ When $F^*(I)$ is regular, it follows from the complexity results of L* that an inductive invariant can be learnt with at most $n$ equivalence queries, where $n$ is the number of states in the minimal DFA of $F^*(I)$, and at most $m\!\cdot\!(n+1)$ membership queries, where $m$ is an upper-bound on the length of the counter-examples returned by the teacher. Here we have several notes in order:
On the length-preserving restriction. We have assumed that the transition relation preserve lengths. In this way, a bad configuration is reachable from some initial configuration if and only if it can be reached within a bounded memory. This restriction is not essential for practical unreachability analysis as long as we allow "padding" in the initial set. That is, for every word in the initial configurations, say $w$, we would pad it with an arbitrary number of placeholders, say $\bot$, so that $w\in I$ implies $w\bot^*\subseteq I$. In this way, the size of available memory for computing $w$ is finite but effectively unbounded. On the other hand, though length-preserving relations are powerful enough to model many useful transition systems, they cannot model systems that require $\epsilon$ in their alphabet, such as lossy channel machines.
Minimality of proof. While L* always learns a minimal DFA by the Myhill-Nerode theorem, here it does not necessarily learn the minimal inductive invariant in terms of set inclusion. Instead, depending on the counterexamples returned by the teacher, L* would try to learn one of the inductive invariants and, when it found one, it learns the minimal DFA for that particular invariant.
Completeness of the method. When $F^*(I)$ is regular, L* is guaranteed to find a proof. When $F^*(I)$ is not regular, however, our method may not find a regular proof even when one exists. On the other hand, checking unreachability is in fact decidable when a regular proof exists, since we can launch two procedures at the same time, one looking for a counterexample and one looking for a proof. From this aspect, L* learning is weaker in completeness than brute force enumeration. (Note that finding a DFA for $F^*(I)$ may still be undecidable even when $F^*(I)$ is regular.)
A non-terminating example. Consider an unreachability problem $(I,F,B)$ where $I:=\{(ab)^n:n\ge 1\}$, $f:= \{(xbay, xaby): x,y\in \{a,b\}^*\}$, and $B$ is some trivial set such as $\emptyset.$ Note that $F^*(I)$ is not regular, since $F^*(I)\cap a^*b^*=\{a^nb^n:n\ge1\}$ is not regular. Now consider a Teacher implementing Step 1-4 for equivalence queries that would return a shortest counterexample for the candidate proof. Below we list the queries and the automata $A$ learnt by L* in each iteration.
Iteration 1: $A=\emptyset$; containment check of $I$ fails with counterexample $ab$; add $ab.$
Iteration 3: $A=a(ba)^*b$; inductiveness check fails at $abab \to aabb$; add $aabb.$

digraph finite_state_machine {
rankdir=LR;
size="8,5"
node [shape = doublecircle]; 3 ;
node [shape = circle];
1 -> 2 [ label = "a" ];
2 -> 3 [ label = "b" ];
3 -> 2 [ label = "a" ];
"init" [shape = point];
"init" -> 1;
}

Iteration 4: $A=a(ba|ab)^*b$; inductiveness check fails at $aababb \to aaabbb$; add $aaabbb.$

digraph finite_state_machine {
rankdir=LR;
size="8,5"
node [shape = doublecircle]; 4 ;
node [shape = circle];
2 -> 3 [ label = "b" ];
1 -> 3 [ label = "a" ];
3 -> 2 [ label = "a" ];
3 -> 4 [ label = "b" ];
4 -> 3 [ label = "a" ];
"init" [shape = point];
"init" -> 1;
}

Iteration 5: $A=a(ba|a(ab)^*b)^*b$; inductiveness check fails at $aaababbb \to aaaabbbb$; add $aaaabbbb.$

digraph finite_state_machine {
rankdir=LR;
size="8,5"
node [shape = doublecircle]; 5 ;
node [shape = circle];
2 -> 3 [ label = "b" ];
3 -> 2 [ label = "a" ];
3 -> 4 [ label = "b" ];
1 -> 4 [ label = "a" ];
4 -> 3 [ label = "a" ];
4 -> 5 [ label = "b" ];
5 -> 4 [ label = "a" ];
"init" [shape = point];
"init" -> 1;
}

One can observe that L* got trapped from the 3rd iteration - it keeps splitting state 2, creating a lineage that leads to a divergent sequence of counterexamples. On the other hand, L* has indeed tried its best after the 3rd iteration: each time L* receives a counterexample of length $2n$, it succeeds to find an inductive proof for the reachable configurations of length $\le 2n$, namely $A_n:=\{w\in \{a,b\}^*:|w|\le n$ and $0\le$#$a-$#$b\le n$ in all prefixes of $w \}.$ Note that $|A_{n+1}|=|A_{n}|+1.$ Due to the fact that L* progresses incrementally in terms of automata size, and that $a^{n+1}b^{n+1}$ is the shortest counter-example for $A_n$, L* will never reach an automaton covering all possible $A_n$.

Learning with witnesses. We have discussed how to use the L* learning algorithm to prove $F^*(I)\cap B=\emptyset$. In order to answer membership queries, we assumed that the transition relation is length-preserving. However, it is possible to use L* without this assumption. For example, Vardhan et al. [3] proposed to learn a set of configuration-witness pairs as a proof, where a witness refers to the number of steps needed to reach a configuration. More precisely, the proof they proposed to learn is a regular subset of $((\Sigma\cup\{\bot\})\times\{0,1\})^*$, where $\bot$ serves as a padding symbol. Each word in this set encodes a pair $(c,n)$, meaning that $c$ is a configuration contained in $F^n(I)$. Let $[c,n]$ denote the encoding of $(c,n).$ Given $I$, $f$, and $B$, we define $I'$, $f'$, and $B'$ as
$\begin{eqnarray*}
I' & := & \{[c,0]: c\in I\};\\
f'(S) &:=& \{[f(c),n+1]: [c,n]\in S\};\\
B' &:= & \{[c,n]:c\in B, n\ge 0\}.
\end{eqnarray*}$
Note that if $I$, $f$, and $B$ are regular then so are $I'$, $f'$, and $B'.$
It is straightforward to learn a proof for unreachability problem $(I',F',B')$ using L*: membership query is decidable thanks to the presence of witness, and equivalence query can be answered as we did before, aiming to find an inductive invariant as an over-approximation. After L* learns a proof for the new problem, we obtain a proof for the original problem by projection. However, note that the transformation from configurations to configuration-witness pairs doesn't preserve regularity. Hence, the transformed problem $(I',F',B')$ doesn't necessarily have a regular proof even when the original problem $(I,F,B)$ does. In particular, unlike the previous method, the learning process here doesn't guarantee to terminate when $F^*(I)$ is regular. It would be interesting to characterise the classes for which this technique is effective, namely, the classes where regularity of $F^*(I)$ implies that of $F'^*(I')$.

References

1. A unified approach for studying the properties of transitions systems, TCS 1982.
2. Learning to prove safety over parameterised concurrent systems, FMCAD 2017.
3. Learning to verify safety properties, ICFME 2004.

A note on induction and coinduction

$\newcommand{\bigsqcap}{\mathop {\huge \huge ⨅}}$ $\newcommand{\lfp}{{\sf lfp}}$ $\newcommand{\gfp}{{\sf gfp}}$

An illustrative example. Consider a context-free grammar (CFG) with start symbol $S$, alphabet $\Sigma=\{0,1,2\}$, and the following production rules:\begin{equation}S\rightarrow 0\ |\ 1\ |\ 0S\ |\ 1S\label{eg1-cfg1}\end{equation}A CFG is conventionally interpreted inductively, which means a string belongs to a grammar's language if and only if it can be transformed from the start symbol through a finite number of rule applications. Hence, the language of the above grammar is $\{0,1\}^+$, for this set contains exactly the strings in $\Sigma$ that can be derived from $S$. On the other hand, a grammar can also be interpreted coinductively, meaning that a string belongs to the a grammar's language if and only if its existence is consistent with the grammar rules. In this sense, a string is in the language of \eqref{eg1-cfg1} if and only if it is of one of the forms 0, 1, $0x$ or $1x$, and, therefore, the language of the grammar is $\{0,1\}^+\cup\{0,1\}^\omega$, the set of nonempty strings comprised of 0's and 1's. Note that any string containing 2 is not in the language, since if $x2y=\{0,1\}\cdot z$ is in the language, then so is a string $x'2y$ with $|x'| = |x| - 1$ and this will eventually lead to a contradiction. Now consider another CFG as follows:\begin{equation}S\rightarrow 0\ |\ 1\ |\ S\ |\ SS\label{eg1-cfg2}\end{equation}It is clear that grammars \eqref{eg1-cfg1} and \eqref{eg1-cfg2} produce the same language when they are interpreted inductively. However, if a coinductive interpretation is taken, then the language of \eqref{eg1-cfg2} will become $\Sigma^\omega$ since any string satisfies rule $S \rightarrow S$. In short, an inductive interpretation of a set of rules looks for the minimal satisfying set (a string is in the language iff it can be derived via the rules), while a coinductive interpre-tation looks for a maximal one (a string is in the language iff it doesn't violate the rules).
The concepts of induction and coinduction can be unified in order theory. To see this, fix a countable domain $D$ and consider a predicate $Q: D \rightarrow \{true,false\}$. We shall use $Q$ to capture the minimal set of elements satisfying a set of recurrent equations. For example, the language induced by grammar \eqref{eg1-cfg1} can be captured by $Q$ with $D=\Sigma^\omega$ and recurrent equations $Q(0)=true$, $Q(1)=true$, $Q(0x)=Q(x)$, and $Q(1x)=Q(x)$, such that a string $x$ is in the language iff $Q(x)=true$. Now we rewrite these equations by replacing the $Q$'s on the left-hand side of each equation with a functional $F$ over $D\rightarrow \{true,false\}$, obtaining a set of equations defining $F$: \begin{equation}F(Q)(0)=true;\quad F(Q)(1)=true;\quad F(Q)(0x)=Q(x);\quad F(Q)(1x)=Q(x).\label{eg1-fp1}\end{equation}Consider the (standard) complete lattice $(D\rightarrow \{true,false\},\ \sqsubseteq)$ of predicates where $(Q_1\sqcap Q_2)(d) = Q_1(d)\wedge Q_2(d)$, $(Q_1\sqcup Q_2)(d) = Q_1(d)\vee Q_2(d)$, $\bot$ maps all $d\in D$ to $false$, $\top$ maps all $d\in D$ to $true$, and $Q_1 \sqsubseteq Q_2$ means $Q_1(d)\Rightarrow Q_2(d)$ for all $d\in D$. Observe that $F$ is a monotone function on this lattice: $Q_1 \sqsubseteq Q_2 \Rightarrow F(Q_1) \sqsubseteq F(Q_2)$. Hence, by Tarski's Fixed Point Theorem, $F$ has a least fixed point (denoted by $\lfp(F)$) and a greatest fixed point (denoted by $\gfp(F)$). The relationship between these fixed points is$$\bot\sqsubseteq F^k(\bot)\sqsubseteq \bigsqcup\nolimits_n F^n(\bot) \sqsubseteq \lfp(F) \sqsubseteq \gfp(F) \sqsubseteq \bigsqcap\nolimits_n F^n(\top) \sqsubseteq F^k(\top) \sqsubseteq \top.$$Take the $F$ defined in \eqref{eg1-fp1} as an example. $F^n(\bot)$ captures the set of strings that can be derived from grammar \eqref{eg1-cfg1} with a parse tree of height less than $n+1$. Furthermore, since each equation only has a finite number of $Q$'s on the right-hand side, $F$ is in fact a Scott continuous function and thus $\lfp(F)=\bigsqcup_n F^n(\bot)$, i.e., $\lfp(F)(x)=true$ iff $x \in\{0,1\}^+$, the set of strings that can be derived from $S$ in a finite number of steps. To find $\gfp(F)$, define $A_n=\{$nonempty binary strings of length less than $n+1\}$ and $B_n=\{$infinite strings in $\Sigma^*$ containing a binary prefix of length less than $n+1\}$. Observe that $F^n(\top)$ captures the set $A_n \cup B_n$, $F^n(\top) \sqcap F^{n+1}(\top)$ captures the set $A_{n+1} \cup B_{n+1}$. Thus $\bigsqcap\nolimits_n F^n(\top)$ will capture the set $\lim_{n\rightarrow\infty}(A_n\cup B_n)$ if the limit exists. However, since $A_n \nearrow \{0,1\}^+$ and $B_n \searrow\{0,1\}^\omega$, we have $$\limsup_{n\rightarrow\infty}(A_n\cup B_n) = \bigcap_{n\ge 1}\bigcup_{k\ge n} (A_k \cup B_k) = \bigcap_{n\ge 1}(\{0,1\}^+\cup B_n) = \{0,1\}^+\cup\{0,1\}^\omega,$$and$$\liminf_{n\rightarrow\infty}(A_n\cup B_n) = \bigcup_{n\ge 1}\bigcap_{k\ge n} (A_k \cup B_k) = \bigcup_{n\ge 1}(A_n \cup \{0,1\}^\omega) = \{0,1\}^+\cup\{0,1\}^\omega.$$It follows that $\lim_{n\rightarrow\infty}(A_n\cup B_n)=\{0,1\}^+\cup\{0,1\}^\omega$, which is also the set captured by $\gfp(F)$ as $F$ is Scott continuous.
Proof by induction. In mathematical induction, we usually set $D=\mathbb N\cup\{0\}$ and try to prove that $Q(0)$ holds and $Q(n)\Rightarrow Q(n+1)$ for all $n\ge 0$. Generally, proving a property $Q$ by induction amounts to proving that $Q$ holds in the base cases and $Q(d)\Rightarrow F(Q)(d)$ for all $d\in D$. The predicate $Q$ satisfying this proof rule turns out to be $\bigsqcup_n F^n(\bot)$, which, when $F$ is Scott continuous, agrees with the least fixed point of $F$. In this sense, proving by induction usually corresponds to taking the least fixed point. In program verification, inductions and least fixed points are extensively used to reason about semantics, because the semantics of a program should precisely describe what will happen during the evaluation of the program.
Proof by coinduction. Suppose $Q$ is the greatest fixed point of $F$. By definition, any predicate $Q'$ satisfying $Q' \sqsubseteq F(Q')$ also satisfies $Q' \sqsubseteq Q$, since $Q$ is an upperbound of any ascending chain in the lattice. Hence, to show $Q(d)$ holds it suffices to find some predicate $Q'$ such that $Q'(d)$ holds and $Q'(d')\Rightarrow F(Q')(d')$ for all $d' \in D$. The rationale behind doing this is to regard the idea of being acceptable (i.e., $Q(d)$ holds) as being consistent with the induction rules (i.e., $\exists Q': Q'(d) \wedge Q'(d')\Rightarrow F(Q')(d')$ for all $d'$). In program verification, coinductions and greatest fixed points are extensively used to check consistence with specifications, because the specification of a program should not forbid a behaviour unless it explicitly specifies so.
Collapse of fixed points. The least fixed point and the greatest fixed point in a complete lattice can coincide when Banach's Fixed Point Theorem can be applied. Namely, a "contractive" operator in a metric space has a unique fixed point. A functional $F$ will be contractive if there exists a well-founded relation $\prec$ on $D$ such that the clause of $F(Q)(d)$ only call $Q$ on arguments smaller than $d$ with respect to $\prec$. For example, the $F$ defined in \eqref{eg1-fp1} is contractive when $D$ is set to $\Sigma^*$; in such case, both $\lfp(F)$ and $\gfp(F)$ capture $\{0,1\}^+$. By contrast, the functional that expresses grammar \eqref{eg1-cfg2}, i.e., the functional $F$ that satisfies\begin{equation}F(Q)(0)=true;\ F(Q)(1)=true;\ F(Q)(x)=Q(x);\ F(Q)(xy)=Q(x)\wedge Q(y),\label{eg1-fp2}\end{equation}is not contractive even when $D=\Sigma^*$. Indeed, one can see that $\lfp(F)$ captures $\{0,1\}^+$ but $\gfp(F)$ captures $\{0,1\}^*$.

Inductive and coinductive datatypes

An introduction to (co)algebra and (co)induction.
https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/notes/20150126_coinduction.txt
http://wiki.c2.com/?CoinductiveDataType

Some interesting proofs using oracles

A proof with oracles exploits the following two facts about Turing Machines (TMs): 1) there exist effective representations of TMs as strings, and 2) a TM can simulate other TMs taking their representation as input. Any argument that only relies on these two facts about TMs treats them as black boxes. This post tries to collect some results with interesting oracle proofs that sketches the proof ideas.$\newcommand{\P}{{\sf P}}$ $\newcommand{\NP}{{\sf NP}}$ $\newcommand{\PSPACE}{{\sf PSPACE}}$ $\newcommand{\EXPTIME}{{\sf EXPTIME}}$
Diagonalization. Any proof exploiting diagonalization proof techniques to prove properties of TMs is a proof with oracles. A well-known application of this proof techniques is to show that the Halting problem is undecidable. That is, generally, no TM can determine whether a TM will halt on a string. The key factors leading to this result are precisely the two facts stated earlier: any TM can be represented as a string, and a TM can simulate another TM based on its string representation. To see that the Halting problem is undecidable, suppose to the contrary that we can decide whether $M$ halts on $x$ for any $M$ and $x$. (It is a convention to regard $M(x)$ as diverging if $M$ is not a valid TM.) Define a TM $N$ such that $N(M)$ halts if $M(M)$ diverges, and $N(M)$ loops if $M(M)$ halts. After some speculation, one can see that it is impossible to determine whether $N(N)$ halts, contradicting to our assumption.

Fixed-Point Theorem. Two TMs $A$ and $B$ are called semantically equivalent, denoted by $A\simeq B$, iff $A(x)=B(x)$ for any string $x$ (set $M(x):=\nearrow$ if a TM $M$ diverges on $x$). We claim that if $f$ is a TM mapping TMs to TMs, then $f$ has a fixed point, i.e., there exists a TM $M$ such that $f(M)\simeq M$. The key to prove this claim is to consider a special TM $G(M):=M(M)$. More precisely, given string $M$, $G(M)$ is a TM that loops on any input when $M(M)$ is not a valid TM, and produces $M(M)(x)$ on input $x$ otherwise. Somehow we guess that a fixed point occurs at $G(N)$ for some TM $N$. Writing down the equation $f(G(N))\simeq G(N)\simeq N(N)$ with unknown $N$, one finds that $N:=f\circ G$ is a solution and thus $G(f\circ G)$ is a fixed point of $f$. By using integers as an encoding of TMs and taking the convention that $M(x):=\nearrow$ on all $x$ when $M$ is not a valid TM, we obtain Rogers' Fixed-Point Theorem: Any total computable function has a fixed point.

P vs NP. A canonical example used to show the power of proofs with oracles is to show that the $\P$ vs $\NP$ problem doesn't relativize. That is, there exist oracles $A$ and $B$ such that a) $\P^A=\NP^A$ and b) $\P^B\neq \NP^B$. First, note that any $C$ oracle such that $\NP \subseteq C$ and $C=\texttt{co}C$ can serve as $A$. For example, $C$ can be $\PSPACE$ or $\EXPTIME$. For such $C$, $C\subseteq \P^A\subseteq \NP^A$ clearly holds. Further, $\NP^A\subseteq C$ holds as any machine in $\NP$ can be simulated in $C$ and any query to $A$ can be answered in $C$. To prove (b), we will construct an oracle $B$ such that language $L_B:=\{1^n: B$ accepts a string of length $n\}$ locates in $\NP^B \setminus \P^B$. To force $L_B \not\in \P^B$, we consider all oracle machines in $\P$ by labelling them as $M_1, M_2,....$ We hope that by the construction of $B$, there exists an integer $n_i$ for each $M_i$ such that $M_i^B$ accepts $1^{n_i}$ iff $1^{n_i} \not\in L_B$. This will then imply $L_B \not\in \P^B.$ The fact that $L_B \in \NP^B$ is clear, as $\NP^B$ can guess a string of size $n$ in $B$ by making at most $n$ non-deterministic queries to $B$.
Let $B_0=\emptyset$ and $n_0=0$. For each $i\ge 1$, we shall construct $B_i$ as follows. Let $n_i>n_{i-1}$ be any number larger than the maximal length of strings in $B_{i-1}$. Now simulate $M_i^{B_{i-1}}$ on $1^{n_i}$ for at most $2^{n_i}/3$ computation steps. If $M_i^{B_{i-1}}$ accepts $1^{n_i}$, then we set $B_i:=B_{i-1},$ which implies $1^{n_i}\not\in L_{B_i}$. If $M_i^{B_{i-1}}$ rejects $1^{n_i}$, then there exists a string $s$ of length $n_i$ not queried by $M_i^{B_{i-1}}$. Define $B_i:=B_{i-1}\cup\{s\}$, which implies $1^{n_i} \in L_{B_i}$. Hence, by construction, $M_i^{B_{i-1}}$ cannot decide the membership of $1^{n_i}$ in $L_{B_i}$ within $2^{n_i}/3$ steps. Define $B:=\bigcup_i B_i$. Observe that $B_i\nearrow B$ and $L_{B_i}\nearrow L_B$. Also, for any string $x$, $M^B(x)=M^{B_{i}}(x)$ as long as $M^B(x)$ terminates in $2^{n_i}/3$ steps. Note that every TM $M$ has infinitely many TMs that i) are semantically equivalent to $M$, ii) are of size arbitrarily larger than $M$, and iii) has the same running time as that of $M$. Since $n_i\nearrow\infty$ as $i\rightarrow\infty$, for each oracle machine $M$ in $\P$, there exists $i$ such that $M_i^B\simeq M^B$ and the running time of $M_i^B$ on $1^{n_i}$ is less than $2^{n_i}/3$. It follows that $M^B$ accepts $1^{n_i}$ iff $1^{n_i}$ is not in $L_B$, i.e., $M^B$ doesn't decide $L_B$. Hence, $L_B$ is a language in $\NP^B$ but not in $\P^B$.