In: Formal Methods in Computer-Aided Design (FMCAD 2002), Proceedings of the 4th International Conference, Portland, OR, USA, November 6-8, 2002, pages 360-377. Volume 2517 of Lecture Notes in Computer Science / M.D. Aagaard, J.W. O'Leary (Eds.) --- Springer Verlag, November 2002.
Abstract: The notion of I/O compatibility of reactive systems is defined. It models the fact that two systems can be connected and establish a correct dialogue through their input and output events. I/O compatibility covers safeness and liveness properties that can be checked with a polynomial-time decision procedure. The relationship between observational equivalence, I/O compatibility and input properness is also studied with the aim at supporting the proposal of transformations for the synthesis of reactive systems. Finally, a set of Petri net transformations that preserve I/O compatibility are shown as an example of application of the theory presented in this paper.
Keywords: Reactive systems; Input/Output compatibility; Observational equivalence; Synchronous product; Trace theory; Conformation; Petri nets.