The Control of Synchronous Systems

In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a wellde ned productbehavior are ruled out. They can be ruled out semantically,by insisting on the existence of certain xed points, or syntactically, by equipping processeswith types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their e ects on the control problem. A static type enforces xed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process...

• Type: Conference
• Year: 2000
• Where: CONCUR
• Authors: Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang
• Keywords: Compatible Dynamic Type, CONCUR 2000, Control Problems, Distributed And Parallel Computing, Dynamic Type