Automatic abstraction for synthesis and verification of deterministic timed systems

Journal ArticleThis paper presents a new approach for synthesis and verification of asynchronous circuits by using abstraction. It attacks the state explosion problem by avoiding the generation of a flat state space for the whole design. Instead, it breaks the design into sub-blocks and conducts synthesis and verification on each of them. Using this approach, the speed of synthesis and verification improves dramatically. This paper introduces how abstraction is applied to times Petri-nets to speed up synthesis and verification