Characterizing Locality (Encapsulation) with Bisimulation

In this paper we investigate formal mechanisms to allow designers to decompose specifications (stated in a given logic) into several components. The basic ideas come from [1] where some notions from category theory are used to put together logical specifications. In this setting the concept of locality allows designers to write separate specifications and then compose them. However, as the work of Fiadeiro and Maibaum [1] is stated in a linear temporal logic, we investigate how to extend these notions to a branching time logic, which can be used to specify systems where non-determinism is a relevant mechanism. Since we are interested in specifying and verifying fault-tolerant systems, we also introduce deontic operators in our logic, we have shown in [2] that deontic logic allows us to express notions such as ideal and abnormal behavior which are closely related to fault-tolerance.