Synthesizing Timed Automata with Minimal Numbers of Clocks from Optimised Timed Scenarios
摘要
We address the problem of synthesizing a timed automaton from a set of optimised timed scenarios, and present a simple, efficient algorithm that solves the problem. Under a simplifying assumption about the set of scenarios we show that our synthesized automaton has the minimal number of clocks in the entire class of language-equivalent automata.