| |
|
|
Electronic Systems Design Seminar
|
|
In this talk I will cover some of my dissertation work. I will focus on the composition and control of synchronous systems. In the synchronous composition of processes, one process may prevent another from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify increasingly stronger notions of typing mechanisms and study their effects on the control problem. The semantics of the types are given in game-theoretic terms, and are able to capture interesting classes of circuits such as all constructive, delay-insensitive circuits, studied by researchers including Gerard Berry, Tom Shiple etc.
Having classified various types of synchronous systems, we will focus on their corresponding control problems. In particular, we define and study the single-step control problem, that is, whether the controller has a strategy to reach the goal in exactly one step, no matter what the system does. The single-step control problem is of both practical and theoretical interest because an algorithm for solving it can be used as a subroutine to solve any LTL control problem of synchronous systems. We study the complexties of single-step control problems, and show that, contrary to folk wisdoms, the notion of "the most general controller" for safety properties does not exist in general for most synchronous systems.
Freddy Mang is currently a R&D Engineer in the Advanced Technoloogy Group of Synopsys, Inc. His doctoral dissertation is on Games for Verification and Synthesis.