An Inverse Method for Parametric Timed Automata

Given a timed automaton with parametric timings, our objective is to describe a procedure for deriving constraints on the parametric timings in order to ensure that, for each value of parameters satisfying these nts, the behaviors of the timed automata are time-abstract equivalent. We will exploit a reference valuation of the parameters that is supposed to capture a characteristic proper behavior of the system. The method has been implemented and is illustrated on various examples of asynchronous circuits.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Étienne André, Thomas Chatain, Laurent Fribourg, Emmanuelle Encrenaz
• Keywords: Characteristic Proper Behavior, ENTCS 2008, Parametric Timings, Timed Automaton