WG211/M7Smith1

Calculating Refinements in Algorithm and System Design

Doug Smith

I've been working on a unified treatment of algorithm and system design. The key is to treat system specification as a combination of dynamical models (to model physical components and other existing infrastructure) and logical constraints on behavior (e.g. trace predicates). The key incremental synthesis problem then is to calculate a refinement of the current model to incorporate one of the logical constraints. These kinds of calculations require a game-theoretic setting, since that's the proper foundation for designing interacting systems. Previous work on algorithm design work in KIDS and Specware falls out as a special case of this framework.