Synthesis and reengineering of persistent systems

In formal verification, a structural object, such as a program or a Petrinet, is given, and questions are asked about its behaviour. In system synthesis,conversely, a behavioural object, such as a transition system, is given, and questionsare asked about the existence of a structural object realising this behaviour.In system reengineering, one wishes to transform a given system into another one,with similar behaviour and other properties not enjoyed by the original system.This paper addresses synthesis and reengineering problems in the specific frameworkof finite-state labelled transition systems, place/transition Petri nets, andbehaviour isomorphisms. Since algorithms solving these problems are prohibitivelytime-consuming in general, it is interesting to know whether they can be improvedin restricted circumstances, and whether direct correspondences can be found betweenclasses of behavioural and classes of structural objects.This paper is concerned with persistent systems, which occur in hardware designand in various other applications. We shall derive exact conditions for a finite persistenttransition system to be isomorphically implementable by a bounded Petrinet exhibiting persistence in a structural way, and derive an efficient algorithm tofind such a net if one exists. For the class of marked graph Petri nets, this leadsto an exact characterisation of their state spaces.SCOPUS: ar.j