HorSat: A model checker for HORS based on SATuration

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.

See also a companion paper that tries to formalize a connection to the saturation algorithm for CPDS (Collapsible Pushdown Systems) through a simplified version of CPDS:

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

The benchmark suite used in the first paper above (which comes from the benchmark programs of TRecS and TravMC; thanks to Ryosuke Sato, Yoshihiro Tobita, Hiroshi Unno, and the TravMC Team) is available here as a zip file. Other implementations of higher-order model checkers ( TRecS, described in Kobayashi's PPDP09 paper GTrecS, described in Kobayashi's FoSSaCS 11 paper, and GTrecS2, a successor of GTRecS) are available elsewhere.

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'.

Examples

Some examples are given below. More examples are available here .

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

The following recursion scheme generates a huge tree, of the form a^{2^{2^2⁵}} 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

Example 3

/*** 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