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