Encapsulating deontic and branching time specifications

In this paper, we investigate formal mechanisms to enable designers to decompose specifications (stated in a given logic) into several interacting components in such a way that the composition of these components preserves their encapsulation and internal non-determinism. The preservation of encapsulation (or locality) enables a modular form of reasoning over specifications, while the conservation of the internal non-determinism is important to …