Exploiting Implicit Representations in Timed Automaton Verification for Controller Synthesis

Abstract

Automatic controller synthesis and verification techniques promise to revolutionize the construction of high-confidence software. However, approaches based on explicit state-machine models are subject to extreme state-space explosion and the accompanying scale limitations. In this paper, we describe how to exploit an implicit, transition-based, representation of timed automata in controller synthesis. The CIRCA Controller Synthesis Module (CSM) automatically synthesizes hard realtime, reactive controllers using a transition-based implicit representation of the state space. By exploiting this implicit representation in search for a controller and in a customized model checking verifier, the CSM is able to efficiently build controllers for problems with very large state spaces. We provide experimental results that show substantial speed-up and orders-of-magnitude reductions in the state spaces explored. These results can be applied to other verification problems, both in the context of controller synthesis and in more traditional verification problems.

This material is based upon work supported by DARPA/ITO and the Air Force Research Laboratory under Contract No. F30602-00-C-0017.The authors thank Stavros Tripakis for many helpful suggestions. Thanks also to our anonymous referees.