RTRecS (Recursive Types for RECursion Schemes): Type-Based Model Checker for Higher-Order Recursion Schemes with Recursive Types

This is a model checker for mu-HORS, higher-order recursion schemes extended with recursive types. (Note that the standard recursion schemes must be simply-typed.) As the extended model checking problem is undecidable, our model checker may not terminate for certain inputs. However, our model checker is relatively complete in the sense that if a given mu-HORS is typable in a recursive intersection type system, the model checker will eventually terminate and find a certificate in theory. (In pratice, the model checker may of course time out or run out of memory.) The model checker uses a SAT solver Minisat 2.2.0 in the backend.

You can check our model checker through the web interface below. Enter a recursion scheme and a specification in the box below, and press the "submit" button. Examples are given below. Currently, our model checker only accepts deterministic Buchi automata with a trivial acceptance condition. Note that on this web interface, only small examples can be tested, as the time-out is set to one second. In general, RTRecS works only for automaton with a very small number of states. Please contact Naoki Kobayashi if you need source code.

Other versions of model checkers for higher-order recursion schemes are available from the following links: TRecS   GTRecS   GTRecS2


Examples

Some examples are given below. More examples are available from the web page on a model checker for FJ. (Do not try, however, twofiles-OO.hrs, for which RTRecS times out.)

Example 1

%BEGING    /*** Rewring rules of a recursion scheme. Non-terminal must start with a capital letter. ***/
S -> F c.  /*** The non-terminal of the first rule is interpreted as the start symbol. ***/
F x -> a x (F (b x)).  /*** Unbounded names ("a", "b" in this rule) are interpreted as terminals. ***/
%ENDG

%BEGINA    /*** Transition rules of a Buchi tree automaton (where all the states are final). ***/
q0 a -> q0 q0. /*** The first state is interpreted as the initial state. **/
q0 b -> q1.
q1 b -> q1.
q0 c -> .
q1 c -> .
%ENDA

Example 2

Same as Example 2, except that recursion is realized by using recursive types, instead of term-level recursion. 
%BEGING    
S -> G G c.  
G g x -> a x (g g (b x)).  
%ENDG

%BEGINA    /*** Transition rules of a Buchi tree automaton (where all the states are final). ***/
q0 a -> q0 q0. /*** The first state is interpreted as the initial state. **/
q0 b -> q1.
q1 b -> q1.
q0 c -> .
q1 c -> .
%ENDA

Example 3

The following recursion scheme simply diverges without generating any node. Thus it is accepted by any trivial automaton. 
%BEGING    
Omega -> X X.  
X x -> x x.  
%ENDG

%BEGINA    
q0 a -> q0 q0. 
q0 b -> q1.
q1 b -> q1.
q0 c -> .
q1 c -> .
%ENDA

Example 4

RTRecS works relatively better than TRecS for recursion schemes that generate huge trees. The following recursion scheme generates a huge tree, of the form a2225 c. The automaton describes the property that the number of "a" is even. 
%BEGING
S -> F0 G2 G1 G0.
F0 f x z -> F1 (F1 f) x z.
F1 f x z -> F2 (F2 f) x z.
F2 f x z -> F3 (F3 f) x z.
F3 f x z -> F4 (F4 f) x z.
F4 f x z -> F5 (F5 f) x z.
F5 f x z -> G3 f x z.
G3 f x z -> f (f x) z.
G2 f x -> f (f x).
G1 x -> a x.
G0 -> c.
%ENDG

%BEGINA
q0 a -> q1.
q1 a -> q0.
q0 c -> .
%ENDA