Towards Practical Verification of Reachability Checking for Timed Automata

Prior research has shown how to construct a mechanically verified model checker for timed automata, a popular formalism for modeling real-time systems. We extend this work to improve its value for practical timed automata model checking in two ways. First, we shift the focus from verified model checking to certifying unreachability. This allows us to benefit from better approximation operations for symbolic states, and reduces execution time by exploring fewer states and by exploiting parallelism. Moreover, this gives us the ability to audit results of unverified model checkers that implement a range of further optimizations, including certificate compression. Second, we provide an improved modeling language that includes the popular modeling features of broadcast channels as well as urgent and committed locations. The resulting tool is evaluated on a set of standard benchmarks to demonstrate its practicality, using a new unverified model checker implementation in Standard ML to construct the certificates.