Checking Equivalence for Reo Networks

Tobias BlechmannTobias Blechmann, Christel BaierChristel Baier

DOI Link

Tobias Blechmann, Christel Baier
Checking Equivalence for Reo Networks
Proc. of the 4th International Workshop on Formal Aspects of Component Software (FACS), volume 215 of Electronic Notes in Theoretical Computer Science, 209--226, 2008. Elsevier

Details
Bibtex

KurzfassungAbstract
Constraint automata have been used as an operational model for component connectors described in the coordination language Reo which specifies the cooperation and communication of the components by means of a network of channels. This paper addresses the problem of checking equivalence of two Reo networks. We present a compositional approach for the generation of a symbolic representation of constraint automata for Reo networks and report on an implementation that realizes a partitioning splitter technique for checking bisimulation equivalence for Reo networks. Using a special operator on our symbolic data structure enables efficient treatment of the rich labeled transitions in constraint automata. In order to show the power of this approach we then present some benchmarks.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BB2008,
  author    = {Tobias Blechmann and Christel Baier},
  title     = {Checking Equivalence for Reo Networks},
  booktitle = {Proc. of the 4th International Workshop on Formal Aspects of
               Component Software (FACS)},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {215},
  publisher = {Elsevier},
  year      = {2008},
  pages     = {209--226},
  doi       = {10.1016/J.ENTCS.2008.06.029}
}