BRAT is a prototype bounded reachability analyzer for timed automata networks described in [1]. It is intended as proof of concept for how a MILP solver (here, Gurobi) may be used for bounded reachability analysis and model checking.
The tool builds two encodings for the reachability problem, one in MILP and one as an SMT problem over linear arithmetics (using MathSAT or Z3 as backend solver, via pysmt). The constraints expressed in both encodings are identical, allowing for comparisons between the two approaches/solvers. Different variants of encoding are available, please refer to [1].
Attention: this is (just) a prototype, with all the usual caveats. In particular, there is no language for specifying timed automata and very few syntactic and structural checks are made on the models. Please refer to the examples and use with caution!
Please fill the following form in order to receive the download link:
[1] Iulian Ober. Revisiting bounded reachability analysis of timed automata based on MILP. In FMICS 2018: 23rd International Conference on Formal Methods for Industrial Critical Systems. LNCS, 2018