Algorithms for Reengineering and Synthesis (ARS)

在形式验证中，人们分析一些结构化对象的行为，如程序或Petri网。在系统综合中，一个匡威的问题被问到：给定一些特定的行为，是否存在一个实现这种行为的结构对象？这两种方法都被广泛考虑，并在计算机科学中有广泛的应用。例如，如果某个期望的行为是由一个变迁系统以顺序的方式指定的，那么可能会问是否存在某个并发Petri网来实现它。在系统再工程中，会问一个相关的问题：对于某个已经存在的实现，是否有一个“更好的”（例如：更有规律，更少的顺序）一个？这些问题已被广泛研究，并已开发出算法。这样的算法可以自动从规范中导出实现，但即使对于有限状态系统，它们在一般情况下也非常耗时。尽管如此，人们并不总是需要完全的一般性，但通常可以专注于在所考虑的应用环境中重要的系统的常规子类。因此，有趣的是，研究是否可以在限制性的情况下，改进合成和再造方法。例如，在数字电路设计中，在同步情况下考虑全局时钟系统，在异步情况下（尽可能）考虑持久和无风险系统。一方面，这样的限制和相应地适应的方法可以导致更有效的算法。另一方面，在行为对象类和结构对象类之间也可能存在比一般情况下更透明或更紧密的数学关系。该项目提出了一个系统的研究，这种对应关系的框架内标记的过渡系统的行为对象和一般的地方/过渡Petri网的结构对象，重点是获得有效的合成和再造算法。在项目初期和整个过程中，重点将放在持久性系统上。非正式地，持久性意味着启用的Activity不能被其他Activity禁用。这种系统不仅重要，而且具有实际意义。对持久系统的研究将逐渐扩展到其他系统类。将特别注意的问题是，它们是否不仅可以同时实施，而且还可以物理分布。

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.