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

%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

%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

%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

%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