=Paper=
{{Paper
|id=Vol-115/paper-10
|storemode=property
|title=Deciding Weak Monadic Second-order Logics using Complex-value Datalog
|pdfUrl=https://ceur-ws.org/Vol-115/10-toman.pdf
|volume=Vol-115
}}
==Deciding Weak Monadic Second-order Logics using Complex-value Datalog==
https://ceur-ws.org/Vol-115/10-toman.pdf
Deciding Weak Monadic Second-order Logics
using Complex-value Datalog
Gulay Unel and David Toman
{gunel,david}@cs.uwaterloo.ca
Abstract
In this paper we propose to use techniques developed for query eval-
uation of Complex-value Datalog queries for determining satisfiability of
WS1S and WS2S formulæ. This in turn can serve as a decision proce-
dure for Description Logics for which embeddings into WS1S and WS2S
have been proposed recently. We show that the use of database query
evaluation techniques—in particular the Magic Set rewriting of Datalog
queries—can considerably improve the performance of automata-based
reasoners such as the MONA system.
Keywords: WS1S, WS2S, Automata, Magic Sets, Complex-value Data-
log (Datalogcv ).
1 Introduction
Recently, WS1S and WS2S reasoners have been employed as reasoners for de-
scription logics (in particular, ALC) [15]. The experimental results have shown
that MONA—an automata-based WS1S/WS2S reasoner [12, 16]—can be used
for testing concept satisfiability. However, for terminological reasoning, the tech-
niques have run into serious state-space explosion problem—the size of a automa-
ton capturing the (language of) models of a given formula quickly exceeds the
space available in most computers. This is in stark contrast with (theoretically
sub-optimal) tableaux methods that in practice are able to handle much larger
problems [11, 13].
This paper introduces an approach that combats this problem. Unlike most
other approaches, however, that (usually) attempt to use compression techniques
based, e.g., on Binary Decision Diagrams (BDDs) [5] or state space factoring
(using, e.g., a guided automaton) [16], our approach is based on techniques
developed for query evaluation in deductive databases, in particular on the Magic
Set transformation [2]. In addition we briefly comment on the use of other query
optimization techniques such as goal reordering (also known as the join-order
selection).
The contributions of the paper are as follows: We show the connection be-
tween automata-based decision procedures for WS1S and WS2S and query eval-
uation in Complex-value Datalog (Datalogcv ). Indeed, the complexity of query
evaluation in Datalogcv matches the complexity of WS1S and WS2S decision
procedures and thus it seems like an appropriate tool for this task. Our ap-
proach is based on representing automata using nested relations and on defining
the necessary operations on automata as Datalogcv queries. Of particular in-
terest is the fact that the final (non-)emptiness check reduces to posing a (s-t)
connectivity query on a nested relational view of the final automaton and can be
achieved, e.g., by computing the transitive closure of the representation of the
transition relation. This observation allows us to use the Magic Set rewriting to
limit the explored state space to elements needed to show non-emptiness.
We have also conducted experiments with CORAL—a Datalogcv sys-
tem [25]—that show the benefits of the proposed method over more common
approaches such as those used by the MONA tool; note that our approach
has often outperformed MONA despite the fact that we have used only a naive
representation of automata in nested relations. The use of BDDs and other com-
pression techniques seems to be orthogonal to our method and should widen the
performance advantage even more1 .
The remainder of the paper is organized as follows. In Section 2, the con-
nection between second order logics and automata is reviewed. Datalogcv and
the representation and querying on automata using Datalogcv is outlined in Sec-
tion 3. In Section 4, the experimental results for the proposed methods are
presented. Related work is discussed in Section 5. Finally, conclusions and
future research directions are given in Section 6.
2 Logic-Automata Connection
Computational properties of automata provide solutions to many problems. One
of these problems is building decision procedures for various logics. In this
section we outline the connection between automata and monadic second order
logics and focus on constructing automata from formulas. The logic-automaton
connection can be generalized to build decision procedures for different logics
such as second order logics with one or two successors (S1S or S2S). Automata
that accept infinite regular languages can be used for this purpose.
2.1 Formulae of Monadic Second Order Logics
We define the formulas of second order logics as follows.
• The expressions x = y, x = s(y), x ∈ X are atomic formulas, where x,
1
This, of course, can work only for certain class of problems as we are faced with the
non-elementary lower bound in general.
y are individual variables, s is the successor function, and X,Y are set
variables.
• Given formulas ϕ and φ, the expressions ϕ ∧ φ, ϕ ∨ φ, ϕ ⇒ φ, ¬ϕ, ∃x : ϕ,
∀x : ϕ, ∃X : ϕ, ∀X : ϕ are also formulas. where x is an individual variable
and X is a set variable.
• No other terms are formulas.
The semantics of WS1S is defined on a line; first-order variables are interpreted
as natural numbers, and second order variables are interpreted as finite sets of
natural numbers. Similarly, the semantics of WS2S is defined over an infinite
binary tree (0 + 1)∗ = {ǫ, 0, 1, 00, 01, 10, 11, 000, ...}; first-order variables are
interpreted as nodes of the binary tree, and second order variables are interpreted
as finite subsets of the nodes. Truth and satisfiability of formulas is defined in
the standard way.
2.2 From Formulae to Automata
It is well known that satisfiability of second order logics, e.g., WS1S and WS2S,
can be determined using finite automata. The crux of these techniques lies
in constructing a finite automaton that accepts exactly the models of a given
formula [27]. This technique has been used for showing decidability and for
providing tight complexity bounds for many logics. In the case of the above two
logics, the automaton is a nondeterministic finite automaton with a finite (or
Büchi [6], Rabin [22], etc.) acceptance condition.
In this paper we explore three automata models: finite word automaton, top-
down tree automaton, and bottom-up tree automaton. Finite word automaton
is the automaton representation of WS1S; and top-down and bottom-up tree
automata are models for WS2S. Bottom-up tree automata start their compu-
tation at the leaves of the input tree, and top-down tree automata at the root
of the input tree in an initial state and then work down the tree level by level
simultaneously.
Definition 1 A finite automaton is a 5-tuple A = (NA , XA , SA , TA , FA ), where
NA is the set of states (nodes), XA is the alphabet, SA is the initial (starting)
state, TA is the transition function, and FA is the set of final states; where TA
⊆ NA × XA × NA for finite word automata, TA ⊆ NA × XA × NA × NA for
top-down tree automata, and TA ⊆ NA × NA × XA × NA for bottom-up tree
automata.
The automaton is constructed from a given formula inductively. It is well known
how to construct automata for the formulas [12, 16]; for example the automaton
for the formula x ∈ X is shown in the left part of Figure 1. Automata rep-
resenting complex formulas are constructed from simpler ones using automata-
theoretic operations.
0 1 0 1 0 1 0 1
0 , 0 0 , 0 0 , 0 0 , 0
1 1
1 1
0 1 0 1
Figure 1: Automata representing the formulae x ∈ X and ¬(x ∈ X).
Lemma 1 Given automata Aϕ and Aφ representing ϕ and φ, respectively, we
can effectively construct an automaton for ϕ ∧ φ, ϕ ∨ φ, ϕ ⇒ φ, ¬ϕ, ∃x : ϕ,
∀x : ϕ, ∃X : ϕ, ∀X : ϕ.
For example, Aϕ ⊕ Aφ , union automaton of A1 and Aφ , accepts L(Aϕ ) ∪ L(Aφ )
and represents ϕ∨φ. The automaton Aϕ ×Aφ , product automaton of Aϕ and Aϕ ,
accepts L(Aϕ ) ∩ L(Aφ ) and represents ϕ ∧ φ. The automaton Acϕ , complement
automaton of Aϕ , accepts the complement of L(Aϕ ) and represents ¬ϕ. Finally,
the automaton Ap1 , projection automaton of Aϕ , represents ∃X : ϕ. Intuitively,
the automaton Apϕ acts as the automaton Aϕ for ϕ except that it is allowed to
guess the bits on the track of X.
Example 1 Let A1 be an automaton representing the formula x ∈ X. Then
the complement automaton Ac1 represents ¬(x ∈ X) which is shown in the right
part of Figure 1.
We give the actual algorithms for constructing the automata in the following
section and in Appendix A (in a Datalogcv syntax).
3 Automata and Datalog for Complex Values
Datalogcv is an extension of Datalog—a language of Horn clauses with variables
ranging over constants—with a limited ability to construct terms in the form
of tuples and finite sets. To retain termination of query evaluation, the use of
terms is restricted in recursive clauses [2, 25]. Datalogcv is equivalent to the
complex value algebra and calculus in expressive power [1]. Datalogcv programs
and queries are defined as follows:
Definition 2 A Datalogcv terms ti are formed from constants, variables and
the tuple ([t1 , . . . , tk ]), set ({t1 , . . . , tk }), and grouping (< t1 >) constructors.
A Datalogcv atom is a predicate symbol applied to an appropriate number of
Datalogcv terms. A Datalogcv program P is a finite set of Horn clauses of
the form h ← g1 , . . . , gk , where h (called head) and g1 , . . . , gk (called goals)
are atoms. The use of the constructors has to be stratified with respect to the
program. A Datalogcv query is a clause of the form ← g1 , . . . , gk . Evaluation of
a Datalogcv query (with respect to P ) determines whether P |= (g1 , . . . , gk )θ for
some ground substitution θ.
The evaluation is commonly based on constructing the minimal Herbrand model
of P and then determining for which substitutions θ is the query is contained in
the model. Furthermore, the extended semi-naive and magic-set techniques can
be used to evaluate our queries like the ones proposed in [18] for Relationlog.
The main advantage of using Datalogcv is its natural use of fixpoint which al-
lows us to express transitive closure (without the use of an additional power-set
operator). Hence, if we transform the automaton and the query representing the
satisfiability of a formula to a logic program we can make use of these efficient
evaluation techniques.
3.1 Representation of Automata
In this section, we provide a general representation for finite automata.
Definition 3 The following program PA represents the automaton A = (NA ,
XA , SA , TA , FA ):
1. NodeA (n) ← (for n ∈ NA ),
2. StartA (n) ← (for n ∈ SA ),
3. F inalA (n) ← (for n ∈ FA ),
4. (a) Automaton for WS1S:
T ransitionA (nf1 , nt1 , x) ← (for (nf1 , x, nt1 ) ∈ TA )
(b) Top-down tree automaton for WS2S:
T ransitionA (nf1 , nt1 , nt2 , x) ← (for (nf1 , x, nt1 , nt2 ) ∈ TA )
(c) Bottom-up tree automaton for WS2S:
T ransitionA (nf1 , nf2 , nt1 , x) ← (for (nf1 , nf2 , x, nt1 ) ∈ TA )
We have x = {x1 , x2 , . . . , xk } ⊆ XA , where each xi (for 1 ≤ i ≤ k) represents
an element (a letter) of XA .
Free variables of the formula represented by A are x1 , x2 , . . . , xk .
Example 2 The following program PA represents the automaton A shown in
the left part of Figure 1:
NodeA (0) ← T ransitionA (0, 0, 0, 0) ←
NodeA (1) ← T ransitionA (0, 0, 1, 0) ←
T ransitionA (0, 1, 1, 1) ←
StartA (0) ←
T ransitionA (1, 1, 0, 0) ←
F inalA (1) ← T ransitionA (1, 1, 1, 0) ←
3.2 Operations on Automata
We define the appropriate automata-theoretic operations: negation, conjunc-
tion, projection, and determinization used in decision procedures for the logics
under consideration as programs in Datalogcv as follows. Negation is defined in
Definition 4, and conjunction, projection, determinization, and transitive closure
of the transition function of an automaton are given in Appendix A.
Definition 4 The following program P¬A represents the complement automaton
Ac of A = (NA , XA , SA , TA , FA ):
1. Node¬A (n) ← NodeA (n)
2. Start¬A (n) ← StartA (n)
3. F inal¬A (n) ← NodeA (n), ¬F inalA (n)
4. (a) Automaton for WS1S:
T ransition¬A (nf1 , nt1 , x) ← T ransitionA (nf1 , nt1 , x)
(b) Top-down tree automaton for WS2S:
T ransition¬A (nf1 , nt1 , nt2 , x) ← T ransitionA (nf1 , nt1 , nt2 , x)
(c) Bottom-up tree automaton for WS2S:
T ransition¬A (nf1 , nf2 , nt1 , x) ← T ransitionA (nf1 , nf2 , nt1 , x)
Lemma 2 If A represents α then Ac represents ¬α.
Similar queries can be used to represent the remaining operations on automata
including the final (non-)emptiness test. Thus we can construct an automaton
Aα corresponding to α(θ1 , θ2 , . . . , θn ), where θ1 , θ2 , . . . , θn are the atomic formu-
las in α, inductively, starting from the atomic formulas and applying the rules
given for each operation in Appendix A.
Theorem 1 Let ϕ be a WS1S (WS2S) formula. Then ϕ is satisfiable if and
only if T ransClosAϕ contains a pair consisting of the start and final states.
Example 3 Suppose that our formula is φ = (∃Y : Y ⊆ X), let A be the
automaton for the subformula Y ⊆ X, we can use the following logic program
to construct the automaton for φ:
Node∃A (n) ← NodeA (n)
Start∃A (n) ← StartA (n)
F inal∃A (n) ← F inalA (n)
T ransition∃A (n1 , n2 , X) ← T ransitionA (n1 , n2 , X, Y )
The above clauses define a non-deterministic automaton (∃A) representing the
formula (see Definition 6).
NodeD∃A ({}) ←
SNodeD∃A ({n}) ← Node∃A (n)
NodeD∃A (N) ← SNodeD∃A (N1 ), NodeD∃A (N2 ), Union(N1 , N2 , N)
StartD∃A ({n}) ← Start∃A (n)
F inalD∃A (N) ← NodeD∃A (N), F inal∃A (n), member(n, N)
T ransitionD∃A (N1 , < n2 >, X) ← T ransition∃A (n1 , n2 , X),
NodeD∃A (N1 ), member(n1 , N1 )
T ranClosD∃A (n1 , n2 ) ← T ransitionD∃A (n1 , n2 , X)
T ranClosD∃A (n1 , n2 ) ← T ransitionD∃A (n1 , n3 , X), T ranClosD∃A (n3 , n2 )
The remaining clauses convert the automaton to a deterministic automaton
(D∃A ) representing the formula (see Definition 7), and compute the transitive
closure of its transition function (see Definition 8) in order to test for non empti-
ness. The final query thus is:
← StartD∃A (N), F inalD∃A (M), T ranClosD∃A (N, M).
Magic-set rewriting [3, 20]—a well known query optimization method—is ap-
plied to the above program prior to query evaluation. The Magic-set technique
improves the bottom-up evaluation such that its performance rivals the efficiency
of the top-down evaluation. The idea behind the magic-set technique lies in re-
stricting the computation of intermediate results to those facts that are needed
to answer a query.
The left part of Figure 2 illustrates the bottom-up evaluation of the program
given in Example 3, the right part illustrates the magic-set evaluation of the
same program. The effect of the Magic set-based query evaluation is even more
Node: {0} {1} { 0 ,1 }
0 X
Node: {0} { 0 ,1 }
Transition:
{0} 1
{ 0 ,1 }
X 0 X
Transition:
{1} {0} 1
{ 0 ,1 }
TranClos: {0} {0}
{0} { 0 ,1 } TranClos: {0} {0}
{1} {1} {0} { 0 ,1 }
{ 0 ,1 } { 0 ,1 } { 0 ,1 } { 0 ,1 }
Figure 2: Bottom-up and Magic Set evaluation of the program in Example 3.
pronounced for larger formulas. For example, for the formula
φ = (x ∈ X) ∧ (∃Y : (y ∈ Y ) ∧ (z ∈ Y ))
the bottom-up evaluation creates 1536 nodes, 24528 transitions while the magic-
set evaluation technique creates only 2 nodes and 1 transition.
4 Experiments
We compare our technique with the MONA system [12, 16], one of the most
efficient tools for reasoning of weak second order logics (WS1S and WS2S). In
contrast to MONA which constructs the whole automaton for a given formula
our method only constructs the nodes we need to answer the non emptiness
query. For the experiments we use CORAL, a deductive system that supports
Datalogcv and Magic sets.
The performance results are given in Figure 3. The response times are mea-
sured in seconds; N/A means “Not Answered”. The formulas are similar to
the ones in T98 satisfiability test suite except we varied their sizes, in particu-
lar the number of existential quantifiers and free variables. We have observed
that the magic-set evaluation method exhibits a considerable performance gain
over MONA for formulas with many free variables. On the other hand, MONA
usually performs better than CORAL for the formulas with many existential
quantifiers. We believe that this is a problem caused by the implementation
CORAL uses for the evaluation of programs with sets (and can be avoided using
a more sophisticated implementation of Datalogcv ). In addition MONA uses the
BDD data structures and algorithms to enhance its performance. Our current
implementation in CORAL does not support these structures and is likely to
perform better using them.
1 2 3 4 5 6 7 8 9 10
MONA N/A N/A 7.08 7.14 5.22 4.37 13.33 N/A 10.80 N/A
CORAL 4.15 5.22 4.76 11.94 3.95 2.42 4.75 16.25 3.78 12.09
Figure 3: Performance results (secs)
We also began exploring the impact of goal reordering on the performance of
the Datalogcv program representations of the automata. The following example
illustrates the importance of technique:
Example 4 We show three rewritings of a formula and their performance re-
sults. Consider the following formulas:
ϕ1 = (x11 ∈ Y11 ) ⇐⇒ (x12 ∈ Y12 )
ϕ2 = (∃Y13 : (x13 ∈ Y13 ) ∧ (x14 ∈ Y13 )
ϕ3 = (((x1 ∈ Y1 ) ⇐⇒ (x2 ∈ Y2 )) ⇒ ((x3 ∈ Y3 ) ⇐⇒ (x4 ∈ Y4 ))) ∧
(((x5 ∈ Y5 ) ⇐⇒ (x6 ∈ Y6 )) ⇒ ((x7 ∈ Y7 ) ⇐⇒ (x8 ∈ Y8 ))) ∧
((x9 ∈ Y9 ) ⇐⇒ (x10 ∈ Y10 ))
Then the goal ordering results in the following timing which shows that the min-
imal response time we get using CORAL is 16.34 seconds, MONA fails in all
three cases.
ϕ1 ∧ ϕ2 ∧ ϕ3 ϕ3 ∧ ϕ1 ∧ ϕ2 ϕ3 ∧ ϕ2 ∧ ϕ1
MONA N/A N/A N/A
CORAL N/A 16.34 31.19
Figure 4: Performance results (secs)
5 Related Work
The connection between logic and automata was first considered by Büchi [6]
and Elgot [10]. They have shown that monadic second-order logic over finite
words and finite automata have the same expressive power, and we can trans-
form formulas of this logic to finite automata and vice versa. Later, Büchi [7],
McNaughton [19], and Rabin [22] proved that monadic second-order logic over
infinite words (and trees) and finite automata also have the same expressive
power. The practical use of this connection was investigated for temporal logics
and fixed-point logics which led to the theory of model checking [4, 29]. An-
other automata theoretic construction used in specification and verification was
for µ-calculus [14] and description logics [30]. An extensive survey on automata
and logic can be found in [27].
The logic-automaton connection has been used for implementing decision
procedures for various logics. It is argued that the success of these procedures
relies on efficient operations on a compact representation of automata based on
BDDs [16, 17].
We have used deductive techniques to represent and query automata. The
system used to support our implementation, CORAL [23, 24, 25], provides effi-
cient set-oriented data manipulation common in relational systems. There are
numerous other deductive systems which support logic-programming languages
with sets and tuples, e.g., LDL [9, 21], and XSB [26] (here sets have to be
explicitly simulated). In terms of the evaluation strategy XSB uses top-down
evaluation with memoing whereas CORAL uses magic sets.
Considerable work has been done on query optimization in relational and
deductive database systems [20]. Query optimization in relational systems in-
cludes choosing join orders and cost models [8, 28]. We use the idea of magic
sets rewriting [3] as a deductive database optimization method for our queries,
and we are planning to use cost-based optimization methods to improve our
query evaluation.
6 Conclusions and Future Work
In this paper we have presented a translation technique that maps satisfiability
questions for formulas in WS1S and WS2S and, in turn, implication problems
in ALC to query evaluation in Datalogcv . The connection was made using the
link between logic and finite automata. We have shown how the evaluation tech-
niques used for answering queries over these programs provide efficient decision
procedures for second order logics.
Future extensions of the proposed approach include extending the translation
to other types of automata on infinite objects, e.g., to Rabin [22] and Alternating
Automata [30], and on improving the upper complexity bounds by restricting
the form of Datalogcv programs generated by the translation (when used for
decision problems in, e.g., EXPTIME). In all these cases, the goal is to match
the optimal theoretical bounds while avoiding the worst-case behavior (inherent
in most automata-based techniques) in as many situations as possible. In ad-
dition we plan to study the impact of goal reordering and various other query
optimization techniques on the performance of the decision procedure and to
develop heuristics (patterned on cost-based join-order and query optimization)
for this purpose. We also plan to compare the CORAL-based implementations
with implementations based on the XSB system, a logic programming system
with memoing [26].
References
[1] S. Abiteoul, C. Beeri, “The Power of Languages for the Manipulation of Complex
Values”, VLDB Journal, Vol. 4, No. 4, pp. 727-794, 1995.
[2] C. Beeri, S. Naqvi, O. Shmueli, S. Tsur, “Set Construction in a Logic Database
Language”, Journal of Logic Programming, Vol. 10, No. 3&4, pp. 181-232, 1991.
[3] C. Beeri, R. Ramakrishnan, “On the Power of Magic”, Journal of Logic Program-
ming, Vol. 10, Nos. 1–4, pp. 255-299, 1991.
[4] O. Bernholtz, M. Y. Vardi, P. Wolper, “An Automata-theoretic Approach to
Branching-time Model Checking”, Computer Aided Verification, Proc. 6th Int.
Workshop, pp. 142-155, 1994.
[5] R. E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary Decision
Diagrams”, ACM Computing Surveys, Vol. 24, No. 3, pp. 293-318, 1992.
[6] J. R. Büchi, “Weak Second-order Arithmetic and Finite Automata”, Z. Math.
Logik Grundl. Math., Vol. 6, pp. 66-92, 1960.
[7] J. R. Büchi, “On a Decision Method in Restricted Second-order Arithmetic”,
Proc. 1960 Int. Congr. for Logic, Methodology and Philosophy of Science, pp. 1-
11, 1962.
[8] S. Chaudhuri, “An Overview of Query Optimization in Relational Systems”,
PODS, pp. 34-43, 1998.
[9] D. Chimenti, R. Gamboa, R. Krishnamurthy, S. A. Naqvi, S. Tsur, C. Zaniolo,
“The LDL System Prototype”, IEEE Trans. Knowl. Data Eng., Vol. 2, No. 1,
pp. 76-90, 1990.
[10] C. C. Elgot, “Decision Problems of Finite Automata Design and Related Arith-
metics”, Trans. Amer. Math. Soc., Vol. 98, pp. 21-52, 1961.
[11] V. Haarslev, R. Möller, “High performance reasoning with very large knowledge
bases: A practical case study”, IJCAI, pp. 161-166, 2001.
[12] J. G. Henriksen, J. L. Jensen, M. E. Jörgensen, N. Klarlund, R. Paige, T. Rauhe,
A. Sandholm, “Mona: Monadic Second-Order Logic in Practice”, TACAS, pp. 89-
110, 1995.
[13] I. Horrocks, “Using an expressive description logic: FaCT or fiction?”, Knowledge
Representation and Reasoning (KR), pp. 636-647, 1998.
[14] D. Janin, I. Walukiewicz, “Automata for the Modal µ-Calculus and related Re-
sults”, MFCS, pp. 552-562, 1995.
[15] E. Karabaev, C. Lutz, “Mona as a DL Reasoner”, Description Logics, 2004.
[16] N. Klarlund, “Mona & Fido: The Logic-Automaton Connection in Practice”,
Computer Science Logic, pp. 311-326, 1997.
[17] N. Klarlund, A. Møller, M. I. Schwartzbach, “MONA Implementation Secrets”,
Int. J. Found. Comput. Sci., Vol. 13, No. 4, pp. 571-586, 2002.
[18] M. Liu, “Query Processing in Relationlog”, DEXA, pp. 342-351, 1999.
[19] R. McNaughton, “Testing and Generating Infinite Sequences by a Finite Au-
tomaton”, Information and Control, Vol. 9, pp. 521-530, 1966.
[20] I. S. Mumick, “Query Optimization in Deductive and Relational Databases”,
PhD Thesis, Department of Computer Science, Stanford University, 1991.
[21] S. Naqvi, S. Tsur, “A Logical Language for Data and Knowledge Bases”, Com-
puter Science Press, 1989.
[22] M. O. Rabin, “Decidability of Second-order Theories and Automata on Infinite
Trees”, Trans. Amer. Math. Soc., Vol. 141, pp. 1-35, 1969.
[23] R. Ramakrishnan, P. Bothner, D. Srivastava, S. Sudarshan, “CORAL–A
Database Programming Language”, Workshop on Deductive Databases, 1990.
[24] R. Ramakrishnan, D. Srivastava, S. Sudarshan, “CORAL–Control, Relations and
Logic”, VLDB Journal, pp. 238-250, 1992.
[25] R. Ramakrishnan, D. Srivastava, S. Sudarshan, P. Seshadri, “The CORAL De-
ductive System”, VLDB Journal, Vol. 3, No. 2, pp. 161-210, 1994.
[26] K. F. Sagonas, T. Swift, D. S. Warren, “XSB as an Efficient Deductive Database
Engine”, SIGMOD Conference, pp. 442-453, 1994.
[27] W. Thomas, “Languages, Automata, and Logic”, Handbook of Formal Languages,
Vol. 3, 1997.
[28] J. D. Ullman, “Principles of Database and Knowledge-Base Systems”, Computer
Science Press, Vol. 1&2, 1989.
[29] M. Y. Vardi, P. Wolper, “An Automata-theoretic Approach to Automatic Pro-
gram Verification”, Proc. of the First Symposium on Logic in Computer Science,
pp. 322-331, 1986.
[30] M. Y. Vardi, “Reasoning about The Past with Two-Way Automata”, ICALP,
pp. 628-641, 1998.
A Appendix
In this section, we define conjunction, projection, determinization, and transitive clo-
sure of the transition function of an automaton. Conjuction operation is provided in
Definition 5, projection in Definition 6, determinization in Definition 7, and finally
transitive clossure of the transition function is given in Definition 8.
Definition 5 The following program PA1 ∧A2 represents the product automaton A1 ×
A2 of A1 = (NA1 , XA1 , SA1 , TA1 , FA1 ), and A2 = (NA2 , XA2 , SA2 , TA2 , FA2 ):
1. N odeA1 ∧A2 ([n1 , n2 ]) ← N odeA1 (n1 ), N odeA2 (n2 )
2. StartA1 ∧A2 ([n1 , n2 ]) ← StartA1 (n1 ), StartA2 (n2 )
3. F inalA1 ∧A2 ([n1 , n2 ]) ← F inalA1 (n1 ), F inalA2 (n2 )
4. (a) Automaton for WS1S:
T ransitionA1∧A2 ([nf11 , nf21 ], [nt11 , nt21 ], x, y, z) ←
T ransitionA1 (nf11 , nt11 , x, y), T ransitionA2 (nf21 , nt21 , y, z)
(b) Top-down tree automaton for WS2S:
T ransitionA1∧A2 ([nf11 , nf21 ], [nt11 , nt21 ], [nt12 , nt22 ], x, y, z) ←
T ransitionA1 (nf11 , nt11 , nt12 , x, y),
T ransitionA2 (nf21 , nt21 , nt22 , y, z)
(c) Bottom-up tree automaton for WS2S:
T ransitionA1∧A2 ([nf11 , nf21 ], [nf12 , nf22 ], [nt11 , nt21 ], x, y, z) ←
T ransitionA1 (nf11 , nf12 , nt11 , x, y),
T ransitionA2 (nf21 , nf22 , nt21 , y, z)
Here, x, y represent the free variables of the formula A1 represents, and y, z of the
formula A2 represents.
Lemma 3 If A1 represents α1 , and A2 represents α2 then, A1 ×A2 represents α1 ∧α2 .
Definition 6 The following program P∃A represents the projection automaton Ap of
A = (NA , XA , SA , TA , FA ):
1. N ode∃A (n) ← N odeA (n)
2. Start∃A (n) ← StartA (n)
3. F inal∃A (n) ← F inalA (n)
4. (a) Automaton for WS1S:
T ransition∃A (nf1 , nt1 , y) ← T ransitionA (nf1 , nt1 , x, y)
(b) Top-down tree automaton for WS2S:
T ransition∃A (nf1 , nt1 , nt2 , y) ← T ransitionA(nf1 , nt1 , nt2 , x, y)
(c) Bottom-up tree automaton for WS2S:
T ransition∃A (nf1 , nf2 , nt1 , y) ← T ransitionA (nf1 , nf2 , nt1 , x, y)
5. (a) Automaton for WS1S:
i. T ransitionX (nf1 , nt1 , x, o) ← T ransitionA(nf1 , nt1 , x, y)
ii. F inal∃A (n) ← N odeA (n), T ransitionX (nf1 , nt1 , x, y), F inalA (nt1 ),
T ransitionA (n, nt2 , x, y), F inalA (nt2 )
(b) Top-down tree automaton for WS2S:
i. T ransitionX (nf1 , nt1 , nt2 , x, o) ← T ransitionA (nf1 , nt1 , nt2 , x, y)
ii. F inal∃A (n) ← N odeA (n),
T ransitionX (nf1 , nt1 , nt2 , x, y), F inalA (nt1 ), F inalA (nt2 ),
T ransitionA (n, nt3 , nt4 , x, y), F inalA (nt3 ), F inalA (nt4 )
(c) Bottom-up tree automaton for WS2S:
i. T ransitionX (nf1 , nf2 , nt1 , x, o) ← T ransitionA(nf1 , nf2 , nt1 , x, y)
ii. F inal∃A (n) ← N odeA (n), T ransitionX (nf1 , nf2 , nt1 , x, y),
F inalA (nt1 ), T ransitionA(n, nf3 , nt2 , x, y), F inalA (nt2 )
iii. F inal∃A (n) ← N odeA (n), T ransitionX (nf1 , nf2 , nt1 , x, y),
F inalA (nt1 ), T ransitionA(nf3 , n, nt2 , x, y), F inalA (nt2 )
Here, o = {0, 0, . . . , 0} where |o| = |y|, y represents free variables, and x represents
bound variables of the formula represented by A.
Lemma 4 If A represents α then Ap represents ∃x1 , x2 , . . . , xk : α where Ap is the
projection automaton of A.
Definition 7 The following program PDA represents the determinized automaton Ad
of A = (NA , XA , SA , TA , FA ):
1. (a) N odeDA ({}) ←
(b) SN odeDA ({n}) ← N odeA (n)
(c) N odeDA (N ) ← SN odeDA (N1 ), N odeDA (N2 ), U nion(N1 , N2 , N )
2. StartDA ({n}) ← StartA (n)
3. F inalDA (N ) ← N odeDA (N ), F inalA (n), member(n, N )
4. (a) Automaton for WS1S:
T ransitionDA (N f1 , < nt1 >, x) ← T ransitionA (nf1 , nt1 , x),
N odeDA (N f1 ), member(nf1 , N f1 )
(b) Top-down tree automaton for WS2S:
T ransitionDA (N f1 , < nt1 >, < nt2 >, x) ← T ransitionA(nf1 , nt1 , nt2 , x),
N odeDA (N f1 ), member(nf1 , N f1 )
(c) Bottom-up tree automaton for WS2S:
T ransitionDA (N f1 , N f2 , < nt1 >, x) ← T ransitionA (nf1 , nf2 , nt1 , x),
N odeDA (N f1 ), member(nf1 , N f1 ),
N odeDA (N f2 ), member(nf2 , N f2 )
The function U nion(N1 , N2 , N ) takes two sets N1 and N2 as inputs and assigns their
union to N , member(n, N ) checks if n is a member of the set N or not.
Lemma 5 If A represents α then Ad represents α, and Ad is the determinized A.
Definition 8 The following program PT CA computes the transitive closure of the tran-
sition function of A to find out if the language A represents is non-empty or not, and
as a result, if α, which is the formula represented by A, is satisfiable or not.
1. Automaton for WS1S:
(a) T ranClosA(nf1 , nt1 ) ← T ransitionA (nf1 , nt1 , x)
(b) T ranClosA(nf1 , nt1 ) ←
T ransitionA(nf1 , nt2 , x), T ranClosA(nt2 , nt1 )
2. Top-down tree automaton for WS2S:
(a) T ranClosA(nf1 , nt1 , nt2 ) ← T ransitionA(nf1 , nt1 , nt2 , x)
(b) T ranClosA(nf1 , nt1 , nt2 ) ←
T ransitionA(nf1 , nt3 , nt4 , x), T ranClosA(nt3 , nt1 , nt2 )
(c) T ranClosA(nf1 , nt1 , nt2 ) ←
T ransitionA(nf1 , nt3 , nt4 , x), T ranClosA(nt4 , nt1 , nt2 )
3. Bottom-up tree automaton for WS2S:
(a) T ranClosA(nf1 , nf2 , nt1 ) ←
T ransitionA(nf1 , nf2 , nt1 , x)
(b) T ranClosA(nf1 , nf2 , nt1 ) ←
T ransitionA(nf1 , nf2 , nt2 , x), T ranClosA(nt2 , nf3 , nt1 )
(c) T ranClosA(nf1 , nf2 , nt1 ) ← T ransitionA (nf1 , nf2 , nt2 , x),
T ranClosA(nf3 , nt2 , nt1 )