BTL Prover Experiments

Test Cases
Performance Result
Syntax
Ocaml interface to Buddy BDD library

This directory contains testcases used in the experiment described in the following paper.

A.Tozawa and M. Hagiya, Efficient Decision Procedure for a Logic for XML

In the paper, we described the satsifiability test algorithm for the binary tree logic (BTL). We performed an experiment of this algorithm on several BTL formulas including those from XSLT typechecking testcases. We also compared the performance of our algorithm with WS2S prover MONA.

Test Cases

Performance Result

The test environment is Linux, Pentium M 1.8GHz with 1GB memory. SAT is outputs of each prover whether or not the formula is satisfiable. Initialization for BTL prover is parse time and preparation of BDD relations, which includes time to find ordering for conjunctive partitioning of relation products. Initialization for MONA includes parse-time and DAG-reduction. We initially set Buddy's node and operator caches to 3,000,000. GC and AVR are numbers of garbage collection and automatic variable reordering performed by Buddy. In MONA, all formulas are localized, i.e., 2^nd order quantifications are put inside whenever possible. Note that numbers are different from the earlier report, since we have improved our BTL prover in several ways, e.g., using Buddy, improved formula simplification, etc.

(* : GC and AVR occur during initialization, ** : using a certain initial variable ordering heuristics)

Discussion: In experiments, BTL prover generally performs better, except for dept_weak which requires μ-loop detection. To solve dept_weak example, BTL prover needs a new optimization technique (representing dependency by total order) and we have to probe initial variable ordering (without which AVR is triggered). However MONA still performs better in loop detection. MONA computes deterministic automata for each fragment of formula, and loop-detection is done by negation, while our algorithm just enumerates states of non-deterministic automata and requires additional analysis for loops. Also note that it is essential to localize formulas for MONA, i.e., we insert as many let-clauses as possible. MONA can exploit locality in formulas, since 2^nd-order variables are quantified earlier. BTL prover, on the other hand, does not affected by localization, except for in the case of dept_weak, in which each local let-clauses can use let-ν since they do not contain interleaves of upward and downward modal operators.

Syntax

BTL uses the following ASCII syntax.

   phi ::= p
         | ~p
         | [m]phi
         | phi & phi
         | phi | phi
         | $x
         | let_{mu,nu} $x := phi, ... $x = phi in phi end

We use ~p for negation of p. We also use <m> meaning that the node has m-th successor. Other ascii strings represent XML names. For the semantic of BTL, please refer to the paper.

Regular Expression Type t specifies the grammar of XML documents. Its syntax is as follows.

  t ::= ()
      | t, t
      | t | t
      | t* 
      | element a { t }
      | X

The following is an example of a schema. This is a schema for preface documents.

LET
  Div = element div { Div.content }
  Div.content = (Div | P | Note)*
  Doc = element doc { Preface, Div.content }
  Header = element header { empty }
  Note = element note { P* }
  P = element p { empty }
  Preface = element preface { Header, P* }
IN
Doc

This means that at top we have Doc, which is an element doc whose content is a sequence of Preface and Div.content, ... and so on. For example, the following is a valid preface document.

    <doc>
      <preface>
        <header/>
        <p/>
      </preface>
      <note>
        <p/>
      </note>
      <div>
        <note>
          <p/>
        </note>
          <p/>
      </div>
    </doc>

Note that <p/> abbreviates <p></p>.

XSLT0 is a tiny XML transformation language which simplifies W3C XSLT. A syntax of XSLT0

  e ::= ()
      | m { e }
      | e, e
      | element a { e }
      | copy { e } 
      | if phi then e else e fi
      | mu X.{ e }
      | X

For example, the following is an example of an XSLT0 program, which is used in the "htmlcopy" and "prefcopy" testcases.

    mu X.{
       copy {1 {X}}, 
       2 {X}}

Let's see how this program transforms the following XML document.

   <a>
     <b></b>
     <c></c>
     <d></d>
   </a>

The evaluation proceeds as follows.

1) The program starts from the root node <a> .. </a>.
2) The "mu X. { ... }" constuct is a fixpoint binder. Here we just skip it.
3) The seqeunce "copy {1 {X}}, 2 {X}" means that we first evaluate "copy {1 {X}}", and then we evaluate "2 {X}".
4) When we evaluate "copy {1 {X}}" on the current node <a> .. </a>, we create a node with its name the same as the current node. Thus we have

  <a> ... </a>

The content of <a> ... </a> should be the result of the evaluation of "1 {X}". The evaluation of "2 {X}" on <a> ... </a>, on the other hand, results in the null sequence since the node has no 2nd successor.
5) When we evaluate "1 {X}" on <a><b></b> .. </a>, we move to the first child node. Hence we evaluate "X" on <b></b>....
6) The evaluation of "X" results in the recursive call. That is, we again evaluate "mu X.{ ... }" on <b></b>...
7) Similarly, we first evaluate "copy {1 {X}}" on <b></b>..., and then evaluate "2 {X}". The first evaluation results in a node <b> ... </b>. When we apply "1 {X}" on <b></b>..., since the node has no 1st successor, the content ... of <b>...</b> is just a null sequence. The result is put into inside <a> ... </a>. So we have

  <a><b></b> ... </a>

8) On the other hand, evaluation of "2 {X}" on <b></b>... sets the current node to the sibling node <c></c>.... We create <c></c> and have:

  <a><b></b><c></c> ... </a>

9) The rest of the evaluation is similar. As a result, the program copies the input tree.

Please refer to the mona manual for the MONA syntax. If you already installed MONA, each program can be simply executed by mona xxx.mona.

Ocaml interface to Buddy BDD library

The implementation language is Ocaml but we internally uses the Buddy BDD library, which is wrapped by the interface buddy_wrapper.c and buddy.ml. This interface links Ocaml-GC with Buddy-GC, so that we do not need to care about removing unnecessary BDD nodes on the Ocaml-side. It is fairly easy to compile (please add bdd.h and Ocaml native interface related headers to your include directory, and pass -cclib -lbdd option to ocamlc). We have tested this both on Linux and windows. Please refer to the manual and examples in the Buddy distribution for the further usage.

Last modified: 11/14/04
Akihiko Tozawa, atozawa@jp.ibm.com