A Small Model Theorem for Rectangular Hybrid Automata Networks

The PASSEL inductive invariant checking executable and HyXML specification files can be downloaded here.