Behavioral Congruences For Wide Reactive Systems

There are many concurrent ones among computer systems nowadays. Because ofthe intrinsic complexity of concurrent systems, we have not still known the essence ofconcurrency. So the reliability and correctness of such systems cannot be ensured.In order to account for the essence of concurrency and to achieve the methodologyof developing concurrent systems correctly, R. Milner introduced the theory of bigra-phical reactive systems (Brs) in 2001. In this model for concurrency, a state of a systemis represented as a bigraph, and a transition between states is represented as a reactionrule for bigraphs. Brss are instances of wide reactive systems (Wrs). In order to usestep-wise refinements in system developments and compositional approaches when analy-zing system behavior, behavioral relations are required to be congruences. R. Milner hasproved that bisimilarity in a Wrs which has sufficient relative pushouts (RPO) is a con-gruence, and has proved further that it in a concrete Brs is a congruence.On the foundations of J. J. Leifer's and R. Milner's theory, and using basic methodsin category theory, this thesis answers the following questions: whether three usual beha-vioral relations-trace preorder, weak bisimilarity and failure preorder-in a Wrs, itssupport quotient, and a concrete Brs are respectively congruences.The thesis first proves that, in the support quotient of a Wrs which has sufficientrelative pushouts (RPO), trace preorder is a congruence, and weak bisimilarity and failurepreorder are both congruences in its reactive context sub-s-category. And on the foun-dation of these conclusions, the thesis then proves that, in a Wrs which has sufficient rela-tive pushouts (RPO), trace preorder is a congruence, and weak bisimilarity and failurepreorder are both congruences in its reactive context, sub-s-category. And further, in anyBrs, trace preorder is proved to be a congruence, and weak bisimilarity and failure preorder are both proved to be congruences in its reactive context sub-s-category.