The Inverse Method for Parametric Timed Automata
Étienne André, Romain Soulat · 2013
This chapter first formally defines the inverse problem by using the example of the “flip-flop” asynchronous circuit. Then, it introduces the inverse method, which is a solution to the inverse problem. This inverse method supposes that we are given a parametric timed automaton and a reference valuation of the parameters that we want to generalize. It also gives results of correctness and termination, and state properties of the method. Next, the chapter presents variants of the inverse method, solving different problems from the inverse problem, and discusses the applications. Finally, the chapter presents work related to the parameter synthesis for timed systems.