A Logic for Seuss

The logic of action systems, developed in chapters 5 and 6, allowed us to specify safety and progress properties of a single box; the logic is extended in chapters 8 and 9 for specifications of ensembles of boxes. Properties such as co and leads-to specify the collective effect of the executions of the actions of a box or a set of boxes; the individual actions are not identified in a specification. Therefore, it is not possible to deduce from earlier specifications how a specific action affects the program state.