Seminar: 16 February 2018, 13:15, EL41

Speaker: Ioannis Filippidis, Caltech

The design of complex engineering systems is typically structured hierarchically by specifying individual subsystems, and their interaction. We describe a method to algorithmically decompose a given overall system specification into a contract of realizable component specifications that together implement the given specification. The decomposition algorithm

eliminates variables that are irrelevant to realizability of each component, in order to simplify the specifications and reduce the amount of information communicated between components. The variables to be eliminated are identified by parametrizing the information flow between components.

The specifications are written in the Temporal Logic of Actions, TLA+, with liveness properties restricted to a fragment known as GR(1). We study whether GR(1) contracts exist in the presence of full information, and prove that introducing either safety constraints or memory is necessary for decomposition, leading to a decomposition algorithm that avoids circularity. We formalize a definition of realizability in TLA+, and define an operator for forming open-systems from closed-systems, based on stepwise implication.

Our symbolic algorithms use binary decision diagrams (BDDs). To convert the generated specifications from BDDs to readable formulas, we symbolically solve a minimal covering problem. We implemented an algorithm for minimal covering over lattices originally proposed for two-level logic minimization. We formalized the computation of essential elements and cyclic core that is part of this algorithm, and machine-checked the proofs of safety properties using a proof assistant.

For presentation slides, please contact Dr Filippidis directly here.