Algorithms for Reengineering and Synthesis (ARS)

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

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.