This paper introduces a novel abstract interpretation framework for deciding language inclusion problems, leveraging overapproximations via quasiorders, applicable to regular, context-free, and other language classes, with connections to existing algorithms.
Contribution
It develops a general method using quasiorder-based overapproximations for deciding language inclusion, unifying and extending existing algorithms, and introduces a new fixpoint-based inclusion checking algorithm.
Findings
01
Decidability of language inclusion under certain abstraction conditions.
02
Systematic design of inclusion algorithms for various language classes.
03
Connection of new methods to existing antichain algorithms.
Abstract
We study the language inclusion problem L1⊆L2 where L1 is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by overapproximating the Kleene iterates of its least fixpoint characterization, is included in L2. We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees termination of least fixpoint computations). This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words "greater than or equal to" a given input word for that quasiorder. We put forward a range of such quasiorders that allow us to…
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Full text
Complete Abstractions for Checking Language Inclusion
We study the language inclusion problem L1⊆L2 where L1 is regular or context-free.
Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by overapproximating the Kleene iterates of its least fixpoint characterization, is included in L2.
We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees
termination of least fixpoint computations).
This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words “greater than or equal to” a given input word for that quasiorder.
We put forward a range of such quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets, and context-free languages into regular languages.
In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms like the so-called antichain algorithms.
Finally, we provide an equivalent language inclusion checking algorithm based on
a greatest fixpoint computation
that relies on quotients of languages and, to the best of our knowledge, was not previously known.
††copyright: acmcopyright††journal: TOCL††ccs: Theory of computation Regular languages††ccs: Theory of computation Grammars and context-free languages††ccs: Theory of computation Abstraction††ccs: Theory of computation Program reasoning††ccs: Software and its engineering Formal language definitions
1. Introduction
Language inclusion is a fundamental and classical problem (Hopcroft and
Ullman, 1979, Chapter 11) which consists in deciding, given two languages L1 and L2, whether L1⊆L2 holds. Language inclusion problems are found in diverse fields ranging
from compiler construction (Bauer and Eickel, 1976; Waite and Goos, 1984) to model checking (Baier and Katoen, 2008; Clarke
et al., 2018).
We consider languages of finite words over a finite alphabet Σ.
For regular and context-free languages, the inclusion problem is well known to be PSPACE-complete (see (Hunt
et al., 1976)).
The basic idea of our approach for solving a language inclusion problem L1⊆L2 is to leverage
Cousot and Cousot’s abstract interpretation (Cousot and Cousot, 1977, 1979) for checking the inclusion of an overapproximation (i.e., a superset) of L1 into L2.
This idea draws inspiration from the work of Hofmann and Chen (2014), who used abstract interpretation to decide language inclusion between languages of infinite words.
Let us assume that L1 is specified as least fixpoint of an equation system X=FL1(X) on sets of words in ℘(Σ∗), that is, L1=lfp(FL1)
is viewed as limit of the possibly infinite sequence of Kleene iterates {FL1n(∅)}n∈N of the transformer FL1.
An approximation of L1 is obtained by applying an overapproximation
for sets of words as modeled by a closure operator
ρ:℘(Σ∗)→℘(Σ∗). In abstract interpretation
one such closure ρ logically defines an abstract domain, which is here
used for
overapproximating a language by adding
words to it, possibly none in case of no approximation.
The language abstraction ρ is then used
for defining an abstract check of convergence
for the Kleene iterates of FL1 whose limit is
L1, i.e.,
the convergence of the sequence {FL1n(∅)}n∈N
is checked on the abstraction ρ by the condition ρ(FL1n+1(∅))⊆ρ(FL1n(∅)). If the abstraction ρ does not contain infinite ascending chains then we obtain finite convergence w.r.t. this abstract check for some
FL1N(∅).
Therefore, this abstract interpretation-based
approach finitely computes
an abstraction L1ρ=ρ(FL1N(∅)) such
that the abstract language inclusion check
L1ρ⊆L2 is
sound because
L1⊆L1ρ always holds.
We then give conditions on ρ which ensure a complete abstract inclusion
check, namely, the answer to L1ρ⊆L2 is always exact (no “false alarm” in abstract interpretation terminology):
(i)
L2 is exactly represented by the abstraction ρ, i.e., ρ(L2)=L2;
2. (ii)
ρ is a complete abstraction for symbol concatenation λX∈℘(Σ∗).aX, for all a∈Σ,
according to the standard notion of completeness in abstract interpretation (Cousot and Cousot, 1977); this entails that
ρ(L1)=L1ρ holds, so that L1ρ⊆L2 implies L1⊆L2.
This approach leads us to design a general algorithmic framework for language inclusion problems which is parameterized by an underlying language abstraction.
We then focus on language abstractions ρ which are
induced by a quasiorder relation on words ⩽⊆Σ∗×Σ∗. Here, a language L is overapproximated by adding all the words which are “greater than or equal to” some word of L for ⩽. This allows us to
instantiate the above conditions (i) and (ii)
for achieving a complete abstract inclusion check in terms of the quasiorder relation ⩽.
Termination, which corresponds to having finitely many Kleene iterates,
is guaranteed by requiring that
the relation ⩽ is a well-quasiorder.
We define well-quasiorders satisfying the conditions (i) and (ii) which are directly derived from the standard Nerode equivalence relations on words.
These quasiorders have been first investigated by Ehrenfeucht et al. (1983) and have been later generalized and
extended by de Luca and Varricchio (1994; 2011).
In particular,
drawing from a result by de Luca and Varricchio (1994), we show that the language abstractions induced by the Nerode quasiorders are the most general ones (intuitively, optimal) which fit in our algorithmic framework for checking
language inclusion.
While these quasiorder abstractions do not depend on some finite
representation of languages (e.g., some class of
automata),
we provide quasiorders which instead exploit an underlying language representation given by a finite automaton.
In particular, by selecting suitable well-quasiorders for the class of language inclusion problems at hand we are able to systematically derive
decision procedures of the inclusion problem
L1⊆L2 for the following cases:
(1)
both L1 and L2 are regular;
2. (2)
L1 is regular and L2 is the trace language of a one-counter net;
3. (3)
L1 is context-free and L2 is regular.
These decision procedures, here systematically designed
by instantiating our framework,
are then related to existing language inclusion checking algorithms.
We study in detail the case where both languages L1 and L2 are regular and represented by finite state automata.
When our decision procedure for L1⊆L2 is derived from
a well-quasiorder on Σ∗ by exploiting an automaton-based representation of L2, it turns out that
we obtain the well-known “antichain algorithm” by De Wulf et al. (2006).
Also, by including a simulation relation in the definition of the well-quasiorder we derive a decision procedure that partially matches the language inclusion algorithm by Abdulla et al. (2010), and in turn also that by Bonchi and Pous (2013).
It is also worth pointing out that for the case in which L1 is regular and L2 is the set of traces of a one-counter net, our systematic instantiation provides
an alternative proof for the decidability of the corresponding language inclusion problem (Jančar
et al., 1999).
Finally, we leverage a standard duality result between abstract least and greatest
fixpoint checking (Cousot, 2000) and put forward a greatest fixpoint approach (instead of the above least fixpoint-based procedures) for the case where both L1 and L2 are regular languages.
Here, we exploit the properties of the overapproximating abstraction induced by the quasiorder relation in order to show that
the Kleene iterates converging to the greatest fixpoint are finitely many.
Interestingly, the Kleene iterates of the greatest fixpoint are finitely many whether you apply the overapproximating abstraction or not, and this is shown
by relying on a second type of completeness in abstract interpretation
called forward completeness (Giacobazzi and
Quintarelli, 2001).
Structure of the Article
In Section 2 we
recall the needed basic notions and background on order theory, abstract interpretation and formal languages.
Section 3
defines a general method for checking the convergence of Kleene iterates on
an abstract domain, which provides the basis for designing in
Section 4 an abstract interpretation-based framework
for checking language inclusion, in particular by relying on abstractions
that are complete for concatenation of languages.
This general framework is instantiated in Section 5
to the class of abstractions
induced by well-quasiorders on words, thus yielding effective inclusion checking algorithms for regular languages and traces of one-counter nets.
Section 6 shows that
one specific instance of our algorithmic framework turns out to be equivalent to the well-known
antichain algorithm for language inclusion by De
Wulf et al. (2006).
The instantiation of the framework for checking the inclusion of context-free languages into regular languages is described in Section 7.
Section 8 shows how
to derive a new language inclusion algorithm
which relies on the computation of a greatest fixpoint rather than a least fixpoint.
Finally, Section 9 outlines some directions
for future work.
This article is an extended and revised version of the conference paper (Ganty
et al., 2019),
that includes full proofs, additional detailed examples, a simplification
of some technical notions, and a new application for checking the inclusion of context-free languages into regular languages.
2. Background
2.1. Order Theory
If X is any set then ℘(X) denotes its powerset.
If X is a subset of some universe set U then Xc denotes the complement of X with respect to U when U is implicitly
given by the context.
If f:X→Y is a function between sets and S∈℘(X) then f(S)≜{f(x)∈Y∣x∈S} denotes its image on a subset S. A composition of two functions f and g is denoted both by fg and f\compg.
⟨D,⩽⟩ is a quasiordered set (qoset) when ⩽ is a quasiorder (qo) relation on D, i.e. a reflexive and
transitive binary relation ⩽⊆D×D. In a qoset ⟨D,⩽⟩ we will
also use the following induced equivalence relation ∼D: for all
d,d′∈D, d\sim_{D}d^{\prime}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{\stackrel{{\scriptstyle{\mbox{\tiny△}}}}{{\Leftrightarrow}}}}d\leqslant d^{\prime}\>\wedge\>d^{\prime}\leqslant d.
A qoset satisfies the ascending (resp. descending) chain condition (ACC, resp. DCC) if there is no countably infinite sequence of distinct elements {xi}i∈N such that, for all i∈N, xi⩽xi+1 (resp. xi+1⩽xi).
A qoset is called ACC (DCC) when it satisfies the ACC (DCC).
A qoset ⟨D,⩽⟩ is a partially ordered set (poset) when ⩽ is antisymmetric.
A subset X⊆D of a poset is directed if X is nonempty and every pair of elements in X has an upper bound in X.
A poset ⟨D,⩽⟩ is a directed-complete partial order (CPO) if it has
the least upper bound (lub) of all its directed subsets.
A poset is a join-semilattice if it has the lub
of all its nonempty finite subsets (therefore
binary lubs are enough).
A poset is a complete lattice if it has
the lub of all its arbitrary (possibly empty) subsets; in this case, let us recall that
it also has the greatest lower bound (glb) of all its
arbitrary subsets.
An antichain in a qoset ⟨D,⩽⟩ is a subset X⊆D such that
any two distinct elements in X are incomparable for ⩽.
We denote the set of antichains of a qoset ⟨D,⩽⟩ by AC⟨D,⩽⟩≜{X⊆D∣X is an antichain}.
A qoset ⟨D,⩽⟩ is a well-quasiordered set (wqoset), and ⩽ is called well-quasiorder (wqo) on D, when for
every countably infinite sequence of elements {xi}i∈N there exist i,j∈N such that i<j and xi⩽xj.
Equivalently, ⟨D,⩽⟩ is a wqoset iff D is DCC and
D has no infinite antichain.
For every qoset ⟨D,⩽⟩, let us define the following binary relation ⊑⩽ on the powerset:
given X,Y∈℘(D),
[TABLE]
A minor of a subset X⊆D, denoted by ⌊X⌋, is a subset of the minimal elements of X w.r.t. ⩽, i.e. ⌊X⌋⊆min⩽(X)≜{x∈X∣∀y∈X,y⩽x⇒y=x}, such that
X⊑⌊X⌋ holds.
Therefore, a minor ⌊X⌋ of X⊆D is always an antichain in D.
Let us recall that every subset X of a wqoset ⟨D,⩽⟩ has at least one minor set, all minor sets of X are finite,
⌊{x}⌋={x}, ⌊∅⌋=∅, and
if ⟨D,⩽⟩ is additionally a poset then there exists exactly one minor set of X.
It turns out that ⟨AC⟨D,⩽⟩,⊑⟩ is a qoset, which is ACC if ⟨D,⩽⟩ is a wqoset and is a poset if ⟨D,⩽⟩ is a poset.
For the sake of clarity, we overload the notation and use the same symbol for a function/relation
and its componentwise (i.e. pointwise) extension on product domains, e.g., if f:X→Y then
f also denotes the standard product function f:Xn→Yn which is
componentwise defined by
λ⟨x1,…,xn⟩∈Xn.⟨f(x1),…,f(xn)⟩.
A vector \vvx in some product domain D∣S∣ indexed by a finite set S is also denoted by ⟨xi⟩i∈S and, for some i∈S,
\vvxi denotes its component xi.
Let ⟨X,⩽⟩ be a qoset and f:X→X be a function. f is monotonic when
x⩽y implies f(x)⩽f(y). For all n∈N, the n-th
power fn:X→X of f is inductively defined by:
f0≜λx.x; fn+1≜f\compfn (or, equivalently,
fn+1≜fn\compf).
The denumerable sequence of Kleene iterates
of f starting from an initial value a∈X is given by ⟨fn(a)⟩n∈N.
If ⟨X,⩽⟩ is a poset and a∈X then
lfpa(f) (resp. gfpa(f)) denotes the least
(resp. greatest) fixpoint of f
which is greater (resp. less) than or equal to a, when this exists;
in particular, lfp(f) (resp. gfp(f)) denotes the least
(resp. greatest) fixpoint of f, when this exists.
If
⟨X,⩽⟩ is an ACC (resp. DCC) CPO, a⩽f(a) (resp. f(a)⩽a) holds and f is monotonic
then the Kleene iterates
⟨fn(a)⟩n∈Nfinitely converge to lfpa(f)
(resp. gfpa(f)), i.e.,
there exists k∈N such that for all n≥k, fn(a)=fk(a)=lfpa(f)
(resp. gfpa(f)).
In particular, if
⊥ (resp. ⊤) is the least (greatest) element of ⟨X,⩽⟩ then ⟨fn(⊥)⟩n∈N (resp. ⟨fn(⊤)⟩n∈N)
finitely converges to lfp(f) (resp. gfp(f)).
2.2. Abstract Interpretation
Let us recall some basic notions on closure operators and Galois Connections commonly used in abstract interpretation (see, e.g., (Cousot and Cousot, 1979; Miné, 2017; Rival and Yi, 2020)).
Closure operators and Galois Connections are equivalent notions
and, therefore, they are both used for
defining the notion of approximation in abstract interpretation, where closure operators allow us to define and reason on abstract domains independently of a specific representation for abstract values which is required by
Galois Connections.
Let ⟨C,≤C,∨,∧⟩ be a complete lattice, where ∨ and ∧ denote, resp., lub and glb.
An upper closure operator, or simply closure, on ⟨C,≤C⟩ is a function ρ:C→C which is:
(i) monotonic,
(ii) idempotent: ρ(ρ(x))=ρ(x) for all x∈C, and
(iii) extensive: x≤Cρ(x) for all x∈C.
The set of all upper closed operators on C is denoted by uco(C).
We often write c∈ρ(C), or simply c∈ρ, to denote that
there exists c′∈C such that c=ρ(c′), and
recall that this happens iff ρ(c)=c.
If ρ∈uco(C) then for all c1∈C, c2∈ρ and X⊆C,
it turns out that:
[TABLE]
In abstract interpretation, a closure operator ρ∈uco(C) on a concrete domain C plays
the role of abstraction function for objects of C. Given two closures ρ,ρ′∈uco(C), ρ is a
coarser abstraction
than ρ′ (or, equivalently,
ρ′ is a more precise abstraction than ρ) iff the image of
ρ is a subset of the image of ρ′, i.e. ρ(C)⊆ρ′(C), and this happens iff for any x∈C,
ρ′(x)≤Cρ(x).
Let us recall that a Galois Connection (GC) or adjunction between two posets ⟨C,≤C⟩, called concrete domain, and ⟨A,≤A⟩, called abstract domain, consists of two functions α:C→A and γ:A→C such that α(c)≤Aa⇔c≤Cγ(a) always holds.
A Galois Connection is denoted by ⟨C,≤C⟩\galoisαγ⟨A,≤A⟩.
The function α is called the left-adjoint of γ, and, dually,
γ is called the right-adjoint of α. This terminology is justified by the fact that if
some function α:C→A
admits a right-adjoint γ:A→C then this is unique, and this dually holds for left-adjoints.
It turns out that in a GC between complete lattices, γ is always co-additive (i.e., it preserves arbitrary glb’s)
while α is always additive (i.e., it preserves arbitrary lub’s).
Moreover, an additive function α:C→A uniquely determines its right-adjoint by γ≜λa.∨C{c∈C∣α(c)≤Aa} and, dually, a co-additive function γ:A→C uniquely determines its left-adjoint by α≜λc.∧A{a∈A∣c≤Cγ(a)}.
The following remark is folklore in abstract interpretation and a proof is here provided for the sake of completeness.
Lemma 2.1.
Let ⟨C,≤C⟩\galoisαγ⟨A,≤A⟩ be a GC between complete lattices and
f:C→C be a monotonic function. Then,
γ(lfp(αfγ))=lfp(γαf).
Proof.
Let us first show that lfp(γαf)≤Cγ(lfp(αfγ)):
[TABLE]
Then, let us prove that γ(lfp(αfγ))≤Clfp(γαf):
[TABLE]
2.3. Languages
Let Σ be an alphabet, i.e., a finite nonempty set of symbols.
A word (or string) on Σ is a finite (possibly empty) sequence of symbols in Σ, where ϵ denotes the empty sequence.
Σ∗ denotes the set of finite words on Σ. A language on Σ is a subset L⊆Σ∗.
Concatenation of words and languages is denoted by simple juxtaposition, that is,
the concatenation of words
u,v∈Σ∗ is denoted by uv∈Σ∗, while the concatenation of
languages L,L′⊆Σ∗ is denoted by
LL′≜{uv∣u∈L,v∈L′}. By considering a word as a singleton language,
we also concatenate words with languages, for example
uL and uLv.
A finite automaton (FA) is a tuple A=⟨Q,δ,I,F,Σ⟩ where: Σ is an alphabet, Q is a finite set of states, I⊆Q is a subset of initial states, F⊆Q is a subset of final states, and δ:Q×Σ→℘(Q) is a transition relation.
The notation q→aq′ is also used to denote that q′∈δ(q,a).
If u∈Σ∗ and q,q′∈Q then q⇝uq′ means that the state q′ is reachable
from q by following the string u. More formally, by induction on the length of u∈Σ∗:
(i) if u=ϵ then q⇝ϵq′ iff q=q′; (ii) if u=av with a∈Σ,v∈Σ∗ then
q⇝avq′ iff ∃q′′∈δ(q,a),q′′⇝vq′.
The language generated by a FA A is L(A)≜{u∈Σ∗∣∃qi∈I,∃qf∈F,qi⇝uqf}.
An example of FA is depicted in Fig. 1.
3. Kleene Iterates with Abstract Inclusion Check
Abstract interpretation can be applied to solve a generic inclusion checking problem
by leveraging backward complete abstractions (Cousot and Cousot, 1977, 1979; Giacobazzi
et al., 2000; Ranzato, 2013).
A closure ρ∈uco(C) is called backward complete
for a concrete
monotonic function f:C→C when ρf=ρfρ holds. Since ρf(c)≤Cρfρ(c) always holds for all c∈C (because ρ is extensive and monotonic and f is monotonic),
the intuition is that
backward completeness models an ideal situation where no loss of precision
is accumulated in the computations of ρf when
its concrete input objects c are approximated by ρ(c).
It is well known (Cousot and Cousot, 1979)
that backward completeness implies completeness of least fixpoints, namely for
all x∈C such that x≤Cf(x),
[TABLE]
provided that these least fixpoints exist (this is the case, e.g., when C is a CPO).
Given an initial value a∈C,
let us define the following iterative procedure:
[TABLE]
which computes the Kleene iterates of f starting from a and stops when
a convergence relation Conv⊆C×C for two consecutive Kleene iterates fn+1(a) and fn(a) holds.
When
Conv=Incl≜{(x,y)∣x≤Cy} is the convergence relation
and a≤Cf(a) holds,
the procedure \textscKleene(Incl,f,a) returns lfpa(f)
if the Kleene iterates finitely converge. Hence, termination of \textscKleene(Eq,f,a)
is guaranteed when C is an ACC CPO.
Given a closure ρ∈uco(C),
let us consider
the following abstract convergence relation induced by ρ:
[TABLE]
Hence, \textscKleene(Inclρ,f,a) terminates if eventually
ρ(f(x))≤Cρ(x) holds. Notice that Incl⊆Inclρ always holds by monotonicity of ρ and Incl=Inclρ iff ρ=id.
Theorem 3.1.
Let ρ∈uco(C) be such that
ρ is backward complete for f and
ρ(C) does not contain infinite ascending chains. Let a∈C
such that a≤Cf(a) holds. Then, the procedure \textscKleene(Inclρ,f,a) terminates and ρ(\textscKleene(Inclρ,f,a))=ρ(lfpa(f))=lfpa(ρf).
Proof.
Let us first prove by induction the following property:
[TABLE]
For n=0, we have that ρ\compf0=ρ=(ρ\compf)0\compρ.
For n+1,
[TABLE]
Then, let us observe that lfpa(ρf)=lfpρ(a)(ρf):
this is a consequence of the fact that
ρ(f(x))=x∧a≤Cx iff ρ(f(x))=x∧ρ(a)≤Cx, because
ρ(f(x))=x∧a≤Cx implies ρ(f(x))=x∧ρ(a)≤Cρ(x)=ρ(ρ(f(x)))=ρ(f(x))=x.
Since a≤Cf(a), we have that ⟨fn(a)⟩n∈N is an ascending chain,
so that, by monotonicity of ρ,
⟨ρ(fn(a))⟩n∈N is an ascending chain in ρ(C).
Since ρ(C) does not contain infinite ascending chains,
there exists N=min({n∈N∣ρ(fn+1(a))≤Cρ(fn(a))}). This means that
\textscKleene(Inclρ,f,a) terminates after N+1 iterations and outputs
fN(a).
We prove by induction on N∈N
that N=min({n∈N∣(ρ\compf)n+1(ρ(a))≤C(ρ\compf)n(ρ(a))}).
(N=0):
We have that ρ(f1(a))≤Cρ(f0(a)), namely,
ρ(f(a))≤Cρ(a). Then, by backward completeness,
ρ(f(ρ(a)))≤Cρ(a), namely,
(ρ\compf)1(ρ(a))≤C(ρ\compf)0(ρ(a)).
(N+1):
We have that ρ(fN+2(a))≤Cρ(fN+1(a)), so that by (5), (ρ\compf)N+2(ρ(a))≤C(ρ\compf)N+1(ρ(a)). Moreover, N+1 is the minimum natural number
such that (ρ\compf)n+1(ρ(a))≤C(ρ\compf)n(ρ(a)) holds,
because if
(ρ\compf)k+1(ρ(a))≤C(ρ\compf)k(ρ(a)) for some k≤N,
then, by (5), we would have that
ρ(fk+1(a))≤Cρ(fk(a)), thus contradicting the minimality of N+1 for
ρ(fn+1(a))≤Cρ(fn(a)).
Since a≤Cf(a) implies, by backward completeness,
ρ(a)≤Cρ(f(a))=(ρ\compf)(ρ(a))), and
N=min({n∈N∣(ρ\compf)n+1(ρ(a))≤C(ρ\compf)n(ρ(a))}), it turns out that (ρ\compf)N(ρ(a))=lfpρ(a)(ρf)=lfpa(ρf). Thus, by (5), we obtain lfpa(ρf)=(ρ\compf)N(ρ(a))=ρ(fN(a))=ρ(\textscKleene(Inclρ,f,a)).
Finally, by (4),
ρ(\textscKleene(Inclρ,f,a))=lfpa(ρf)=ρ(lfpa(f)).
∎
We will apply the order-theoretic algorithmic
scheme provided by \textscKleene under the hypotheses of
Theorem 3.1 to a number of
different language inclusion problems L1⊆L2, where L1 can be expressed
as least fixpoint of a monotonic function on ℘(Σ∗). This will allow
us to systematically design several language inclusion algorithms which rely on
different backward complete abstractions of the complete lattice
⟨℘(Σ∗),⊆⟩.
4. An Algorithmic Framework for Language Inclusion
4.1. Languages as Fixed Points
Let A=⟨Q,δ,I,F,Σ⟩ be a FA.
Given S,T⊆Q, define the set of words leading from some state in S to some
state in T as follows:
[TABLE]
When S={q} or T={q′} we slightly abuse the notation and write Wq,TA, WS,q′A, or Wq,q′A.
Also, we omit the automaton A in superscripts when this is clear from the context.
The language accepted by A is therefore L(A)≜WI,FA.
Observe that
[TABLE]
where, as usual, ⋃∅=∅.
Let us recall how to define the language accepted by an automaton as a solution of a set of equations (Schützenberger, 1963).
Given a generic Boolean predicate p(x) for a variable x ranging in some set (typically a membership predicate x∈\scaleto?3.5ptZ)
and two generic sets T and F, we define the following parametric
choice function:
[TABLE]
The FA A induces the following set of equations, where the Xq’s
are variables of type Xq∈℘(Σ∗) and are indexed by states q∈Q of A:
[TABLE]
Thus, the functions λ⟨Xq′⟩q′∈Q.ψ∅{ϵ}(q∈\scaleto?3.5ptF)∪⋃a∈Σ,q′∈δ(q,a)aXq′
in the right-hand side of the equations in
Eqn(A) have
type ℘(Σ∗)∣Q∣→℘(Σ∗).
Since ⟨℘(Σ∗)∣Q∣,⊆⟩ is a (product) complete lattice (as ⟨℘(Σ∗),⊆⟩ is a complete lattice) and all the right-hand side functions in Eqn(A) are clearly monotonic,
the least solution ⟨Yq⟩q∈Q∈℘(Σ∗)∣Q∣ of Eqn(A) does exist and it is easy to check
that for every q∈Q, Yq=Wq,FA holds.
It is worth noticing that, by relying on right concatenations rather than left ones
aXq′ used
in Eqn(A), one could also define a
set of symmetric equations whose least solution coincides with ⟨WI,qA⟩q∈Q instead of ⟨Wq,FA⟩q∈Q.
Example 4.1.
Let us consider the automaton A in Figure 1. The set of equations induced by A are as follows:
[TABLE]
It is notationally convenient
to formulate the equations in Eqn(A) by exploiting
an “initial” vector \vvϵF∈℘(Σ∗)∣Q∣ and a predecessor
function PreA:℘(Σ∗)∣Q∣→℘(Σ∗)∣Q∣ defined as follows:
[TABLE]
The intuition for the function PreA is that given the language Wq′,FA and a transition q′∈δ(q,a), we have that aWq′,FA⊆Wq,FA holds, i.e., given a subset Xq′ of the language generated by A from some state q′, the function PreA computes a subset Xq of the language generated by A for its predecessor state q. Notice that if all the components of
\vvX are finite sets of words then PreA(\vvX) is still a vector of finite sets.
Since ϵ∈Wq,FA for all q∈F, the least fixpoint computation can start from the vector
\vvϵF and iteratively apply PreA.
Therefore, it turns out that
[TABLE]
Together with Equation (6), it follows that L(A) is given by the union of the component languages of the vector
lfp(λ\vvX.\vvϵF∪PreA(\vvX)) that are indexed by the initial states in I.
Consider a language inclusion problem L1⊆L2, where L1=L(A) for some FA A=⟨Q,δ,I,F,Σ⟩.
The language L2 can be formalized as a vector in ℘(Σ∗)∣Q∣ as follows:
[TABLE]
whose components indexed by initial states in I are L2 and those indexed by noninitial states are Σ∗. Then, as a consequence of (6), (7) and (8), we have that
[TABLE]
Theorem 4.3.
If ρ∈uco(℘(Σ∗)) is backward complete for λX∈℘(Σ∗).aX for all a∈Σ,
then, for all FAs A=⟨Q,δ,I,F,Σ⟩ on the alphabet Σ, ρ is backward complete for PreA and λ\vvX.\vvϵF∪PreA(\vvX).
Proof.
First, it turns out that:
[TABLE]
As a consequence, ρ is backward complete for λ\vvX.\vvϵF∪PreA(\vvX):
[TABLE]
∎
Then, by resorting to least fixpoint transfer of completeness (4), we also obtain the following
consequence.
Corollary 4.4.
If ρ∈uco(℘(Σ∗))
is backward complete for λX∈℘(Σ∗).aX for all a∈Σ then
ρ(lfp(λ\vvX.\vvϵF∪PreA(\vvX)))=lfp(λ\vvX.ρ(\vvϵF∪PreA(\vvX))).
Note that if ρ is backward complete for λX.aX for all a∈Σ
and L2∈ρ then, by Theorem 3.1 and Corollary 4.4, the equivalence (9) becomes
[TABLE]
4.2.1. Right Concatenation
Let us consider the symmetric case of right concatenation λX.Xa.
Recall that
WI,q={w∈Σ∗∣∃qi∈I,qi⇝wq} and
that WI,q=ψ∅{ϵ}(q∈\scaleto?3.5ptI)∪⋃a∈Σ,a∈Wq′,qWI,q′a holds. Correspondingly,
we define
a set of fixpoint equations on ℘(Σ∗) which is based on right concatenation
and is symmetric to the equations defined in (7):
[TABLE]
In this case, if \vvY=⟨Yq⟩q∈Q is the
least fixpoint solution of Eqnr(A) then
Yq=WI,qA for every q∈Q.
Also, by defining \vvϵI∈℘(Σ∗)∣Q∣ and
PostA:℘(Σ∗)∣Q∣→℘(Σ∗)∣Q∣ as follows:
[TABLE]
we have that
[TABLE]
Thus, by (6), it turns out that
L(A)=⋃qf∈FWI,qf holds, that is,
L(A) is the union of the component
languages of the vector
lfp(λ\vvX.\vvϵI∪PostA(\vvX))
indexed by the final states in F.
Example 4.5.
Consider again the FA A in Figure 1.
The set of right equations for A is as follows:
[TABLE]
so that
[TABLE]
In a language inclusion problem L(A)⊆L2,
we consider the vector
\vvL2F≜⟨ψΣ∗L2(q∈\scaleto?3.5ptF)⟩q∈Q∈℘(Σ∗)∣Q∣, so that, by (11), it turns out that:
[TABLE]
We therefore have the following symmetric version
of Theorem 4.3 for right concatenation.
Theorem 4.6.
If ρ∈uco(℘(Σ∗))
is backward complete for λX.Xa for all a∈Σ then, for all FAs A on the alphabet Σ, ρ is backward complete for λ\vvX.\vvϵI∪PostA(\vvX).
4.3. A Language Inclusion Algorithm with Abstract Inclusion Check
Let us now apply the general Theorem 3.1 to design
an algorithm that solves a language inclusion problem L(A)⊆L2
by exploiting a language abstraction ρ that satisfies
a list of requirements of backward completeness and computability.
Theorem 4.7.
Let A=⟨Q,δ,I,F,Σ⟩ be a FA, L2∈℘(Σ∗) and
ρ∈uco(℘(Σ∗)).
Assume that the following properties hold:
(i)
The closure ρ is backward complete for λX∈℘(Σ∗).aX, for all a∈Σ, and satisfies ρ(L2)=L2.
2. (ii)
ρ(℘(Σ∗))* does not contain
infinite ascending chains.*
3. (iii)
If X,Y∈℘(Σ∗) are finite sets of words then
the inclusion ρ(X)⊆\scaleto?3.5ptρ(Y) is decidable.
4. (iv)
If Y∈℘(Σ∗) is a finite set of words then
the inclusion ρ(Y)⊆\scaleto?3.5ptL2 is decidable.
Conditions (i), (ii) and (iii) guarantee that
the hypotheses of
Theorem 3.1 are satisfied. Thus,
\textscKleene(Inclρ,λ\vvX.\vvϵF∪PreA(\vvX),\vv∅) is an algorithm that terminates
with output ⟨Yq⟩q∈Q and
[TABLE]
Moreover, by (9),
L(A)⊆L2⇔ρ(L(A))⊆ρ(L2)=L2⇔ρ(lfp(λ\vvX.\vvϵF∪PreA(\vvX)))⊆\vvL2I⇔ρ(⟨Yq⟩q∈Q)⊆ρ(\vvL2I)⇔Inclρ(⟨Yq⟩q∈Q,\vvL2I). Finally, by condition (iv), Inclρ(⟨Yq⟩q∈Q,\vvL2I) is decidable.
∎
It is worth noticing that Theorem 4.7 can also be stated in a symmetric version for λ\vvX.\vvϵI∪PostA(\vvX) similarly to Theorem 4.6.
5. Instantiating the Framework with Quasiorders
We instantiate the general algorithmic framework of
Section 4 to the class of closure operators induced by quasiorder relations on words.
5.1. Word-based Abstractions
Let ⩽⊆Σ∗×Σ∗ be a quasiorder relation on words in Σ∗.
The corresponding closure operator ρ⩽∈uco(℘(Σ∗)) is defined as follows:
[TABLE]
Thus, ρ⩽(X) is the ⩽-upward closure
of X and it is easy to check that ρ⩽ is indeed a closure
on the complete lattice ⟨℘(Σ∗),⊆⟩.
Following (de Luca and
Varricchio, 1994), a quasiorder ⩽ on Σ∗ is left-monotonic (resp. right-monotonic)
if
[TABLE]
Also, ⩽ is called monotonic if it is both left- and right-monotonic.
It turns out that ⩽ is left-monotonic (resp. right-monotonic) iff
[TABLE]
In fact, if x1⩽x2 then (13) implies
that for all y∈Σ∗, yx1⩽yx2: by induction
on the length ∣y∣∈N, we have that:
(i) if y=ϵ then yx1⩽yx2; (ii) if y=av with a∈Σ,v∈Σ∗ then, by inductive
hypothesis,
vx1⩽vx2, so that by (13), yx1=avx1⩽avx2=yx2.
Definition 5.1 (L-Consistent Quasiorder).
Let L∈℘(Σ∗). A quasiorder ⩽L⊆Σ∗×Σ∗ is called left (resp. right) L-consistent when:
(a)
⩽L∩(L׬L)=∅;
2. (b)
⩽L is left-monotonic (resp. right-monotonic).
Also, ⩽L is called L-consistent when it is both left and right L-consistent.
It turns out that a quasiorder is L-consistent iff it induces a closure which includes L in its image and it is
backward complete for concatenation.
Lemma 5.2.
Let L∈℘(Σ∗) and ⩽L be a quasiorder on Σ∗.
Then, ⩽L is a
left (resp. right) L-consistent quasiorder on Σ∗ if and only if
(a)
ρ⩽L(L)=L, and
2. (b)
ρ⩽L* is backward complete for λX.aX (resp. λX.Xa) for all a∈Σ.*
Proof.
We consider the left case, the right case is symmetric.
(a)
The inclusion
L⊆ρ⩽L(L) always
holds because ρ⩽L is an upper closure. Then, it turns out that ρ⩽L(L)=L iff
ρ⩽L(L)⊆L iff ∀v∈Σ∗,
(∃u∈L,u⩽Lv)⇒v∈L iff ⩽L∩(L׬L)=∅.
Thus, ρ⩽L(L)=L iff
condition (a) of Definition 5.1 holds.
2. (b)
We first prove that if ⩽L is left-monotonic then for all X∈℘(Σ∗),
ρ⩽L(aX)=ρ⩽L(aρ⩽L(X)) for all a∈Σ.
Monotonicity of concatenation together with monotonicity and extensivity of
ρ⩽L imply that ρ⩽L(aX)⊆ρ⩽L(aρ⩽L(X)) holds.
For the reverse inclusion, we have that:
[TABLE]
Conversely, assume that for all X∈℘(Σ∗) and a∈Σ,
ρ⩽L(aX)=ρ⩽L(aρ⩽L(X)).
Consider x1,x2∈Σ∗ and a∈Σ.
If x1⩽Lx2 then
{x2}⊆ρ⩽L({x1}), and in turn
a{x2}⊆aρ⩽L({x1}).
Then, by applying the monotonic function
ρ⩽L,
ρ⩽L(a{x2})⊆ρ⩽L(aρ⩽L({x1})), so that, by backward completeness,
ρ⩽L(a{x2})⊆ρ⩽L(a{x1}).
Hence, a{x2}⊆ρ⩽L(a{x1}), namely,
ax1⩽Lax2. By (13), this shows that ⩽L is left-monotonic. ∎
We can apply Theorem 4.7
to the closure ρ⩽L2l induced by a left L2-consistent
well-quasiorder, since it satisfies all the required hypotheses,
thus obtaining the following Algorithm FAIncW which solves the language inclusion problem L(A)⊆L2 for any automaton A.
This algorithm is called “word-based” because the output
vector ⟨Yq⟩q∈Q computed by \textscKleene
consists of finite sets of words. Here, the convergence relation
Inclρ⩽L2l of \textscKleene coincides with the relation
⊑⩽L2l
because
Inclρ⩽L2l(X,Y) iff ρ⩽L2l(X)⊆ρ⩽L2l(Y) iff
X⊑⩽L2lY.
Theorem 5.3.
*Let A=⟨Q,δ,I,F,Σ⟩ be a FA and L2∈℘(Σ∗) be a language such that:
(i) membership in L2 is decidable;
(ii) there exists a decidable left L2-consistent wqo on Σ∗.
Then, Algorithm FAIncW decides the inclusion problem L(A)⊆L2.*
Proof.
Let ⩽L2l be the
decidable left L2-consistent wqo on Σ∗.
Let us check that the hypotheses (i)-(ii)-(iii)
of Theorem 4.7 are satisfied.
(i)
It follows from hypothesis (ii) and Lemma 5.2 that ⩽L2l is backward complete for left concatenation and satisfies ρ⩽L2l(L2)=L2.
2. (ii)
Since ⩽L2l is a well-quasiorder, it follows that {ρ⩽L2l(S)∣S∈℘(Σ∗)} does not contain infinite ascending chains.
3. (iii)
For finite sets for finite sets X and Y, the abstract inclusion
Inclρ⩽L2l(X,Y)⇔X⊑⩽L2lY is decidable
since ⩽L2l is a decidable wqo.
Moreover, it turns out that
the check Inclρ⩽L2l(⟨Yq⟩q∈Q,\vvL2I) of Theorem 4.7 is decidable and
is performed
by lines 2-5 of Algorithm FAIncW.
In fact, since, by Theorem 4.7,
\textscKleene(⊑⩽L2l,λ\vvX.\vvϵF∪PreA(\vvX),\vv∅) terminates after a finite number of steps
with output ⟨Yq⟩q∈Q, each set of words
Yq of the output turns out to be finite.
Also, since \vvL2I=⟨ψΣ∗L2(q∈\scaleto?3.5ptI)⟩q∈Q), the abstract inclusion trivially holds for all components Yq with q∈/I.
Therefore, it suffices to check whether Yq⊑⩽L2lL2 holds for all q∈I. Since Yq⊑⩽L2lL2 iff ρ⩽L2l(Yq)⊆ρ⩽L2l(L2)=L2 iff
Yq⊆L2 and since Yq is a finite set,
Yq⊑⩽L2lL2
can be decided by performing the finitely many membership check u∈\scaleto?3.5ptL2
at lines 2-5, where
by hypothesis (ii), any membership
check is decidable. Thus, hypothesis (iv)
of Theorem 4.7 is satisfied.
Summing up, we have shown that
Algorithm FAIncW decides the inclusion L(A)⊆L2.
∎
Remark 5.4.
It is worth noticing that in each iteration of \textscKleene(⊑⩽L2l,λ\vvX.\vvϵF∪PreA(\vvX),\vv∅)
in Algorithm FAIncW, in the current
vector ⟨Yq⟩q∈Q one
could safely remove from a component Yq any word w∈Yq such that there
exists a word u∈Yq such that u⩽L2lw and u=w.
This enables replacing each finite set Yq occurring in Kleene iterates
with a minor subset ⌊Yq⌋ w.r.t. ⩽L2l.
This replacement is correct, i.e. Theorem 5.3 still holds
for the corresponding modified language inclusion algorithm, because an
inclusion check X⊑⩽L2lY holds iff the check
⌊X⌋⊑⩽L2l⌊Y⌋ for the corresponding minor subsets
holds.
◊
5.1.1. Right Concatenation
Following Section 4.2.1,
a symmetric version, called FAIncWr, of the algorithm FAIncW (and of Theorem 5.3) for rightL2-consistent wqos can be given as follows.
Theorem 5.5.
*Let A=⟨Q,δ,I,F,Σ⟩ be a FA and L2∈℘(Σ∗) be a language such that:
(i) membership in L2 is decidable;
(ii) there exists a decidable right L2-consistent wqo on Σ∗.
Then, Algorithm FAIncWr decides the inclusion problem L(A)⊆L2.*
In the following, we will consider different quasiorders on Σ∗ and we will show that they fulfill the requirements of Theorem 5.3, therefore yielding algorithms for solving language inclusion problems.
5.2. Nerode Quasiorders
The notions of left and right quotient of a language L∈℘(Σ∗) w.r.t. a word w∈Σ∗ are standard:
[TABLE]
Correspondingly, let us define the following quasiorder relations on Σ∗:
[TABLE]
De Luca and Varricchio (1994, Section 2) call them, resp., the left
(≦Ll)
and right (≦Lr)
Nerode quasiorders relative to L.
The following result shows that Nerode quasiorders are the weakest (i.e., greatest w.r.t. set inclusion of binary relations) L2-consistent quasiorders for which the algorithm FAIncW can be instantiated to decide a language inclusion L(A)⊆L2.
Lemma 5.6.
Let L∈℘(Σ∗).
(a)
≦Ll* and
≦Lr are, resp., left and right
L-consistent quasiorders.
If L is regular then, additionally, ≦Ll and ≦Lr
are decidable wqos.*
2. (b)
If ⩽ is a left (resp. right) L-consistent quasiorder on Σ∗ then ρ≦Ll(℘(Σ∗))⊆ρ⩽(℘(Σ∗)) (resp. ρ≦Lr(℘(Σ∗))⊆ρ⩽(℘(Σ∗))).
Proof.
Let us consider point (a).
De Luca and Varricchio (1994, Section 2) observe that ≦Ll and ≦Lr are,
resp., left and right monotonic.
Moreover, De Luca and Varricchio (1994, Theorem 2.4) show that if
L is regular then both ≦Ll and ≦Lr are wqos.
Let us also observe that given u∈L and v∈/L we have that ϵ∈Lu−1 and ϵ∈u−1L while ϵ∈/Lv−1 and ϵ∈/v−1L. Hence, ≦Ll (≦Lr) is a left (right) L-consistent quasiorder.
Finally, if L is regular then both relations are
clearly decidable.
Let us now consider point (b) for the left case (the right case is symmetric).
By the characterization of left consistent quasiorders given by Lemma 5.2,
De Luca and Varricchio (1994, Section 2, point 4) observe that ≦Ll is maximum in the set of all left L-consistent quasiorders, i.e. every left L-consistent quasiorder ⩽ is such that
x⩽y⇒x≦Lly.
As a consequence, ρ⩽(X)⊆ρ≦Ll(X) holds for all X∈℘(Σ∗), namely, ρ≦Ll(℘(Σ∗))⊆ρ⩽(℘(Σ∗)).
∎
This allows us to derive a first instantiation of Theorem 5.3. Because membership is decidable for regular languages L2, Lemma 5.6 (a) for ≦L2l implies that the hypotheses (i) and (ii) of Theorem 5.3 are satisfied, so that the algorithm FAIncW instantiated to ≦L2l
decides the inclusion L(A)⊆L2 when L2 is regular.
Furthermore, under these hypotheses,
Lemma 5.6 (b) shows that ≦L2l is the weakest
left L2-consistent quasiorder relation on Σ∗ for which the algorithm FAIncW can be instantiated
for deciding an inclusion L(A)⊆L2.
Example 5.7.
We illustrate the use of the left Nerode quasiorder in Algorithm FAIncW for solving the language inclusion L(A1)⊆L(A2), where A1 and A2 are the FAs shown in Figure 2.
The equations for A1 are as follows:
[TABLE]
We have the following quotients (among others) for L=L(A2)=a∗(a(a+b)∗a+a+c+ab+bb):
[TABLE]
Hence, among others, the following relations hold:
c≦Lla, c≦Llb and c≦Llw
for all w∈(a(a+b)∗a+ac+ab+bb).
Then, let us show the computation of the Kleene iterates performed by the Algorithm FAIncW.
[TABLE]
It turns out that
⟨{aa,ab,ac,a,b,c},{ϵ}⟩⊑≦Ll⟨{a,b,c},{ϵ}⟩ because c≦Llaa, c≦Llab and
c≦Llac hold, so that \textscKleene stops with \vvY(3) and outputs
\vvY=⟨{a,b,c},{ϵ}⟩.
Since c∈\vvY1 and c∈/L(A2), the Algorithm FAIncW correctly concludes that L(A1)⊆L(A2) does not hold. ◊
5.2.1. On the Complexity of Nerode quasiorders
For the inclusion problem between languages generated by finite automata, deciding the
(left or right) Nerode quasiorder relation between words can be easily shown to be as hard as the language inclusion problem itself, which is PSPACE-complete.
In fact, given the automata A1=(Q1,δ1,I1,F1,Σ) and A2=(Q2,δ2,I2,F2,Σ), one can define the union automaton A3≜(Q1∪Q2∪{qι},δ3,{qι},F1∪F2) where δ3 maps (qι,a) to I1, (qι,b) to I2 and behaves like δ1 or δ2 elsewhere. Then, it turns out that a≦L(A3)rb⇔a−1L(A3)⊆b−1L(A3)⇔L(A1)⊆L(A2).
Also, for the inclusion problem of a language generated by an
automaton within the trace set of a one-counter net (cf. Section 5.4), the right Nerode quasiorder is a right language-consistent well-quasiorder but it turns out to be undecidable (cf. Lemma 5.16).
5.3. State-based Quasiorders
Consider an inclusion problem L(A1)⊆L(A2) where A1 and A2 are FAs.
In the following, we study a class of well-quasiorders based on A2, that we call state-based quasiorders.
These quasiorders are strictly stronger (i.e., lower w.r.t. set inclusion of binary relations) than the Nerode quasiorders defined in Section 5.2 and sidestep the untractability or undecidability of Nerode quasiorders (cf. Section 5.2.1) yet allowing to define an algorithm solving the language inclusion L(A1)⊆L(A2).
5.3.1. Inclusion in Regular Languages.
We define the
quasiorders ≤Al and ≤Ar on Σ∗
induced by a FA A=⟨Q,δ,I,F,Σ⟩
as follows: for all u,v∈Σ∗,
[TABLE]
where, for all X∈℘(Q),
preuA(X)≜{q∈Q∣u∈Wq,XA}
and postuA(X)≜{q′∈Q∣u∈WX,q′A} denote the standard predecessor/successor state
transformers in A.
The superscripts in ≤Al and ≤Ar stand, resp., for left/right because the following result holds.
Lemma 5.8.
The relations ≤Al and ≤Ar are, resp., decidable left and right
L(A)-consistent wqos.
Proof.
Since, for every u∈Σ∗, preuA(F) is a finite and computable set, it turns out that ≤Al is a decidable wqo.
Let us check that ≤Al is left L(A)-consistent according to Definition 5.1 (a)-(b).
(a) By picking u∈L(A) and v∈/L(A) we have that preuA(F) contains some initial state while prevA(F) does not, hence u≰Alv.
(b) Let us check that ≤Al is left monotonic.
Observe that, for all x∈Σ∗, prexA is a monotonic function and that
[TABLE]
Therefore, for all x1,x2∈Σ∗ and a∈Σ,
[TABLE]
The proof that ≤Ar is a decidable right L(A)-consistent quasiorder is symmetric.
∎
As a consequence, Theorem 5.3 applies to the wqo ≤A2l (and
≤A2r), so that one can instantiate the algorithm FAIncW to ≤A2l for deciding
an inclusion L(A1)⊆L(A2).
Turning back to the left Nerode wqo
≦L(A2)l, it turns out that the following equivalences hold:
[TABLE]
Since preuA2(F)⊆prevA2(F) entails WI,preuA2(F)⊆WI,prevA2(F), it follows that u≤A2lv⇒u≦L(A2)lv and, in turn,
ρ≦L(A2)l(℘(Σ∗))⊆ρ≤A2l(℘(Σ∗)).
Example 5.9.
We illustrate the left state-based quasiorder by using it to solve the language inclusion L(A1)⊆L(A2) of Example 5.7.
We have, among others, the following set of predecessors of FA2:
[TABLE]
Recall from Example 5.7 that, for the Nerode quasiorder, we have c≦L(A2)lb, c≦L(A2)la while none of these relations hold for ≤A2l.
Let us next show the Kleene iterates computed by Algorithm FAIncW when using the quasiorder ≤A2l.
[TABLE]
It turns out that ⟨{aaa,aab,aac,aa,ab,ac,a,b,c},{ϵ}⟩⊑≤A2l⟨{aa,ab,ac,a,b,c},{ϵ}⟩ so that \textscKleene outputs the vector
\vvY=⟨{aa,ab,ac,a,b,c},{ϵ}⟩.
Since c∈\vvY0 and c∈/L(A2), Algorithm FAIncW concludes that the language inclusion L(A1)⊆L(A2) does not hold. ◊
5.3.2. Simulation-based Quasiorders.
Recall that a simulation on a FA A=⟨Q,δ,I,F,Σ⟩ is a binary relation ⪯⊆Q×Q such that for all p,q∈Q such that p⪯q the following two conditions hold:
(i)
if p∈F then q∈F;
2. (ii)
for every transition pap′, there exists a transition qaq′ such that p′⪯q′.
It is well known that simulation relations are closed under arbitrary unions, where
the greatest (w.r.t. inclusion) simulation relation ⪯A≜∪{⪯⊆Q×Q∣⪯ is a simulation on A}
is a quasiorder, called simulation quasiorder
of A.
It is also well known that simulation implies language inclusion, i.e., if ⪯ is
a simulation on A then
[TABLE]
A relation ≤⊆Q×Q on states
can be lifted in the standard universal/existential way to a relation ≤∀∃⊆℘(Q)×℘(Q) on sets of states as follows:
[TABLE]
In particular, if ≤ is a quasiorder
then ≤∀∃ is a quasiorder as well.
Also, if ⪯ is a simulation relation then its lifting ⪯∀∃ is such
that X⪯∀∃Y⇒WX,FA⊆WY,FA holds. This suggests us to
define a right simulation-based quasiorder⪯Ar on Σ∗ induced by a simulation ⪯ on A as follows: for all u,v∈Σ∗,
[TABLE]
Lemma 5.10.
Given a simulation relation ⪯ on A, the right simulation-based quasiorder ⪯Ar is a decidable right L(A)-consistent wqo.
Proof.
Let u∈L(A) and v∈/L(A), so that
F∩postuA(I)=∅ and (F∩postvA(I))=∅ hold. Hence, there exists q∈postuA(F)∩F such that q⪯Arq′ for no q′∈postvA(F) since, by simulation, this would imply q′∈postvA(F)∩F, which would contradict F∩postvA(I)=∅.
Therefore, u⋠Arv holds.
Next we show that ⪯Ar is right monotonic. By (13), we check that for all u,v∈Σ∗ and a∈Σ,
u⪯Arv⇒ua⪯Arva:
[TABLE]
Thus, ⪯Ar is a right L(A)-consistent quasiorder.
Finally, since ℘(Q) is finite, it follows that ⪯Ar is a well-quasiorder and, since postuA(I) is finite and computable for every u∈Σ∗, it follows that ⪯Ar is decidable. ∎
Thus, once again, Theorem 5.5 applies to
⪯A2r and this allows us to instantiate the
algorithm FAIncWr to the quasiorder
⪯A2r for deciding an inclusion L(A1)⊆L(A2).
Note that it is possible to define a left simulation ⪯R∀∃ on an automaton A by applying ⪯∀∃ on the reverse automaton
AR of A where arrows are flipped and initial/final states are swapped.
This left simulation induces a left simulation-based quasiorder on Σ∗ as follows: for all u,v∈Σ∗,
[TABLE]
It is straightforward to check that Theorem 5.3 applies to ⪯A2l and, therefore, we can instantiate the Algorithm FAIncW for deciding L(A1)⊆L(A2).
Example 5.11.
Let us illustrate the use of the left simulation-based quasiorder to solve the language inclusion L(A1)⊆L(A2) of Example 5.7.
For the set FA2 of final states A2
we have the same set of predecessors computed in Example 5.9 and, among others, the following left simulations between these sets w.r.t. the simulation quasiorder
⪯A2R
of the reverse of A2
(recall that
⪯∀∃ is defined w.r.t. simulations of A2R):
[TABLE]
because q2⪯A2Rq1, q2⪯A2Rq3 and q2⪯A2Rq4 hold.
Let us show the computation of the Kleene iterates performed by Algorithm FAIncW when using the quasiorder ⊑⪯A2l as abstract inclusion check:
[TABLE]
It turns out that ⟨{aa,ab,ac,a,b,c},{ϵ}⟩⊑⪯A2l⟨{a,b,c},{ϵ}⟩, so that \textscKleene outputs the vector
\vvY=⟨{a,b,c},{ϵ}⟩. Thus, once again,
since c∈\vvY0 and c∈/L(A2), Algorithm FAIncW concludes that L(A1)⊆L(A2) does not hold. ◊
Let us observe that u⪯A2rv implies WpostuA2(I),F⊆WpostvA2(I),F, which is equivalent to the right Nerode quasiorder u≦L(A2)rv for L(A2) defined in (14),
so that u⪯A2rv⇒u≦L(A2)rv holds. Furthermore, for the state-based quasiorder defined in
(15), we have that
u≤A2rv⇒u⪯A2rv trivially holds.
Summing up, the following containments relate (the right versions of) state-based,
simulation-based and Nerode quasiorders:
[TABLE]
All these quasiorders are decidable L(A2)-consistent wqos so
that the
algorithm FAIncW can be instantiated to each of them for deciding an inclusion L(A1)⊆L(A2).
Examples 5.7, 5.9 and 5.11 show how FAIncW behaves for each of the three quasiorders considered in this section.
Despite their simplicity, the examples show the differences in the behavior of the algorithm when considering the different quasiorders.
In particular, we observe that the iterations of \textscKleene for ≦L(A2)r coincides with those for ⪯A2r and, as expected, these Kleene iterates converge faster than those for ≤A2r.
Recall that ≦L(A2)r is the coarsest well-quasiorder for which Algorithm FAIncW works, hence its corresponding Kleene iterates exhibit optimal behavior in terms of number of iterations to converge.
The drawback of using the Nerode quasiorder ≦L(A2)r
is that it requires checking language inclusion in order to decide whether two words are related, and this is a PSPACE-complete problem.
Therefore, the coincidence of the Kleene iterates for ≦L(A2)r and ⪯A2r is of special interest since it highlights that Algorithm FAIncW might exhibit optimal behavior while using a “simpler” (i.e., finer) well-quasiorder such as ⪯A2r, which is a polynomial approximation of ≦L(A2)r.
5.4. Inclusion in Traces of One-Counter Nets.
We show that our framework can be instantiated to systematically derive an algorithm for deciding an inclusion L(A)⊆L2 where L2 is the trace set of a one-counter net (OCN).
This is accomplished by defining a decidable L2-consistent quasiorder so that Theorem 5.3 can be applied.
Intuitively, an OCN is a FA endowed with a nonnegative integer counter which
can be incremented, decremented or
left unchanged by a transition.
Formally, a one-counter net (Hofman and Totzke, 2018) is a tuple O=⟨Q,Σ,δ⟩ where Q is a finite set of states, Σ is an alphabet and δ⊆Q×Σ×{−1,0,1}×Q is a set of transitions.
A configuration of O is a pair qn consisting of a state q∈Q and a value n∈N for the counter.
Given two configurations qn,q′n′∈Q×N we write qnaq′n′ and call it a a-step (or simply step) if there exists a transition (q,a,d,q′)∈δ such that n′=n+d.
Given qn∈Q×N, the trace setT(qn)⊆Σ∗ of an OCN is defined as follows:
[TABLE]
Observe that Zϵqn={qn} and Zuqn is a finite set for every word u∈Σ∗.
Let us consider the poset ⟨N⊥≜N∪{⊥},≤N⊥⟩ where ⊥≤N⊥n holds for all n∈N⊥, while for all n,n′∈N, n≤N⊥n′ is the standard ordering relation between numbers.
For a finite set of states S⊆Q×N, define the so-called macro state MS:Q→N⊥ as follows:
[TABLE]
where max∅≜⊥. Let us define the following quasiorder ≤qnr⊆Σ∗×Σ∗:
[TABLE]
Example 5.12.
Figure 3 depicts an OCN over the singleton alphabet Σ={a}.
For O we have the following sets:
[TABLE]
Hence, we have that:
[TABLE]
Therefore, the words ϵ,a and aa are pairwise incomparable for ≤q10r, while we have that aa≤q10raaa and ϵ≤q10raaa. ◊
Lemma 5.13.
Let O be an OCN. For any configuration qn of O, ≤qnr is a right T(qn)-consistent decidable wqo.
Proof.
It follows from Dickson’s Lemma (Sakarovitch, 2009, Section II.7.1.2) that ≤qnr is a wqo.
Since Zuqn and Zvqn are finite sets of configurations, the macro state functions
MZuqn and MZvqn are computable, hence the relation ≤qnr is decidable.
If u∈T(qn) and v∈/T(qn) then u≤qnrv, otherwise we would have that
MZuqn(q′)=⊥ for some q′∈Q, hence MZvqn(q′)=⊥, and this would be
a contradiction because Zvqn=∅, so that MZvqn(q′)=⊥.
Finally, let us show that
u≤qnrv implies ua≤qnrva
for all a∈Σ, since, by (13), this is equivalent to the fact that ≤qnr is right monotonic.
We proceed by contradiction.
Assume that u≤qnrv and ∃q′∈Q, MZuaqn(q′)≤N⊥MZvaqn(q′).
Then, m1≜max{n∣pn∈Zuaqn}≤N⊥m2≜max{n∣pn∈Zvaqn}, which implies, since
m1=⊥, that
m1,m2∈N and m1>m2.
Thus, for all (q,a,d,q′)∈δ we have q′(m1−d)∈Zuqn and q′(m2−d)∈Zvqn.
Since m1−d>m2−d we have that max{n∣pn∈Zuqn}>max{n∣pn∈Zvqn}, which contradicts u≤qnrv. ∎
By Theorem 5.3,
Lemma 5.13 and the decidability of membership u∈\scaleto?3.5ptT(qn),
the following known decidability result for inclusion of regular languages into traces of OCNs (Jančar
et al., 1999, Theorem 3.2) is systematically derived as a consequence of our algorithmic framework.
Corollary 5.14.
Let A be a FA and O be an OCN. For any configuration qn of O, the language inclusion problem
L(A)⊆T(qn) is decidable.
Example 5.15.
Consider the OCN of Figure 3 and the problem of deciding whether Σ∗=a∗ is included into T(q00), i.e., whether the trace set of O is universal.
By considering
the equation X=Xa∪{ϵ} which defines Σ∗, it turns
out that the
Kleene iterates computed by Algorithm FAIncW when using the abstract inclusion check
given by ⊑≤q00r are as follows:
[TABLE]
We have that Y(4)⊑≤q00rY(3) because
aa≤q00raaa holds, as shown in Example 5.12, so that
the output of \textscKleene is Y(3)={aa,a,ϵ}.
Since {aa,a,ϵ} is a set of traces of O (i.e. {aa,a,ϵ}⊆T(q00)) we conclude that O is universal. ◊
Moreover, by exploiting
Lemma 5.13 and (Hofman
et al., 2013, Theorem 20), the following result settles a conjecture made by de Luca and Varricchio (1994, Section 6) on the right Nerode quasiorder
for traces of OCNs.
Lemma 5.16.
The right Nerode quasiorder ≦T(qn)r is an undecidable well-quasiorder.
Proof.
As already recalled, de Luca and Varricchio (1994, Section 2, point 4)
show that ≦T(qn)r is maximum in the set of all right T(qn)-consistent quasiorders, so that u≤qnrv⇒u≦T(qn)rv, for all u,v∈Σ∗.
By Lemma 5.13, ≤qnr is a wqo, so that ≦T(qn)r is a wqo as well.
Undecidability of ≦T(qn)r follows from the undecidability of the trace inclusion problem for nondeterministic OCNs (Hofman
et al., 2013, Theorem 20) by an argument similar to the automata case.
∎
It is worth remarking that, by Lemma 5.6 (a), the left and right Nerode quasiorders ≦T(qn)l and ≦T(qn)r are T(qn)-consistent.
However, the left Nerode quasiorder does not need to be a wqo, otherwise T(qn) would be regular.
We conclude this section by conjecturing that our framework could be instantiated for extending
Corollary 5.14 to traces of Petri Nets, a result
which is already known to be true (Jančar
et al., 1999).
6. A Novel Perspective on the Antichain Algorithm
In this section we
will show how
to solve the language inclusion problem by computing Kleene iterates
in an abstract domain of ℘(Σ∗) as
defined by a Galois connection.
This is of practical interest since it allows us to decide a language inclusion problem L(A)⊆L2 by manipulating an
automaton representation for L2.
6.1. A Language Inclusion Algorithm Using Galois Connections
The next result provides a formulation of Theorem 4.7
by using a Galois Connection ⟨℘(Σ∗),⊆⟩\galoisαγ⟨D,≤D⟩
rather than a closure operator ρ∈uco(℘(Σ∗) and shows
how to design
an algorithm that solves a language inclusion
L(A)⊆L2 by computing Kleene iterates on the abstract domain D.
Theorem 6.1.
Let A=⟨Q,δ,I,F,Σ⟩ be a FA and L2∈℘(Σ∗).
Let ⟨D,≤D⟩ be a poset and
⟨℘(Σ∗),⊆⟩\galoisαγ⟨D,≤D⟩ be a GC.
Assume that the following properties hold:
(i)
L2∈γ(D)* and for all a∈Σ and X∈℘(Σ∗), γα(aX)=γα(aγα(X)).*
2. (ii)
⟨D,≤D,⊔,⊥D⟩* is an effective domain, meaning that: ⟨D,≤D,⊔,⊥D⟩ is an ACC join-semilattice with bottom ⊥D,
every element of D has a finite representation, the binary relation
≤D is decidable and the binary lub ⊔ is computable.*
3. (iii)
There is an algorithm, say Pre♯, which computes α\compPreA\compγ.
4. (iv)
There is an algorithm, say ϵ♯, which computes α(\vvϵF).
5. (v)
There is an algorithm, say Incl♯, which decides
\vvX♯≤Dα(\vvL2I), for all
\vvX♯∈α(℘(Σ∗))∣Q∣.
Let ρ≜γα∈uco(℘(Σ∗)), so that hypothesis (i) can be stated as
ρ(L2)=L2 and ρ(aX)=ρ(aρ(X)), and this allows us to apply
Corollary 4.4.
It turns out that:
[TABLE]
Thus, by hypotheses (ii), (iii) and (iv), it turns out that
\textscKleene(≤D,λ\vvX♯.ϵ♯⊔Pre♯(\vvX♯),\vv⊥D) is an algorithm computing the least fixpoint
lfp(λ\vvX♯.α(\vvϵF)⊔α(PreA(γ(\vvX♯)))). In particular,
(ii), (iii) and (iv) ensure that the Kleene iterates of
λ\vvX♯.ϵ♯⊔Pre♯(\vvX♯)
starting from \vv⊥D
are computable and finitely many and that
it is decidable when the iterates converge for ≤D, namely, reach the least fixpoint.
Finally, hypothesis (v) ensures the
decidability of the ≤D-inclusion check of this least fixpoint
in α(\vvL2I).
∎
It is worth pointing out that, analogously to Theorem 4.6,
the above Theorem 6.1 can be also stated in a symmetric version
for right (rather than left) concatenation.
6.2. Antichains as a Galois Connection
Let A1=⟨Q1,δ1,I1,F1,Σ⟩ and A2=⟨Q2,δ2,I2,F2,Σ⟩ be two FAs
and consider
the state-based left L(A2)-consistent wqo
⩽A2l defined by (15).
Theorem 5.3 shows that Algorithm FAIncW decides L(A1)⊆L(A2) by
computing vectors of finite sets of words.
Since u⩽A2lv⇔preuA2(F2)⊆prevA2(F2), we can equivalently consider
the
set of states preuA2(F2)∈℘(Q2) rather than
a word u∈Σ∗.
This observation suggests to design a version of Algorithm FAIncW that
computes Kleene iterates on the poset
⟨AC⟨℘(Q2),⊆⟩,⊑⟩ of antichains
of sets of states of the complete lattice ⟨℘(Q2),⊆⟩.
In order to do this, ⟨AC⟨℘(Q2),⊆⟩,⊑⟩ is viewed as an abstract domain through the following maps α:℘(Σ∗)→AC⟨℘(Q2),⊆⟩ and γ:AC⟨℘(Q2),⊆⟩→℘(Σ∗). Moreover, we use
the abstract function PreA1A2:(AC⟨℘(Q2),⊆⟩)∣Q1∣→(AC⟨℘(Q2),⊆⟩)∣Q1∣ defined as follows:
[TABLE]
where ⌊X⌋ is the unique minor set w.r.t. subset inclusion
of X⊆℘(Q2).
Observe that the functions α and PreA1A2 are well-defined because minors of finite subsets of ℘(Q2) are uniquely defined antichains.
Lemma 6.2.
The following properties hold:
(a)
⟨℘(Σ∗),⊆⟩\galoisαγ⟨AC⟨℘(Q2),⊆⟩,⊑⟩* is a GC.*
2. (b)
γ\compα=ρ⩽A2l.
3. (c)
PreA1A2=α\compPreA1\compγ.
Proof.
(a)
Let us first observe that α is well-defined: in fact,
α(X) is an antichain of ⟨℘(Q2),⊆⟩ since it is a minor for the well-quasiorder ⊆ and, therefore, it is finite.
Then, for all X∈℘(Σ∗) and
Y∈AC⟨℘(Q2),⊆⟩,
it turns out that:
[TABLE]
2. (b)
For all X∈℘(Σ∗):
[TABLE]
3. (c)
For all \vvX∈(AC⟨℘(Q2),⊆⟩)∣Q1∣:
[TABLE]
Thus, by Lemma 5.8 and
Lemma 6.2, it turns out that the GC ⟨℘(Σ∗),⊆⟩\galoisαγ⟨AC⟨℘(Q2),⊆⟩,⊑⟩ and the abstract
function PreA1A2 satisfy the hypotheses (i)-(iv) of Theorem 6.1.
In order to obtain an algorithm for deciding L(A1)⊆L(A2) it remains to show that the hypothesis (v) of Theorem 6.1 holds, i.e.,
there is an algorithm to decide whether \vvY⊑α(\vvL2I2) for every \vvY∈α(℘(Σ∗))∣Q1∣.
Notice that the Kleene iterates of λ\vvX♯.α(\vvϵF1)⊔PreA1A2(\vvX♯) of Theorem 6.1 are vectors of antichains in ⟨AC⟨℘(Q2),⊆⟩,⊑⟩, where
each component is indexed by some q∈Q1 and represents,
through its minor, a set of sets of states that are predecessors of F2 in A2 through a word u generated by A1 from that state q, i.e., preuA2(F2) with u∈Wq,F1A1.
Since ϵ∈Wq,F1A1 for all q∈F1 and preϵA2(F2)=F2, the first
iteration of \textscKleene gives the vector α(\vvϵF1)=⟨ψ∅F2(q∈\scaleto?3.5ptF1)⟩q∈Q1.
Let us also observe that by taking the minor of each vector component,
we are considering smaller sets which still preserve the relation ⊑ since
the following equivalences hold: A⊑B⇔⌊A⌋⊑B⇔A⊑⌊B⌋⇔⌊A⌋⊑⌊B⌋.
Let ⟨Yq⟩q∈Q1 be the output of
\textscKleene(⊑,λ\vvX♯.α(\vvϵF1)⊔PreA1A2(\vvX♯),\vv∅).
Hence, we have that, for each component q∈Q1, Yq=⌊{preuA2(F2)∣u∈Wq,F1A1}⌋ holds.
Whenever the inclusion L(A1)⊆L(A2) holds, all the sets of states in Yq for some initial state q∈I1 are predecessors of F2 in A2 through words in L(A2), so that for
each q∈I1 and S∈Yq, S∩I2=∅ must hold.
As a result, the following state-based
algorithm FAIncS (S stands for state) decides the
inclusion L(A1)⊆L(A2) by computing on the abstract domain of antichains ⟨AC⟨℘(Q2),⊆⟩,⊑⟩.
Theorem 6.3.
The algorithm FAIncS decides the inclusion problem L(A1)⊆L(A2).
Proof.
We show that all the hypotheses (i)-(v) of Theorem 6.1 are satisfied for the abstract domain ⟨D,≤D⟩=⟨AC⟨℘(Q2),⊆⟩,⊑⟩ as defined by the GC of Lemma 6.2.
(i)
Since ρ≤A2l(X)=γ(α(X)), it follows from Lemmata 5.2 and 5.8 that L2∈γ(D).
Moreover, by Lemma 5.2 (b) with ρ≤A2l=γα, we have that
for all a∈Σ, X∈℘(Σ∗), γ(α(aX))=γ(α(aγ(α(X)))).
2. (ii)
⟨AC⟨℘(Q2),⊆⟩,⊑,⊔,∅⟩ is an effective domain
because
Q2 is finite.
3. (iii)
By Lemma 6.2 (c) we have that
α(PreA1(γ(\vvX♯)))=PreA1A2(\vvX♯) for all \vvX♯∈α(℘(Σ∗))∣Q1∣, and PreA1A2 is computable.
4. (iv)
α({ϵ})={F2} and α(∅)=∅, hence α(\vvϵF1) is trivial to compute.
5. (v)
Since α(\vvL2I1)=⟨α(ψΣ∗L2(q∈\scaleto?3.5ptI1))⟩q∈Q1, for all \vvY∈α(℘(Σ∗))∣Q1∣ the relation ⟨Yq⟩q∈Q1⊑α(\vvL2I1) trivially holds for all components q∈/I1, since α(Σ∗) is the greatest antichain.
For the components q∈I1, it suffices to show that
Yq⊑α(L2)⇔∀S∈Yq,S∩I2=∅, which is the check performed by lines 2-5 of algorithm FAIncS:
[TABLE]
Thus, by Theorem 6.1, the algorithm FAIncS solves the inclusion problem L(A1)⊆L(A2). ∎
6.3. Relationship to the Antichain Algorithm
De Wulf et al. (2006) introduced two so-called antichain algorithms, called
forward and backward, for deciding the universality of the language accepted by a FA, i.e., whether the language is Σ∗ or not.
Then, they extended the backward algorithm in order to decide inclusion of languages accepted by FAs.
In what follows we show that the above algorithm FAIncS is equivalent to the corresponding extension of the forward antichain algorithm and, therefore, dual to the backward antichain algorithm for language inclusion put forward by De Wulf et al. ([)Theorem 6]DBLP:conf/cav/WulfDHR06.
In order to do this, we first define the poset of antichains in which the forward antichain algorithm computes its fixpoint.
Then, we give a formal definition of the forward antichain algorithm for deciding language inclusion and show that this algorithm coincides with FAIncS when applied to the reverse automata.
Since language inclusion between the languages generated by two FAs holds iff inclusion holds between the languages generated by their reverse FAs, this entails that our algorithm FAIncS is equivalent to the forward antichain algorithm.
Consider a language inclusion problem
L(A1)⊆L(A2) where
A1=⟨Q1,δ1,I1,F1,Σ⟩ and A2=⟨Q2,δ2,I2,F2,Σ⟩.
Let us consider the following poset of antichains
⟨AC⟨℘(Q2),⊆⟩,⊑⟩ where
[TABLE]
and notice that ⊑ coincides with the reverse
⊑−1 of the relation defined by (1).
As observed by De Wulf et al. ([)Lemma 1]DBLP:conf/cav/WulfDHR06, it turns out that ⟨AC⟨℘(Q2),⊆⟩,⊑,⊔,⊓,{∅},∅⟩ is a finite lattice, where ⊔ and ⊓ denote, resp., lub and glb, and {∅} and ∅ are, resp., the least and greatest elements.
This lattice ⟨AC⟨℘(Q2),⊆⟩,⊑⟩ is the domain in which the forward antichain algorithm computes on for deciding language universality (De
Wulf et al., 2006, Theorem 3).
The following result extends this forward algorithm in order to decide language inclusion.
where PostA1A2(⟨Xq⟩q∈Q1)≜⟨⌊{postaA2(S)∈℘(Q2)∣∃a∈Σ,q′∈Q1,q∈δ1(q′,a)∧S∈Xq′}⌋⟩q∈Q1.
Then, L(A1)⊈L(A2) if and only if there exists q∈F1 such that \vvFPq⊑{F2c}.
Proof.
Let us first introduce some notation to describe the forward antichain algorithm by De Wulf et. al (2006) which decides L(A1)⊆L(A2).
Let us consider the poset
⟨Q1×℘(Q2),⊆×⟩ where (q_{1},S_{1})\subseteq_{\times}(q_{2},S_{2})\stackrel{{\scriptstyle{\mbox{\tiny\triangle}}}}{{\Leftrightarrow}}q_{1}=q_{2}\wedge S_{1}\subseteq S_{2}. Then,
let
⟨AC⟨Q1×℘(Q2),⊆×⟩,⊑×,⊔×,⊓×⟩ be the lattice of antichains over ⟨Q1×℘(Q2),⊆×⟩ where:
[TABLE]
Also, let Post:AC⟨Q1×℘(Q2),⊆×⟩→AC⟨Q1×℘(Q2),⊆×⟩ be defined as follows:
[TABLE]
Then, the dual of the backward antichain algorithm in (De
Wulf et al., 2006, Theorem 6) states that L(A1)⊈L(A2) iff there exists q∈F1 such that FP⊑×{(q,F2c)} where
[TABLE]
We observe that for some X∈AC⟨Q1×℘(Q2),⊆×⟩, a pair (q,S)∈Q1×℘(Q2) such that (q,S)∈X is used by
(De
Wulf et al., 2006, Theorem 6) simply as
a way to associate states q of A1 with sets S of states of A2.
In fact, an antichain
X∈AC⟨Q1×℘(Q2),⊆×⟩
can be equivalently formalized
by a vector ⟨{S∈℘(Q2)∣(q,S)∈X}⟩q∈Q1∈(AC⟨℘(Q2),⊆⟩)∣Q1∣ whose components are indexed by states q∈Q1 and are antichains of set of states in AC⟨℘(Q2),⊆⟩.
Correspondingly, we consider
the lattice ⟨AC⟨℘(Q2),⊆⟩,⊑⟩, where for
all X,Y∈AC⟨℘(Q2),⊆⟩:
[TABLE]
Then, these definitions allow us to replace Post by an equivalent function
[TABLE]
that transforms vectors of antichains as follows:
[TABLE]
In turn, the above FP∈AC⟨Q1×℘(Q2),⊆×⟩ is replaced by the
following equivalent vector:
[TABLE]
Finally, the condition
∃q∈F1,FP⊑×{(q,F2c)} is equivalent
to ∃q∈F1,\vvFPq⊑{F2c}.
∎
Let us recall that AR denotes the reverse automaton of A, where arrows are flipped and the initial/final states become final/initial.
Note that language inclusion can be decided by considering the reverse automata since L(A1)⊆L(A2)⇔L(A1R)⊆L(A2R) holds.
Furthermore, let us observe that PostA1A2=PreA1RA2R.
We therefore obtain the following consequence of Theorem 6.4.
Corollary 6.5.
Let
[TABLE]
Then, L(A1)⊈L(A2) iff ∃q∈I1,\vvFPq⊑{I2c}.
Since ⊑=⊑−1, we have that ⊓=⊔, ⊔=⊓ and the greatest element ∅ for ⊑ is the least element for ⊑.
Moreover, by (20), α(\vvϵF1)=⟨ψ∅{F2}(q∈\scaleto?3.5ptF1)⟩q∈Q1.
Therefore, we can rewrite the vector
\vvFP of
Corollary 6.5 as
[TABLE]
which is precisely the least fixpoint in ⟨(AC⟨℘(Q2),⊆⟩)∣Q1∣,⊑⟩ of PreA1A2 above
α(\vvϵF1).
Hence, it turns out that the Kleene iterates of the least fixpoint computation
that converge to \vvFP exactly coincide with the iterates computed by the \textscKleene procedure of the state-based algorithm
FAIncS.
In particular, if \vvY is the output vector of
\textscKleene(⊑,λ\vvX.α(\vvϵF1)⊔PreA1A2(\vvX),\vv∅)
at line 1 of
FAIncS then \vvY=\vvFP.
Furthermore, ∃q∈I1,\vvFPq⊑{I2c}⇔∃q∈I1,∃S∈\vvFPq,S∩I2=∅.
Summing up, the ⊑-lfp algorithm FAIncS exactly coincides with the ⊑-gfp antichain algorithm as given by Corollary 6.5.
We can easily derive an antichain algorithm which is perfectly equivalent to FAIncS by considering the antichain
lattice ⟨AC⟨℘(Q2),⊇⟩,⊑⟩ for the dual lattice ⟨℘(Q2),⊇⟩
and by replacing the functions
α, γ and PreA1A2 of Lemma 6.2, resp., with the following dual versions:
[TABLE]
where cpreuA2(S)≜(preuA2(Sc))c for u∈Σ∗.
When using these functions, the corresponding algorithm computes
on the abstract domain ⟨AC⟨℘(Q2),⊇⟩,⊑⟩ and
it turns out that L(A1)⊆L(A2) iff \textscKleene(⊑,λ\vvX♯.αc(\vvϵF1)⊔CPreA1A2(\vvX♯),\vv∅)⊑αc(\vvL2I1).
This language inclusion algorithm coincides with the backward antichain algorithm defined by De Wulf et al. ([)Theorem 6]DBLP:conf/cav/WulfDHR06 since both compute on the same lattice, ⌊X⌋ corresponds to the maximal (w.r.t. set inclusion) elements of X, αc({ϵ})={F2c} and for all X∈αc(℘(Σ∗)), we have that X⊑αc(L2)⇔∀S∈X,I2⊈S.
We have thus shown that the two forward/backward antichain algorithms introduced by De Wulf et al. (2006) can be systematically derived by instantiating our framework.
The original antichain algorithms were later improved by Abdulla et al. (2010) and, subsequently, by Bonchi and Pous (2013). Among their improvements, they showed how to exploit a precomputed binary relation between pairs of states of the input automata such that language inclusion holds for all the pairs in the relation.
When that binary relation is a simulation relation, our framework allows to partially match their results by using the simulation-based quasiorder ⪯Ar defined in Section 5.3.2.
However, this relation ⪯Ar does not consider pairs of states Q2×Q2 whereas the aforementioned algorithms do.
7. Inclusion for Context Free Languages
A context-free grammar (CFG) is a tuple G=⟨V,Σ,P⟩ where V={X0,…,Xn} is a finite set of variables including a start symbol X0, Σ is a finite alphabet of terminals and P is a finite set of productions Xi→β where β∈(V∪Σ)∗.
We assume, for simplicity and without loss of generality, that CFGs are in Chomsky Normal Form (CNF), that is, every production Xi→β∈P is such that β∈(V×V)∪Σ∪{ϵ} and if β=ϵ then i=0 (Chomsky, 1959).
We also assume that for all Xi∈V there exists a production Xi→β∈P, otherwise Xi can be safely removed from V.
Given two strings w,w′∈(V∪Σ)∗ we write w→w′ iff there exists u,v∈(V∪Σ)∗ and X→β∈P such that w=uXv and w′=uβv.
We denote by →∗ the reflexive-transitive closure of →.
The language generated by a G is L(G)≜{w∈Σ∗∣X0→∗w}.
7.1. Extending the Framework to CFGs
Similarly to the case of automata, a CFG G=(V,Σ,P) in CNF induces the following set of equations:
[TABLE]
Given a subset of variables S⊆V of a grammar, the set of words generated from some variable in S is defined as
[TABLE]
When S={X} we slightly abuse the notation and write WXG.
Also, we drop the superscript G when the grammar is clear from the context.
The language generated by G is therefore L(G)=WX0G.
We define the vector \vvb∈℘(Σ∗)∣V∣ and the function FnG:℘(Σ∗)∣V∣→℘(Σ∗)∣V∣, which are used to formalize the fixpoint equations in Eqn(G), as follows:
[TABLE]
Notice that λ\vvX.\vvb∪FnG(\vvX) is a well-defined monotonic function in ℘(Σ∗)∣V∣→℘(Σ∗)∣V∣, which therefore has the least fixpoint
⟨Yi⟩i∈[0,n]=lfp(λ\vvX.\vvb∪FnG(\vvX)). It is known (Ginsburg and Rice, 1962) that the language L(G) accepted by G is such that L(G)=Y0.
Example 7.1.
Consider the CFG G=⟨{X0,X1},{a,b},{X0→X0X1∣X1X0∣b,X1→a}⟩ in CNF.
The corresponding equation system is
[TABLE]
so that
[TABLE]
Moreover, we have that \vvb∈℘(Σ∗)2 and FnG:℘(Σ∗)2→℘(Σ∗)2 are given by
[TABLE]
It turns out that
[TABLE]
where \vvL2X0≜⟨ψΣ∗L2(i=\scaleto?3.5pt0)⟩i∈[0,n].
Theorem 7.2.
Let G=(V,Σ,P) be a CFG in CNF.
If ρ∈uco(℘(Σ∗)) is backward complete for both λX.Xa and λX.aX, for all a∈Σ then ρ is backward complete for λ\vvX.\vvb∪FnG(\vvX).
Proof.
Let us first show that backward completeness for left and right concatenation can be extended from letter to words.
We give the proof for left concatenation, the right case is symmetric.
We prove that ρ(wX)=ρ(wρ(X)) for every w∈Σ∗.
We proceed by induction on ∣w∣≥0.
The base case ∣w∣=0 iff w=ϵ is trivial because ρ is idempotent.
For the inductive case ∣w∣>0 let w=au for some
u∈Σ∗ and a∈Σ, so that:
[TABLE]
Next we turn to the binary concatenation case, i.e., we prove that ρ(YZ)=ρ(ρ(Y)ρ(Z)) for all Y,Z∈℘(Σ∗):
[TABLE]
Then, the proof follows the same lines of the proof of Theorem 4.3.
Indeed, it follows from the definition of FnG(⟨Xi⟩i∈[0,n])
that:
[TABLE]
Hence, by a straightforward
componentwise application on vectors in ℘(Σ∗)∣V∣, we obtain that ρ is backward complete for FnG.
Finally, ρ is backward complete for
λ\vvX.(\vvb∪FnG(\vvX)),
because:
[TABLE]
The following result, which is an adaptation of Theorem 4.7 to
grammars, relies on Theorem 7.2 for designing
an algorithm that solves the
inclusion problem L(G)⊆L2
by exploiting a language abstraction ρ that satisfies some requirements
of backward completeness and computability.
Theorem 7.3.
Let G=⟨V,Σ,P⟩ be a CFG in CNF,
L2∈℘(Σ∗)
and ρ∈uco(Σ∗).
Assume that the following properties hold:
(i)
The closure ρ is backward complete for both λX∈℘(Σ∗).aX and λX∈℘(Σ∗).Xa for all a∈Σ and
satisfies ρ(L2)=L2.
2. (ii)
ρ(℘(Σ∗))* does not contain
infinite ascending chains.*
3. (iii)
If X,Y∈℘(Σ∗) are finite sets of words then
the inclusion ρ(X)⊆\scaleto?3.5ptρ(Y) is decidable.
4. (iv)
If Y∈℘(Σ∗) is a finite set of words then
the inclusion ρ(Y)⊆\scaleto?3.5ptL2 is decidable.
Let us instantiate the general algorithmic framework provided by Theorem 7.3 to the class of closure operators induced by quasiorder relations on words.
As a consequence of Lemma 5.2,
we have the following characterization of L-consistent quasiorders.
Lemma 7.4.
Let L∈℘(Σ∗) and ⩽L be a quasiorder on Σ∗.
Then, ⩽L is a L-consistent quasiorder on Σ∗ if and only if
(a)
ρ⩽L(L)=L, and
2. (b)
ρ⩽L* is backward complete for
for λX.aX and λX.Xa for all a∈Σ.*
Analogously to Section 5.1 for automata, Theorem 7.3
induces an algorithm for deciding the language inclusion L(G)⊆L2 for any CFG G and regular language L2.
More in general, given a language L2∈℘(Σ∗) whose membership problem is decidable and a decidable L2-consistent wqo, the following algorithm CFGIncW (CFGInclusion based on Words) decides
L(G)⊆L2.
Theorem 7.5.
*Let G=⟨Q,δ,I,F,Σ⟩ be a CFG and let L2∈℘(Σ∗) be a language such that:
(i) membership u∈\scaleto?3.5ptL2 is decidable;
(ii) there exists a decidable L2-consistent wqo on Σ∗.
Then, algorithm CFGIncW decides the inclusion L(G)⊆L2.*
Proof.
The proof is analogous to the proof of Theorem 5.3:
it applies Theorem 7.3 and Lemma 7.4 in the same way of the proof of Theorem 5.3 where the role of
a left L2-consistent wqo on Σ∗
is replaced by a L2-consistent wqo.
∎
7.2.1. Myhill and State-based Quasiorders
In the following, we will consider two quasiorders on Σ∗ and we will show that they fulfill the requirements of Theorem 7.5, so that they correspondingly yield algorithms for deciding the language inclusion L(G)⊆L2 for every CFG G and regular language L2.
The context for a language L∈℘(Σ∗) w.r.t. a given word w∈Σ∗ is defined as usual:
[TABLE]
Correspondingly, let us define the following quasiorder relation on ≦L⊆Σ∗×Σ∗:
[TABLE]
De Luca and Varricchio (1994, Section 2) call ≦L the Myhill quasiorder relative to L.
The following result is the analogue
of Lemma 5.6 for the Nerode quasiorder:
it shows that the Myhill quasiorder is the weakest
L2-consistent quasiorder for which the above algorithm CFGIncW can be instantiated to decide a language inclusion L(G)⊆L2.
Lemma 7.6.
Let L∈℘(Σ∗).
(a)
≦L* is a L-consistent quasiorder.
If L is regular then, additionally, ≦L is a decidable wqo.*
2. (b)
If ⩽ is a L-consistent quasiorder on Σ∗ then ρ≦L(℘(Σ∗))⊆ρ⩽(℘(Σ∗)).
Proof.
The proof follows the same lines of the proof of Lemma 5.6.
Let us consider (a).
De Luca and Varricchio (1994, Section 2) observe that ≦L is monotonic.
Moreover, if
L is regular then ≦L is a wqo (de Luca and
Varricchio, 1994, Proposition 2.3).
Let us observe that given u∈L and v∈/L we have that (ϵ,ϵ)∈ctxL(u) while (ϵ,ϵ)∈/ctxL(v).
Hence, ≦L is a L-consistent quasiorder.
Finally, if L is regular then ≦L is clearly decidable.
Let us consider (b).
By the characterization of L-consistent quasiorders of Lemma 7.4,
De Luca and Varricchio (1994, Section 2, point 4) observe that ≦L is maximum in the set of all L-consistent quasiorders, i.e. every L-consistent quasiorder ⩽ is such that
x⩽y⇒x≦Ly.
As a consequence, ρ⩽(X)⊆ρ≦L(X) holds for all X∈℘(Σ∗), namely,
ρ≦L(℘(Σ∗))⊆ρ⩽(℘(Σ∗)).
∎
Example 7.7.
Let us illustrate the use of the Myhill quasiorder ≦L(A) in Algorithm CFGIncW for solving the language inclusion L(G)⊆L(A), where G is the CFG in Example 7.1 and A is the FA depicted in Figure 4.
The equations for G are as follows:
[TABLE]
We write {(S,T)}∪{(X,Y)} to compactly denote a set {(u,v)∣(u,v)∈S×T∪X×Y}.
Then, we have the following contexts (among others) for L=L(A)=(b+ab∗a)(a+b)∗:
[TABLE]
Notice that a≦Lba and
ctxL(ab)=ctxL(a) and ctxL(ba)=ctxL(baa)=ctxL(aab)=ctxL(aba).
Next, we show the computation of the Kleene iterates according to Algorithm CFGIncW using ⊑≦L by recalling from
Example 7.1 that \vvb=⟨{b},{a}⟩ and
FnG(⟨X0,X1⟩)=⟨X0X1∪X1X0,∅⟩:
[TABLE]
It turns out that ⟨{baa,aba,ba,aab,ab,b},{a}⟩⊑≦L⟨{ba,ab,b},{a}⟩
because a≦Lbaa, a≦Laba, a≦Laab hold, so that
\textscKleene(⊑≦L,λ\vvX.\vvb∪FnG(\vvX),\vv∅) stops with \vvY(3) and
outputs \vvY=⟨{ba,ab,b},{a}⟩.
Since ab∈\vvY0 but ab∈/L(A), Algorithm CFGIncW correctly
concludes that L(G)⊆L(A) does not hold. ◊
Similarly to Section 5.3, next we consider a state-based quasiorder that can be used with Algorithm CFGIncW.
First, given a FA A=⟨Q,δ,I,F,Σ⟩ we define the state-based equivalent of the context of a word w∈Σ∗ as follows:
[TABLE]
Then, the quasiorder ≤A on Σ∗
induced by A is defined as follows: for all u,v∈Σ∗,
[TABLE]
The following result is the analogue of Lemma 5.8 and
shows that ≤A is a L(A)-consistent well-quasiorder and, therefore, it can be used with Algorithm CFGIncW to solve a language inclusion L(G)⊆L(A).
Lemma 7.8.
The relation ≤A is a decidable L(A)-consistent wqo.
Proof.
For every u∈Σ∗, ctxA(u) is a finite and computable set, so that ≤A is a decidable wqo.
Next, we show that ≤A is L(A)-consistent according to Definition 5.1 (a)-(b).
(a) By picking u∈L(A) and v∈/L(A) we have that ctxA(u) contains a pair (qi,qf) with qi∈I and qf∈F while ctxA(v) does not, hence u≰Av.
(b) Let us check that ≤A is monotonic.
Observe that ctxA:⟨Σ∗,≤A⟩→⟨℘(Q2),⊆⟩ is monotonic.
Therefore, for all x1,x2∈Σ∗ and a,b∈Σ,
[TABLE]
For the Myhill wqo
≦L(A), it turns out that for all u,v∈Σ∗,
Let us illustrate the use of the state-based quasiorder ≤A to solve the language inclusion L(G)⊆L(A) of Example 7.7.
Here, among others, we have the following contexts:
[TABLE]
Moreover, ctxA(ba)=ctxA(baa)=ctxA(aab)=ctxA(aba).
Recall from Example 7.7 that for the Myhill quasiorder we have that a≦L(A)ba, while for the state-based quasiorder a≰Aba.
The Kleene iterates computed by Algorithm CFGIncW when using
⊑≤A are exactly the same of Example 7.7.
Here, it turns out that CFGIncW outputs \vvY(2)=⟨{ba,ab,b},{a}⟩ because
\vvY(3)=⟨{baa,aba,ba,aab,ab,b},{a}⟩⊑≦L⟨{ba,ab,b},{a}⟩=\vvY(2) holds: in fact, we have that
ba≤Abaa, ba≤Aaba, ba≤Aaab hold.
Since ab∈\vvY0(2) but ab∈/L(A), Algorithm CFGIncW derives that L(G)⊆L(A). ◊
7.3. An Antichain Inclusion Algorithm for CFGs
We can easily formulate an equivalent of
Theorem 6.1 for context-free languages, therefore
defining an algorithm for solving L(G)⊆L2
by computing on an abstract domain as defined by a Galois connection.
Theorem 7.10.
Let G=⟨V,Σ,P⟩ be a CFG in CNF and let L2∈℘(Σ∗).
Let ⟨D,≤D⟩ be a poset and
⟨℘(Σ∗),⊆⟩\galoisαγ⟨D,⊑⟩ be a GC.
Assume that the following properties hold:
(i)
L2∈γ(D)* and for every a∈Σ, X∈℘(Σ∗), γ(α(aX))=γ(α(aγ(α(X)))) and γ(α(Xa))=γ(α(γ(α(X))a)).*
2. (ii)
(D,≤D,⊔,⊥D)* is an effective domain, meaning that: (D,≤D,⊔,⊥D) is an ACC join-semilattice with bottom ⊥D,
every element of D has a finite representation, the binary relation
≤D is decidable and the binary lub ⊔ is computable.*
3. (iii)
There is an algorithm, say Fn♯(\vvX♯), which computes α\compFnG\compγ.
4. (iv)
There is an algorithm, say b♯, which computes α(\vvb).
5. (v)
There is an algorithm, say Incl♯, which decides
\vvX♯≤Dα(\vvL2X0), for all \vvX♯∈α(℘(Σ∗))∣V∣.
Similarly to what is done in Section 6.1,
in order to solve
an inclusion problem L(G)⊆L(A), where
A=⟨Q,δ,I,F,Σ⟩ is a FA,
we leverage Theorem 7.10
to systematically design a “state-based” algorithm that computes Kleene iterates
on the antichain poset ⟨AC⟨℘(Q×Q),⊆⟩,⊑⟩ viewed as an abstraction of ⟨℘(Σ∗),⊆⟩.
Here, the abstraction and concretization maps
α:℘(Σ∗)→AC⟨℘(Q×Q),⊆⟩ and
γ:AC⟨℘(Q×Q),⊆⟩→℘(Σ∗) and the function
FnGA:(AC⟨℘(Q×Q),⊆⟩)∣V∣→(AC⟨℘(Q×Q),⊆⟩)∣V∣ are defined
as follows:
[TABLE]
where ⌊X⌋ is the unique minor set w.r.t. subset inclusion
of some X⊆℘(Q×Q) and
X\compY≜{(q,q′)∈Q×Q∣(q,q′′)∈X,(q′′,q′)∈Y} denotes
the standard composition of two
relations X,Y⊆Q×Q. By
the analogue of Lemma 6.2 (the proof follows the same pattern
and is therefore omitted), it turns out that:
(a)
⟨℘(Σ∗),⊆⟩\galoisαγ⟨AC⟨℘(Q×Q),⊆⟩,⊑⟩ is a GC,
2. (b)
γ\compα=ρ⩽A,
3. (c)
FnGA=α\compFnG\compγ.
Thus, the GC ⟨℘(Σ∗),⊆⟩\galoisαγ⟨AC⟨℘(Q×Q),⊆⟩,⊑⟩ and the abstract
function FnGA satisfy the hypotheses (i)-(iv) of
Theorem 7.10. Here, the inclusion check
\vvX♯≤Dα(\vvL(A)X0) boils down to verify
that for the start component Y0 of the output ⟨Yi⟩i∈[0,n] of
\textscKleene(⊑,λ\vvX♯.α(\vvb)⊔FnGA(\vvX♯),\vv∅), for all R∈Y0, R does not contain
a pair (qi,qf)∈I×F. We therefore derive the following state-based
algorithm CFGIncS (S stands for state) that decides
an inclusion L(G)⊆L(A) on the abstract domain of antichains
AC⟨℘(Q×Q),⊆⟩.
Theorem 7.11.
The algorithm CFGIncS decides the inclusion problem L(G)⊆L(A).
Proof.
The proof follows the same pattern of the proof of Theorem 6.3. We just focus
on the inclusion check at lines 2-4, which is slightly different from
the check at lines 2-5 of Algorithm FAIncS. Let L2=L(A).
Since α(\vvL2X0)=⟨α(ψΣ∗L2(i=\scaleto?3.5pt0))⟩i∈[0,n], for all \vvY∈α(℘(Σ∗))∣V∣ the relation \vvY⊑α(\vvL2X0) trivially holds
for all components Yi with i=0.
For Y0, it is enough to prove that
Y0⊑α(L2)⇔∀R∈Yq,R∩(I×F)=∅:
[TABLE]
Hence, Theorem 7.10 entails that
Algorithm CFGIncS decides L(G)⊆L(A).
∎
The resulting algorithm CFGIncS shares some features with two previous related works.
On the one hand, it is related to the work of Hofmann and Chen (2014) which defines an abstract interpretation-based language inclusion decision procedure similar to ours.
Even though Hofmann and Chen’s algorithm and ours both manipulate sets of pairs of states of an automaton,
their abstraction is based on equivalence relations and not quasiorders.
Since quasiorders are strictly more general than equivalences our framework can be instantiated to
a larger class of abstractions, most importantly coarser ones.
Finally, it is worth pointing out
that Hofmann and Chen (2014) approach aims at including languages of finite and also infinite words.
A second related work is that of Holík and
Meyer (2015) who define an antichain-based algorithm manipulating sets of pairs of states.
However, they tackle the inclusion problem L(G)⊆L(A), where G is a grammar and A and automaton, by rephrasing it as a data flow analysis problem over a relational domain.
In this scenario, the solution of the problem requires the computation of a least fixpoint on the relational domain, followed by an inclusion check between sets of relations.
Then, they use the “antichain principle” to improve the performance of the fixpoint computation and, finally, they move from manipulating relations to manipulating pairs of states.
As a result, Holík and
Meyer (2015) devise an antichain algorithm for checking the inclusion L(G)⊆L(A).
By contrast to these two approaches, our design
technique is direct and systematic, since the algorithm CFGIncS is derived
from the known Myhill quasiorder.
We believe that our approach reveals the relationship between the original antichain algorithm by De
Wulf et al. (2006) for regular languages and the one by Holík and
Meyer (2015) for context-free languages, which is the relation between our algorithms FAIncS and CFGIncS.
Specifically, we have shown that these two algorithms are conceptually identical and just differ in the well-quasiorder used to define the abstract domain where
computations take place.
8. An Equivalent Greatest Fixpoint Algorithm
Let us assume that
g:C→C is a monotonic function on a complete lattice ⟨C,≤,∨,∧⟩ which admits
its unique right-adjoint g:C→C,
i.e., ∀c,c′∈C,g(c)≤c′⇔c≤g(c′) holds.
Then, Cousot (2000, Theorem 4) shows that the following equivalence holds:
for all c,c′∈C,
[TABLE]
This property has been used in (Cousot, 2000) to derive equivalent least/greatest fixpoint-based invariance proof methods for programs.
In the following, we use (23) to derive an algorithm for deciding the inclusion L(A1)⊆L(A2), which relies on the computation of a greatest fixpoint rather than a least fixpoint.
This can be achieved by exploiting the following simple observation, which defines an adjunction between concatenation and quotients
of sets of words.
Lemma 8.1.
For all X,Y∈℘(Σ∗) and w∈Σ∗, wY⊆Z⇔Y⊆w−1Z and Yw⊆Z⇔Y⊆Zw−1.
Proof.
By definition, for all u∈Σ∗, u∈w−1Z iff wu∈Z.
Hence, Y⊆w−1Z⇔∀u∈Y,wu∈Z⇔wY⊆Z.
Symmetrically, Yw⊆Z⇔Y⊆Zw−1 holds. ∎
Given a FA A=⟨Q,δ,I,F,Σ⟩, we define the function PreA:℘(Σ∗)∣Q∣→℘(Σ∗)∣Q∣ on Q-indexed vectors of
sets of words as follows:
[TABLE]
where, as usual, ⋂∅=Σ∗. It turns out that PreA is the usual weakest liberal precondition which is
right-adjoint
of PreA.
Lemma 8.2.
For all \vvX,\vvY∈℘(Σ∗)∣Q∣, PreA(\vvX)⊆\vvY⇔\vvX⊆PreA(\vvY).
Proof.
[TABLE]
∎
Hence, from equivalences (9) and (23) we obtain that for all
FAs A1 and L2∈℘(Σ∗):
[TABLE]
The following algorithm FAIncGfp decides the inclusion L(A1)⊆L2 when L2 is regular by implementing the greatest fixpoint
computation in equivalence (24).
The intuition behind Algorithm FAIncGfp is that
[TABLE]
Therefore, FAIncGfp computes the set ⋂{w−1L2∣w∈L(A1)}.
by using the automaton A1 and by
considering prefixes of L(A1) of increasing lengths. This means that
after n iterations of \textscKleene, the algorithm FAIncGfp has computed
[TABLE]
for every state q∈Q1.
The regularity of L2 and the property of regular languages of being closed under intersections and quotients entail that each Kleene
iterate of \textscKleene(⊇,λ\vvX.\vvL2I1∩PreA1(\vvX),\vvΣ∗)
is a (computable) regular language.
To the best of our knowledge, this gfp-based
language inclusion algorithm FAIncGfp has never been described in the literature before.
Next, we discharge the fundamental assumption guaranteeing
the correctness of this algorithm FAIncGfp: the Kleene iterates computed by FAIncGfp are finitely many.
In order to do that, we consider an abstract version of the greatest fixpoint computation exploiting
a closure operator which ensures that the abstract Kleene iterates are finitely many.
This closure operator ρ≤A2 will be defined by using an ordering relation ≤A2
induced by a FA A2 such that
L2=L(A2) and will be shown to be
forward complete for the function λ\vvX.\vvL2I1∩PreA1(\vvX)
used by FAIncGfp.
Forward completeness of abstract interpretations (Giacobazzi and
Quintarelli, 2001), also called
exactness (Miné, 2017, Definition 2.15), is different
from and orthogonal to backward completeness introduced in Section 3
and crucially used throughout Sections 4–7.
In particular, a remarkable consequence
of exploiting a forward complete abstraction is
that the Kleene iterates of the concrete and abstract greatest fixpoint computations coincide.
The intuition here is that this forward complete closure ρ≤A2 allows us to establish that all the Kleene iterates of \vvX.\vvL2I1∩PreA1(\vvX) belong to the image of the closure ρ≤A2, more precisely that every Kleene iterate is a language which is upward closed for ≤A2.
Interestingly, a similar phenomenon occurs in well-structured transition systems (Abdulla
et al., 1996; Finkel and
Schnoebelen, 2001).
Let us now describe in detail this abstraction.
A closure ρ∈uco(C) on a concrete domain C is forward complete for a monotonic function f:C→C if ρfρ=fρ holds.
The intuition here is that forward completeness means that no loss of precision
is accumulated when the output of a computation of fρ is approximated by ρ, or, equivalently, the concrete function f maps abstract elements
of ρ into abstract elements of ρ.
Dually to the case of backward completeness, forward completeness implies that gfp(f)=gfp(fρ)=gfp(ρfρ) holds, when these greatest fixpoints exist (this is the case, e.g., when C is a complete lattice).
When the function
f:C→C admits the right-adjoint f:C→C, i.e.,
f(c)≤c′⇔c≤f(c′) holds,
it turns out that forward and backward completeness are related by the following duality (Giacobazzi and
Quintarelli, 2001, Corollary 1):
[TABLE]
Thus, by (25), in the following result instead of
assuming the hypotheses implying that a closure ρ is forward complete for the right-adjoint PreA1 we
state some hypotheses which guarantee that ρ is backward complete for its left-adjoint, which, by Lemma 8.2, is PreA1.
Theorem 8.3.
Let A1=⟨Q1,δ1,I1,F1,Σ⟩ be a FA , L2 be a regular language and
ρ∈uco(℘(Σ∗)). Let us assume that:
(1)
ρ(L2)=L2;
2. (2)
ρ* is backward complete for λX.aX for all a∈Σ.*
Then, L(A1)⊆L2 iff \vvϵF1⊆gfp(λ\vvX.ρ(\vvL2I1∩PreA1(ρ(\vvX)))).
Moreover, the Kleene iterates of
λ\vvX.ρ(\vvL2I1∩PreA1(ρ(\vvX))) and λ\vvX.\vvL2I1∩PreA1(\vvX) from the initial value \vvΣ∗ coincide in lockstep.
Proof.
Theorem 4.3 shows that if ρ is backward complete for λX.aX for every a∈Σ then it is backward complete for PreA1.
Thus, by (25), ρ is forward complete for PreA1.
Then, it turns out that ρ is forward complete for λ\vvX.\vvL2I1∩PreA1(\vvX), because:
[TABLE]
Since, by forward completeness, gfp(λ\vvX.\vvL2I1∩PreA1(\vvX))=gfp(λ\vvX.ρ(\vvL2I1∩PreA1(ρ(\vvX)))), by equivalence (24), we conclude
that L(A1)⊆L2 iff \vvϵF1⊆gfp(λ\vvX.ρ(\vvL2I1∩PreA1(ρ(\vvX)))).
Finally, we observe that the Kleene iterates of λ\vvX.\vvL2I1∩PreA1(\vvX) and λ\vvX.ρ(\vvL2I1∩PreA1(ρ(\vvX))) starting from \vvΣ∗ coincide in lockstep since
ρ(\vvL2I1∩PreA1(ρ(\vvX)))=\vvL2I1∩PreA1(ρ(\vvX)) and
ρ(\vvL2I1)=\vvL2I1. ∎
We can now establish that the Kleene iterates of
\textscKleene(⊇,λ\vvX.\vvL2I1∩PreA1(\vvX),\vvΣ∗) are finitely many.
Let L2=L(A2), for some FA A2, and consider the corresponding left
state-based quasiorder ≤A2l on Σ∗ as defined by (15).
By Lemma 5.8, ≤A2l is a left L2-consistent wqo.
Furthermore, since Q2 is finite we have that both ≤A2l and (≤A2l)−1 are wqos, so that, in turn, ⟨ρ≤A2l(℘(Σ∗)),⊆⟩ is a poset which is both ACC and DCC.
In particular, the definition of ≤A2l implies that every chain in ⟨ρ≤A2l(℘(Σ∗)),⊆⟩ has at most 2∣Q2∣ elements, so that
if we compute 2∣Q2∣ Kleene iterates then we surely converge to the greatest fixpoint.
Moreover, as a consequence of the DCC we have that
\textscKleene(⊇,λ\vvX.ρ≤A2(\vvL2I1∩PreA1(ρ≤A2(\vvX))),\vvΣ∗)
always terminates,
thus implying that
\textscKleene(⊇,λ\vvX.\vvL2I1∩PreA1(\vvX),\vvΣ∗)
terminates as well, because their Kleene iterates go in lockstep as stated by Theorem 8.3. We have therefore shown the correctness of FAIncGfp.
Corollary 8.4.
The algorithm FAIncGfp decides the inclusion L(A1)⊆L2
Example 8.5.
Let us illustrate the greatest fixpoint algorithm FAIncGfp on the inclusion check
L(B)⊆L(A) where A is the FA in Fig. 1 and
B is the following FA:
q_{3}$$q_{4}$$b$$a$$a
By Corollary 8.4, the Kleene iterates of λ\vvY.\vvL(A){q3}∩PreB(\vvY)
are guaranteed to converge in finitely many steps. We have that
[TABLE]
Then, the Kleene iterates are as follows (we automatically
checked them by
the FAdo tool (Almeida et al., 2009)):
[TABLE]
Thus, \textscKleene outputs the vector
⟨Y3,Y4⟩=⟨L(A),(b∗a)+⟩.
Since ϵ∈L(A), FAIncGfp concludes that L(B)⊆L(A) holds.
◊
Finally, it is worth citing that Fiedor et al. (2019) put forward an algorithm for deciding WS1S formulae which relies on the same lfp computation used in FAIncS.
Then, they derive a dual gfp computation by relying on Park’s duality (Park, 1969): lfp(λX.f(X))=(gfp(λX.(f(Xc))c))c.
Their approach differs from ours since we use the equivalence (23) to compute a gfp, different from the lfp, which still allows us to decide the inclusion problem.
Furthermore, their algorithm decides whether a given automaton accepts ϵ and it is not clear how their algorithm could be extended for deciding language inclusion.
9. Future Work
We believe that this work only scratched the surface of the use of well-quasiorders on words for solving language inclusion problems.
In particular, our approach based on complete abstract interpretations allowed us to systematically derive well-known algorithms
, such as the antichain algorithms by De Wulf et al. (2006), as well as novel algorithms, such as FAIncGfp, for deciding the inclusion of regular languages.
Future directions include leveraging well-quasiorders for infinite words (Ogawa, 2004) to shed new light on the inclusion problem between ω-languages.
Our results could also be extended to inclusion of tree languages by relying on the extensions of Myhill-Nerode theorems for tree languages (Kozen, 1992).
Another interesting topic for future work is the enhancement of quasiorders using simulation relations.
Even though we already showed in this paper that simulations can be used to refine our language inclusion algorithms, we are not on par with the thoughtful use of simulation relations made by Abdulla et al. (2010) and Bonchi and Pous (2013).
Finally, let us mention that the correspondence between least and greatest fixpoint-based inclusion checks assuming complete abstractions was studied by Bonchi et al. (2018) with the aim of formally connecting sound up-to techniques and complete abstract interpretations.
Further possible developments include the study of our abstract interpretation-based algorithms for language inclusion from the viewpoint of sound up-to techniques.
Bibliography39
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1(1)
2Abdulla et al . (1996) Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. 1996. General decidability theorems for infinite-state systems. In Proc. of the 11th Annual IEEE Symp. on Logic in Computer Science (LICS’96) . IEEE Computer Society, Washington, DC, USA, 313–321.
3Abdulla et al . (2010) Parosh Aziz Abdulla, Yu-Fang Chen, Lukáš Holík, Richard Mayr, and Tomáš Vojnar. 2010. When Simulation Meets Antichains. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10) . Springer Berlin Heidelberg, 158–174. https://doi.org/10.1007/978-3-642-12002-2_14 · doi ↗
4Almeida et al . (2009) André Almeida, Marco Almeida, José Alves, Nelma Moreira, and Rogério Reis. 2009. F Ado and GU Itar: Tools for Automata Manipulation and Visualization. In Implementation and Application of Automata . Springer Berlin Heidelberg, 65–74. https://doi.org/10.1007/978-3-642-02979-0_10 · doi ↗
5Baier and Katoen (2008) Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking . The MIT Press.
6Bauer and Eickel (1976) Friedrich L. Bauer and Jürgen Eickel. 1976. Compiler Construction, An Advanced Course, 2nd Ed. Springer-Verlag, Berlin, Heidelberg.
7Bonchi et al . (2018) Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, and Dusko Pavlovic. 2018. Sound up-to techniques and Complete abstract domains. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’18) . ACM Press. https://doi.org/10.1145/3209108.3209169 · doi ↗
8Bonchi and Pous (2013) Filippo Bonchi and Damien Pous. 2013. Checking NFA Equivalence with Bisimulations Up to Congruence. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13) . ACM Press, 457–468. https://doi.org/10.1145/2429069.2429124 · doi ↗