Algorithms for Reengineering and Synthesis (ARS)

• Applicant: Professor Dr. Ernst-Rüdiger Olderog, since 11/2018
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 265430725

In formal verification, one analyses the behaviour of some structural object, such as a program, or a Petri net. In system synthesis, a converse question is asked: Given some specified behaviour, does there exist a structural object implementing this behaviour? Both approaches are widely considered and have a broad spectrum of applications in computer science. For instance, if some desired behaviour is specified in a sequential way by a transition system, it may be asked whether there exists some concurrent Petri net realising it. In system reengineering, a related question is asked: For some already existing implementation, is there a `better' (e.g.: more regular, less sequential) one? These questions have been extensively studied, and algorithms have been developed. Such algorithms can serve to derive an implementation automatically from a specification, but even for finite-state systems, they are prohibitively time-consuming in the general case. Nevertheless, one does not always need the full generality but can often focus on regular subclasses of systems which are significant in the application contexts being considered. It is therefore interesting to investigate whether synthesis and reengineering methods can be improved under restrictive circumstances. For example, in digital circuit design, one considers globally clocked systems in the synchronous case and (as far as possible) persistent and hazard-free systems in the asynchronous case. On the one hand, such restrictions and correspondingly adapted methods may lead to more efficient algorithms. On the other hand, there may also exist more transparent, or tighter, mathematical relationships between classes of behavioural and classes of structural objects than in the general case. This project proposes a systematic study of such correspondences within the framework of labelled transition systems as behavioural objects and general place/transition Petri nets as structural objects, with an emphasis on obtaining efficient synthesis and reengineering algorithms. Initially and throughout the project, the focus will be on persistent systems. Informally, persistency means that an activity which is enabled cannot become disabled by other activities. Such systems are not only non-trivial, but also of practical relevance. The study of persistent systems will gradually be extended to other system classes. Special attention will be paid to the question whether they can not only be implemented in a concurrent way, but also be distributed physically.

• DFG Programme: Research Grants
• Ehemaliger Antragsteller: Professor Dr. Eike Best, until 10/2018