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

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

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.