This is a Web interface for a new version of a higher-order model checker HorSat. The technical background is described in:

- Christopher Broadbent and Naoki Kobayashi, Saturation-Based Model Checking of Higher-Order Recursion Schemes, a preliminary version of the paper that will appear in Proceedings of CSL 2013.

- Christopher Broadbent and Naoki Kobayashi, Streamlining Collapsible Pushdown Systems and their Model-Checking , draft.

Enter a recursion scheme and a tree automaton (in the TRecS format) in the box below, choose the functionality, and press the "submit" button. The property should be given using a trivial tree automaton. (In the "co-trivial automaton model checking" below, the complement of the trivial tree automaton is constructed internally.) Some examples are given below. Note that on this web interface, only small examples can be tested (as the time-out is set to 3 seconds). The source code is available here, under the subdirectory 'horsat'.

%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 -> 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

/*** An example taken from POPL09 paper, which creates and accesses two files ***/ %BEGING S -> Newr C1. C1 x -> Neww (C2 x). C2 x y -> F x y end. F x y k -> br (Close x (Close y k)) (Read x (Write y (F x y k))). I x y -> x y. K x y -> y. Newr k -> br (newr (k I)) (k K). Neww k -> br (neww (k I)) (k K). Close x k -> x close k. Read x k -> x read k. Write y k -> y write k. %ENDG %BEGINA q0 br -> q0 q0. qr br -> qr qr. qw br -> qw qw. qrw br -> qrw qrw. q0 newr -> qr. qr read -> qr. qr close -> qc. q0 neww -> qw. qw write -> qw. qw close -> qc. qw newr -> qrw. qr neww -> qrw. qrw read -> qrw. qrw write -> qrw. qrw close -> qrw. qc end ->. q0 end ->. qrw end ->. %ENDA