Skip to main content

Automated Incremental Synthesis of Timed Automata

Publication Type
Year of Publication
Conference/Journal Name
Formal Methods in Industrial Critical Systems (FMICS)
In this paper, we concentrate on incremental synthesis of timed automata for automatic addition of different types of bounded response properties. Bounded response – that 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 non-determinism 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., 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 PSPACE-complete in the size of the input timed automaton.