Automated Incremental Synthesis of Timed Automata

Borzoo Bonakdarpour and Sandeep S. Kulkrani

Abstract

In this paper, we concentrate on incremental synthesis of timed automata for automatic addition of different types of bounded response properties. Bounded response -- that \emph{something good} will happen soon, in a certain amount of time -- captures a wide range of requirements for specifying real-time and embedded systems. We show that the problem of automatic addition of a bounded response property to a given timed automaton while maintaining maximal nondeterminism is NP-hard in the size of locations of the input automaton. Furthermore, we show that by relaxing the maximality requirement, we can devise a sound and complete algorithm that adds a bounded response property to a given timed automaton, while preserving its existing universally quantified properties (e.g., \textsc{Mtl}). This synthesis method is useful in adding properties
that are later discovered as a crucial part of a system. Moreover, we show that addition of interval-bounded response, where the good thing should not happen sooner than a certain amount of time, is also NP-hard in the size of locations even without maximal nondeterminism. Finally, we show that the problems of adding bounded and unbounded response properties are both \textsc{Pspace}-complete in the size of the input timed automaton.


Paper:


Return to the publication list
Return to the Sandeep's home page