A Logical View of Composition and Refinement

Abstract

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition and refinement rules, and a framework for the use of the modular specification methods that these rules underpin. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear.