GTRecS (Games and Types for RECursion Schemes) 2: Model Checker and Transformer for Higher-Order Recursion Schemes

This is a Web interface for a new version of a higher-order model checker, extended with a capability to transform recursion schemes to compute the output of a transducer. The underlying model checking algorithm has been newly designed to work well (at least better than the previous model checkers:) for recursion schemes that compactly represent large finite trees. Other implementations of higher-order model checkers ( TRecS, described in Kobayashi's PPDP09 paper and GTrecS, described in Kobayashi's FoSSaCS 11 paper) are available elsewhere.

GTrecS 2 provides the following three features.

Co-Trivial Automata Model Checking
Take a recursion scheme G and a co-trivial automaton A as input, and check whether Tree(G) (the tree generated by G) is accepted by A. A co-trivial automaton is a Buchi tree automaton with a "co-trivial" acceptance condition, which accepts only trees having finite run-trees. Pattern match queries on finite trees can be encoded into this form of model checking: see the examples below.
Transformation of Higher-Order Recursion Scheme
Take a recursion scheme G and a transducer X as input, and output a recursion scheme G' such that Tree(G') = X(Tree(G)). (If X is a non-deterministic transducer, then G' generates one of the outputs of X.) Actually, on this web interface, you can specify a tree transducer only in the form of a (co-trivial) tree automaton. If you write a transition rule:
```
    q a -> q1 q2 q3
```
then, the output action of the transducer for this transition is automatically named as Taq1_q2_q3_q. If you would like the transducer to output b for this transition, for example, you need to add the following rule to the output recursion scheme.
```
    Taq1_q2_q3_q x1 x2 x3 = b x1 x2 x3.
 
```
Trivial Automata Model Checking
Take a recursion scheme G and a trivial automaton A as input, and check whether Tree(G) (the tree generated by G) is accepted by A. This is the same functionality as the one provided by previous higher-order model checkers TRecS and GTrecS.

NOTE: GTRecS2 is not good at DISPROVING a given property. Thus, to decide a property (for which you do not know an answer), in general, you need to prepare two automata, one representing the property and the other representing the NEGATION of the property, and run GTRecS2 for the two automata in parallel. In the examples below, all the automata represent properties satisfied by the recursion schemes (so that you need not negate the properties).

Enter a recursion scheme and a tree automaton in the box below, choose the functionality, and press the "submit" button. Some examples are given below. More examples are available here as a zip file Note that on this web interface, only small examples can be tested (as the time-out is set to 3 seconds). Please contact Naoki Kobayashi if you need source code.

TRecS, another version of type-based model checker, is available here.

Examples

Some examples are given below. (Cut the part from %BEGING to %ENDA and paste it into the box above.)

Example 1 (for query)

Check that 1024th Fibonacci word contains "aa" as a substring.

%BEGING  /*** Rewring rules of a recursion scheme. Non-terminal must start with a capital letter. ***/
/*** The non-terminal of the first rule is interpreted as the start symbol. ***/
/*** Unbounded names ("a", "b" in this rule) are interpreted as terminals. ***/
S = Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice Next))))))))) Fst b a.
Twice f k x y = f (f k) x y.
Next k x y = k y (Concat y x).
Fst x y = x e.
Concat x y c = x(y c).
%ENDG

%BEGINA /*** Transition rules of a Buchi tree automaton. ***/
/* Contains aa? */
q0 a -> q1.  /*** The first state is interpreted as the initial state. **/
q0 b -> q0.
q1 b -> q0.
q1 a -> q2.
q2 a -> q2.
q2 b -> q2.
q2 e -> .
%ENDA

Example 2 (for query)

Check that 1024th Fibonacci word does NOT contain "bb" as a substring.

%BEGING
S = Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice Next))))))))) Fst b a.
Twice f k x y = f (f k) x y.
Next k x y = k y (Concat y x).
Fst x y = x e.
Concat x y c = x(y c).
%ENDG

%BEGINA
/* Contains no aaa? */
q0 a -> q0.
q0 b -> q1.
q1 a -> q0.
q0 e -> .
q1 e -> .
%ENDA

Example 2' (for query)

Check that 1024th Fibonacci word does NOT contain "aaa" as a substring.

%BEGING
S = Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice Next))))))))) Fst b a.
Twice f k x y = f (f k) x y.
Next k x y = k y (Concat y x).
Fst x y = x e.
Concat x y c = x(y c).
%ENDG

%BEGINA
/* Contains no aaa? */
q0 a -> q1.
q0 b -> q0.
q1 b -> q0.
q1 a -> q2.
q2 b -> q0.
q0 e -> .
q1 e -> .
q2 e -> .
%ENDA

Example 3 (for transformation)

Replace every occurence of "ab" in 1024th Fibonacci word with "bb". (NOTE: You need to add the following rules to the output of the transformation:

Taq1_q0 x = x.
Tbq0_q0 x = b(x).
Taq1_q1 x = a(x).
Tbq0_q1 x = b(b(x)).
Teq0 = e.
Teq1 = a(e).

)

%BEGING
S = Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice (Twice Next))))))))) Fst b a.
Twice f k x y = f (f k) x y.
Next k x y = k y (Concat y x).
Fst x y = x e.
Concat x y c = x(y c).
%ENDG

%BEGINA
/* replace ab with bb */
q0 a -> q1. /* epsilon */
q0 b -> q0. /* b */
q1 a -> q1. /* a */
q1 b -> q0. /* bb */
q0 e -> .   /* e */
q1 e -> .   /* a e */
%ENDA

Example 4 (for query)

Check that a DNA sequence (represented by the recursion scheme below) does not contain "acgtac" as a substring.

%BEGING
S =  X119 (X45 (X116 (X80 (X119 (X80 (X64 (X41 (X75 a)) (a (g
(X111 a (c (X75 g (X79 (t (X68 c (X20 (X19 (c (X112 (X44 (X99
c (X66 (g (X89 (g (X20 (X61 (t (X79 (a (X43 (X86 (X24 a (X78
(X105 t (X42 (X95 t (X37 (X78 (g (X112 (a (X85 (X18 (X105 a
(X65 (X117 (X114 (t (X78 (X36 (X35 (X108 a (X33 (t (X30 (X64
c (X92 t (g (X60 (X15 (X102 a (X20 (g (t (X54 (X19 (X88 (g
(X13 (X117 (X48 t (X95 c (X16 (X18 (X65 (X108 c (X42 (t (X77
(X12 (X83 t (g (X43 (g (X37 (X16 (g (g (X36 (c (X43 (a (X77
(X6 (X87 (X60 (X44 (X111 c (X83 c (t (t (X86 (X36 (X15 (X87
(t (X99 a (g (X102 c
e))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
X4 x1 x2 x3 = x1 (x2 x3).
X5 x y = X4 t x y.
X6 x = X5 a x.
X10 x7 x8 x9 = x8 (x7 x9).
X11 x y = X10 t x y.
X12 x = X11 c x.
X13 x = X5 g x.
X14 x y = X10 c x y.
X15 x = X14 g x.
X16 x = X14 a x.
X17 x y =  X4 a x y.
X18 x =  X17 t x.
X19 x =  X17 a x.
X20 x =  X5 c x.
X21 x y =  X4 c x y.
X24 x22 x23 =  g (x22 (x22 x23)).
X28 x25 x26 x27 =  x25 (x26 (x25 x27)).
X29 x y =  X10 X13 x y.
X30 x =  X28 t c x.
X31 x y =  X28 c x y.
X32 x =  X31 c x.
X33 x =  X29 c x.
X34 x y =  X4 X16 x y.
X35 x =  X34 c x.
X36 x =  X29 a x.
X37 x =  X31 a x.
X40 x38 x39 =  x38 (x38 (a x39)).
X41 x y =  X10 X16 x y.
X42 x =  X34 t x.
X43 x =  X41 t x.
X44 x =  X40 t x.
X45 x =  X40 c x.
X48 x46 x47 =  c (x46 (x46 (X6 x47))).
X52 x49 x50 x51 =  x49 (x49 (a (x50 x51))).
X53 x y =  X52 a x y.
X54 x =  X53 t x.
X55 x y =  X10 X45 x y.
X56 x =  X55 a x.
X59 x57 x58 =  x57 (c (X20 x58)).
X60 x =  X53 c x.
X61 x =  X52 c t x.
X64 x62 x63 =  t (x62 (X43 (x62 x63))).
X65 x =  X55 g x.
X66 x =  X59 a x.
X68 x67 y =  X24 (X5 x67) y.
X72 x69 x70 x71 =  x69 (x70 (X16 (x69 x71))).
X75 x73 x74 =  c (X12 (x73 (x73 (c x74)))).
X76 x y =  X72 c x y.
X77 x =  X68 a x.
X78 x =  X76 c x.
X79 x =  X76 a x.
X80 x =  X72 a c x.
X83 x81 x82 =  g (X18 (t (x81 (x81 (X16 x82))))).
X85 x84 =  X44 (X32 x84).
X86 x =  X31 X66 x.
X87 x =  X59 X61 x.
X88 x =  X31 X80 x.
X89 x =  X11 X85 x.
X92 x90 x91 =  c (X56 (x90 (a (x90 (x90 x91))))).
X95 x93 x94 =  X43 (x93 (X56 (c (x93 x94)))).
X99 x96 x98 =  X21 x96 (X33 (x96 (x96 (t (X21 x96 x98))))).
X102 x100 x101 = X6 (x100 (c (X54 (g (x100 x101))))).
X105 x103 x104 = X18 (X45 (x103 (X32 (x103 (X12 x104))))).
X108 x106 x107 = t (X66 (X35 (x106 (t (x106 x107))))).
X111 x109 x110 =  X48 c (x109 (X30 (x109 (a x110)))).
X112 x =  X55 X89 x.
X114 x113 =  X89 (X56 x113).
X116 x115 =  c (a (X92 c x115)).
X117 x =  X21 X114 x.
X119 x118 = c (X116 (X88 x118)).
%ENDG

%BEGINA
q0 a -> q1.
q0 c -> q0.
q0 t -> q0.
q0 g -> q0.
q1 a -> q1.
q1 c -> q2.
q1 t -> q0.
q1 g -> q0.
q2 a -> q1.
q2 c -> q0.
q2 t -> q3.
q2 g -> q0.
q3 a -> q1.
q3 c -> q0.
q3 t -> q0.
q3 g -> q4.
q4 a -> q5.
q4 c -> q0.
q4 t -> q0.
q4 g -> q0.
q5 a -> q1.
q5 c -> q6.
q5 t -> q0.
q5 g -> q0.
q6 a -> q6.
q6 c -> q6.
q6 t -> q6.
q6 g -> q6.
q0 e -> .
q1 e -> .
q2 e -> .
q3 e -> .
q4 e -> .
q5 e -> .
%ENDA

Example 5 (for trivial automata model checking)

Check that no Fibonacci word contains "aaa" as a substring.

%BEGING
S = Fib b a.
Fib x0 x1 = br (x0 e) (Fib x1 (Concat x1 x0)).
Concat x y c = x(y c).
%ENDG

%BEGINA
/* Contains no aaa? */
q0 br -> q0 q0.
q0 a -> q1.
q0 b -> q0.
q1 b -> q0.
q1 a -> q2.
q2 b -> q0.
q0 e -> .
q1 e -> .
q2 e -> .
%ENDA

Example 6 (for query)

Define n-th sequence S(n) of an L-system by:

S(0) = f
S(n+1) = S(n) [ + S(n) ] S(n) [ - S(n) ] S(n)

Check that S(999) does not contain "ff" as a substring.

%BEGING 
/* S(999) (the following encoding uses the binary representation 1111100111 of 999) */
S = One(One(One(Zero(Zero(One(One (One (One Step)))))))) f e.
Step g z = g(lpar(plus (H g (lpar (minus (H g z)))))).
Zero h g z = h(h(g)) z.
One h g z = h(h(Step g)) z.
H g z = g (rpar (g z)).
%ENDG

%BEGINA
/* Contains no ff? */
q0 f -> q1.
q0 lpar -> q0.
q0 rpar -> q0.
q0 plus -> q0.
q0 minus -> q0.
q1 f -> q2.
q1 lpar -> q0.
q1 rpar -> q0.
q1 plus -> q0.
q1 minus -> q0.
q0 e -> .
q1 e -> .
%ENDA