ITR: Synthesis System for Discrete Event Systems through Solving Equations over Mathematical Machines

自动机有状态和状态之间的转换；有些状态被标记为“接受”。从初始状态开始，输入符号序列使自动机改变状态作为响应。如果序列可以使自动机结束于接受状态，则输入符号序列被认为是被接受的，并且被定义为使用自动机的语言。有限状态机(FSM)与自动机的不同之处在于，所有状态都是可接受的，并且每个输入符号被分为输入部分和输出部分。自动机和FSM被用来定义“常规”语言。许多有趣的问题都可以用自动机、FSM或Petri网及其所涉及的语言来定义。这些问题包括二值和多值逻辑综合、工程更改、离散控制器设计、逻辑验证、测试、推导离散游戏的制胜策略、协议构造和密码学。我们小组观察到，这些不同的应用程序可以在语言解决方面以统一的方式形式化。一般而言，在已知环境和外部规范的情况下，这些问题可以用子系统或组件的合成来说明。要合成的成分可能已经存在，在这种情况下，目标是提供更好或最优的替代。在其他情况下，可能还不存在任何实现，目标是检查是否存在这样一个所需的子系统，如果存在，则找到最佳实现。前者的一个例子是在由相互作用的元件组成的微芯片上发现的数字系统。系统可以按原样正常运行，即系统已经满足其外部规范，但其中一个组件在速度、成本、功率等方面需要改进。一个实施可能未知的例子是控制系统，其中我们被给予一个“对象”和一个外部规范，声明对象的输出总是保持在一定的范围内(是稳定的)，我们想要合成一个摩尔型FSM反馈控制单元来完成这项工作。“工程变更”，发生在系统几乎完全设计完成，但在最后一刻，其概念中的错误需要更改系统的规范。如果只有一个组件可以更改，而其他组件保持不变，就会出现一个问题。在生物系统中，在组件内部进行测量的能力通常是有限的，但需要合成组件的模型。有几种方式可以使两个子系统交互(可以组合)。在硬件中，通常将两个组件连接在一起，并使用时钟同步它们的交互；在每个时钟节拍上，信息都会交换。在软件中，通信是“异步”的；只有在经过了足够的时间后，信息才被发送到另一个组件，以便另一个组件有足够的“循环”来计算其结果。这类问题可以归结为求解如下形式的方程，其中X是要导出的未知组件，A描述系统已知部分的行为(或环境)，S是外部规范或期望的行为，是一种描述A和X如何通信的并行合成操作符，并且是说明整个系统何时满足规范的一致性关系。像许多方程一样，解可能不是唯一的，因此也存在寻找“最佳”解的问题。具有适当附加性质的受限解集是感兴趣的，例如，没有死锁或活锁，或者是摩尔型有限状态机的解。我们建议：1.开发在各种数学机器、合成算子和一致性关系上求解方程所需的数学工具。针对不同的问题领域，确定并表征具有实际意义的受限解决方案的子集。开发高效的计算机工具，用于在不同的数学表示中构造解决方案。研究并制定对不同应用有用的方程类型。5.开发提取最优解的方法。建立一个软件系统，在这个系统中，方程很容易指定，并且已经实现了构造最优解的有效工具。最后一个目标很重要，因为已知的求解方法计算复杂。这导致缺乏任何构建解决方案和探索这些问题的系统。我们已经开发了一个系统MVSIS，用于多层次、多值、非确定性网络的综合和优化。在操纵逻辑方面，它变得特别高效。我们建议在MVSIS中表示语言求解问题，并开发派生解决方案所需的各种操作的新实现。此外，我们还将开发从一般解中找到最优子解的方法。

An automaton has states and transitions between states; some states are marked as "accepting". Starting from the initial state, a sequence of input symbols causes the automaton to change states in response. If a sequence can cause the automaton to end up at an accepting state, the sequence of input symbols is said to be accepted and is defined to be in the language of the automaton. Finite state machines (FSMs) differ from automata in that all states are accepting and each input symbol is divided into an input part and an output part. Automata and FSMs are used to define "regular" languages. Many interesting problems can be defined in terms of automata, FSMs, or Petri nets and the languages involved. These include problems in binary and multi-valued logic synthesis, engineering change, design of discrete controllers, logic verification, testing, deriving winning strategies for discrete games, construction of protocols, and cryptography. It was observed by our group that these diverse applications could be formalized in a unified way in terms of language solving. In general, these problems can be stated in terms of the synthesis of a subsystem or component, given a known environment and an external specification. The component to be synthesized may already exist, in which case the goal is to provide a better or optimum alternative. In other cases, no implementation may yet exist, and the goal is to check if such a desired subsystem exists, and if so to find an optimal implementation. An example of the former is a digital system as found on a microchip composed of interacting components. The system may operate correctly as is, i.e. the system already satisfies its external specification, but one of the components should be improved, in terms of speed, cost, power, etc. An example in which an implementation may be unknown is a control system where we are given a "plant" and an external specification, stating that the output of the plant always stays within certain bounds (is stable), and we want to synthesize a Moore type FSM feedback control unit which does the job. "Engineering change", occurs when a system has been almost completely designed, but at the last moment, a bug in its concept requires the system's specification to be changed. A question arises if just one component can be changed while the other components are left alone. In a biological system, the ability to make measurements inside a component is often limited, but a model of the component is required to be synthesized. There can be several ways that two subsystems interact (can be composed). In hardware, typically two components are wired together and their interaction synchronized using a clock; on each clock tick, information is exchanged. In software, the communication is "asynchronous"; information is sent to another component only after enough time has passed so that the other component has had enough "cycles" to compute its result.Such problems can be reduced to solving an equation of the form, ,where X is the unknown component to be derived, A describes the behavior (or environment) of the known part of the system, S is the external specification or desired behavior, is a type of parallel composition operator describing how A and X, are to communicate, and is a conformance relation stating when the overall system satisfies the specification. Like many systems of equations, the solution may not be unique; hence there is also the problem of finding a "best" solution. Sets of restricted solutions that have appropriate additional properties are of interest, e.g. no deadlocks or livelocks, or a solution that is a Moore-type FSM.We propose to:1. Develop the mathematical tools required for solving equations over various mathematical machines, composition operators and conformance relations.2. Determine and characterize, for various problem areas, subsets of restricted solutions, which are of practical interest.3. Develop efficient computer tools for constructing solutions within different mathematical representations.4. Study and formulate the types of equations that are useful for different applications. 5. Develop methods for extracting optimum solutions.6. Build a software system where the equation is easily specified and efficient tools for constructing optimum solutions have been implemented.The last goal is important because the known methods of solutions are computationally complex. This has led to the lack of any system for constructing solutions and exploring these problems. We have already developed a system, MVSIS, for the synthesis and optimization of multi-level, multi-valued, non-deterministic networks. It has been made especially efficient in manipulating logic. We propose to represent language solving problems in MVSIS and develop new implementations of various operations required to derive the solutions. In addition, we will develop methods which find an optimum sub-solution from a general solution.