In this paper we propose to use techniques developed for query evaluation of Complex-value Datalog queries for determining satisfiability of WS1S and WS2S formulae. This in turn can serve as a decision procedure 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.
Recently, WS1S and WS2S reasoners have been employed as reasoners for description 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 techniques have run into serious state-space explosion problem-the size of a automaton 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 between automata-based decision procedures for WS1S and WS2S and query evaluation in Complex-value Datalog (Datalog cv ). Indeed, the complexity of query evaluation in Datalog cv matches the complexity of WS1S and WS2S decision procedures and thus it seems like an appropriate tool for this task. Our approach is based on representing automata using nested relations and on defining the necessary operations on automata as Datalog cv queries. Of particular interest 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 Datalog cv system [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 compression techniques seems to be orthogonal to our method and should widen the performance advantage even more 1 .
The remainder of the paper is organized as follows. In Section 2, the connection between second order logics and automata is reviewed. Datalog cv and the representation and querying on automata using Datalog cv is outlined in Section 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.
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.
We define the formulas of second order logics as follows.
• The expressions x = y, x = s(y), x ∈ X are atomic formulas, where x, 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.
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, topdown 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 computation 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.
, where N A is the set of states (nodes), X A is the alphabet, S A is the initial (starting) state, T A is the transition function, and F A is the set of final states; where
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 representing complex formulas are constructed from simpler ones using automatatheoretic operations.
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 : ϕ.
and represents ϕ∨φ. The automaton A ϕ ×A φ , product automaton of A ϕ and A ϕ , accepts L(A ϕ ) ∩ L(A φ ) and represents ϕ ∧ φ. The automaton A c ϕ , complement automaton of A ϕ , accepts the complement of L(A ϕ ) and represents ¬ϕ. Finally, the automaton A p 1 , projection automaton of A ϕ , represents ∃X : ϕ. Intuitively, the automaton A p ϕ acts as the automaton A ϕ for ϕ except that it is allowed to guess the bits on the track of X.
Example 1 Let A 1 be an automaton representing the formula x ∈ X. Then the complement automaton A c 1 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 Datalog cv syntax).
Datalog cv 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]. Datalog cv is equivalent to the complex value algebra and calculus in expressive power [1]. Datalog cv programs and queries are defined as follows:
Definition 2 A Datalog cv terms t i are formed from constants, variables and the tuple ([t 1 , . . . , t k ]), set ({t 1 , . . . , t k }), and grouping (< t 1 >) constructors. A Datalog cv atom is a predicate symbol applied to an appropriate number of Datalog cv terms. A Datalog cv program P is a finite set of Horn clauses of the form h ← g 1 , . . . , g k , where h (called head) and g 1 , . . . , g k (called goals) are atoms. The use of the constructors has to be stratified with respect to the program. A Datalog cv query is a clause of the form ← g 1 , . . . , g k . Evaluation of a Datalog cv query (with respect to P ) determines whether P |= (g 1 , . . . , g k )θ 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 Datalog cv is its natural use of fixpoint which allows 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.
In this section, we provide a general representation for finite automata.
Top-down tree automaton for WS2S:
T ransition A (nf 1 , nt 1 , nt 2 , x) ← (for (nf 1 , x, nt 1 , nt 2 ) ∈ T A ) (c) Bottom-up tree automaton for WS2S:
We have x = {x 1 , x 2 , . . . , x k } ⊆ X A , where each x i (for
Free variables of the formula represented by A are x 1 , x 2 , . . . , x k .
The following program P A represents the automaton A shown in the left part of Figure 1:
We define the appropriate automata-theoretic operations: negation, conjunction, projection, and determinization used in decision procedures for the logics under consideration as programs in Datalog cv 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.
The following program P ¬A represents the complement automaton
) Top-down tree automaton for WS2S:
) Bottom-up tree automaton for WS2S:
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 formulas 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 ransClos Aϕ 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 φ:
The above clauses define a non-deterministic automaton (∃A) representing the formula (see Definition 6).
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 emptiness. The final query thus is:
Magic-set rewriting [3,20]-a well known query optimization method-is applied 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 restricting 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 pronounced for larger formulas. For example, for the formula
the bottom-up evaluation creates 1536 nodes, 24528 transitions while the magicset evaluation technique creates only 2 nodes and 1 transition.
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 Datalog cv and Magic sets.
The performance results are given in Figure 3. The response times are measured 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 particular 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 Datalog cv ). 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. We also began exploring the impact of goal reordering on the performance of the Datalog cv 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 results. Consider the following formulas:
Then the goal ordering results in the following timing which shows that the minimal response time we get using CORAL is 16.34 seconds, MONA fails in all three cases.
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 transform 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]. Another 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 efficient 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 includes 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.
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 Datalog cv . The connection was made using the link between logic and finite automata. We have shown how the evaluation techniques 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 Datalog cv 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 addition 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].
In this section, we define conjunction, projection, determinization, and transitive closure 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.