The aim of this project was: to provide efficient methods and tools for equivalent transformations of high-level models and to elucidate the relationship between asynchronous hardware implementation and behavioral high-level specifications of concurrent systems. Since the semantics of the most of the models is given in terms of transition systems we have chosen to develop methods of transformation of transition systems.
Method for manipulating Petri nets have been developed such that given a PN we can always obtain a transition-minimal and a place-minimal net. We studied the relationship between such place/transition minimization and state minimization of the transition systems. We also developed a method to manipulate with transition systems and Petri Nets and structural constraints such that a resulting net is to be a free-choice, safe, unique-choice, uniquely labelled, etc.
We developed a model, called Causal Logic Net, which is aimed as the least possible generalisation of Petri nets and Change Diagrams. It allows to express all types of OR-causality and AND-causality.