From Scenarios to Optimally Allocated Timed Automata

Abstract

Our contribution is twofold. First, we develop a new method for synthesizing a formal model for real-time systems from scenarios. Scenarios describe partial behaviours of realtime systems during some time interval. We propose Timed Event Sequences to formally express scenarios. Given a set of scenarios as Timed Event Sequences, along with a mode graph, we propose a method to automatically construct a minimal, acyclic, and deterministic timed automaton that models the specified aspects of the system. Second, we consider the problem of optimally allocating clocks in timed automata. Reducing the number of clocks in a timed automaton is important, as it directly affects the complexity of the verification problem. Given a timed automaton, it is undecidable, in general, to check whether there exists another timed automaton that accepts the same language but has fewer number of clocks. We identify a fairly general class of timed automata and propose an algorithm (polynomial time) for optimally allocating clocks to timed automata in this class. The previous approaches changed the shape of the graph of the original timed automaton by constructing bisimilar timed automata. Our method does not change the graph of timed automata. The cost of our algorithm is quadratic in the size of the underlying graph of the timed automaton.