Input/output compatibility of reactive systems

Abstract

The notion of I/O compatibility ofreactiv e 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 ofP etri net transformations that preserve I/O compatibility are shown as an example ofapplication ofthe theory presented in this paper.