Exploiting implicit representations in timed automaton verification for controller synthesis

Abstract. Automatic controller synthesis and verication techniques promise to revolutionize the construction of high-condence 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 real-time, 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 verier, the CSM is able to eciently 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 verication problems, both in the context of controller synthesis and in more traditional verication problems.