Characterizing Locality (Encapsulation) with Bisimulation.

PABLO F. CASTRO; T.S.E. MAIBAUM

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlin; Año: 2010 vol. 6255 p. 322 - 336

0302-9743

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. References: [1] Fiadeiro, J.L., Maibaum, T.: Temporal theories as modularization units for concurrent system specification. Formal Aspects of Computing 4, 239–272 (1992) [2] Castro, P.F., Maibaum, T.: Deontic action logic, atomic boolean algebra and fault-tolerance. Journal of Applied Logic 7(4), 441–466 (2009)