Document Open Access Logo

Conditional Bisimilarity for Reactive Systems

Authors Mathias Hülsbusch, Barbara König, Sebastian Küpper, Lara Stoltenow

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.10.pdf
  • Filesize: 0.57 MB
  • 19 pages

Document Identifiers

Author Details

Mathias Hülsbusch
  • Universität Duisburg-Essen, Germany
Barbara König
  • Universität Duisburg-Essen, Germany
Sebastian Küpper
  • FernUniversität in Hagen, Germany
Lara Stoltenow
  • Universität Duisburg-Essen, Germany

Funding

Research partially supported by DFG Project BEMEGA.

Cite AsGet BibTex

Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow. Conditional Bisimilarity for Reactive Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.10

Abstract

Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We instantiate reactive systems in order to obtain DPO graph rewriting and consider a case study in this setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Program reasoning
Keywords
  • conditional bisimilarity
  • reactive systems
  • up-to context
  • graph transformation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Jiří Adámek, Filippo Bonchi, Mathias Hülsbusch, Barbara König, Stefan Milius, and Alexandra Silva. A coalgebraic perspective on minimization and determinization. In Proc. of FOSSACS '12, pages 58-73. Springer, 2012. LNCS/ARCoSS 7213. Google Scholar
  2. Paolo Baldan, Andrea Bracciali, and Roberto Bruni. Bisimulation by unification. In Proc. of AMAST '02, pages 254-270. Springer, 2002. LNCS 2422. Google Scholar
  3. Harsh Beohar, Barbara König, Sebastian Küpper, and Alexandra Silva. Conditional transition systems with upgrades. In Proc. of TASE '17 (Theoretical Aspects of Software Engineering). IEEE Xplore, 2017. Google Scholar
  4. Filippo Bonchi. Abstract Semantics by Observable Contexts. PhD thesis, Università degli Studi di Pisa, Dipartimento di Informatica, May 2008. Google Scholar
  5. Filippo Bonchi, Barbara König, and Ugo Montanari. Saturated semantics for reactive systems. In Proc. of LICS '06, pages 69-80. IEEE, 2006. Google Scholar
  6. H.J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König. Conditional reactive systems. In Proc. of FSTTCS '11, volume 13 of LIPIcs. Schloss Dagstuhl - Leibniz Center for Informatics, 2011. Google Scholar
  7. Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay. Simulation-based abstractions for software product-line model checking. In Proc. of ICSE '12, pages 672-682. IEEE, 2012. Google Scholar
  8. Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, and Michael Löwe. Algebraic approaches to graph transformation - part I: Basic concepts and double pushout approach. In G. Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformation, Vol. 1: Foundations, chapter 3. World Scientific, 1997. Google Scholar
  9. Hartmut Ehrig and Barbara König. Deriving bisimulation congruences in the DPO approach to graph rewriting. In Proc. of FOSSACS '04, pages 151-166. Springer, 2004. LNCS 2987. Google Scholar
  10. Hartmut Ehrig, Michael Pfender, and Hans Jürgen Schneider. Graph-grammars: An algebraic approach. In 14th Annual Symposium on Switching and Automata Theory (SWAT 1973), pages 167-180, October 1973. Google Scholar
  11. Melvin Fitting. Bisimulations and boolean vectors. In Advances in Modal Logic, volume 4, pages 1-29. World Scientific Publishing, 2002. Google Scholar
  12. Annegret Habel, Reiko Heckel, and Gabriele Taentzer. Graph grammars with negative application conditions. Fundamenta Informaticae, 26(3,4):287-313, December 1996. Google Scholar
  13. Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout graph transformation revisited. Mathematical Structures in Computer Science, 11(5):637-688, October 2001. Google Scholar
  14. Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 19(2):245-296, 2009. Google Scholar
  15. Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theoretical Computer Science, 138(2):353-389, 1995. Google Scholar
  16. Mathias Hülsbusch and Barbara König. Deriving bisimulation congruences for conditional reactive systems. In Proc. of FOSSACS '12, pages 361-375. Springer, 2012. LNCS/ARCoSS 7213. Google Scholar
  17. Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow. Conditional bisimilarity for reactive systems, 2020. arXiv:2004.11792. URL: https://arxiv.org/abs/2004.11792.
  18. Ole Høgh Jensen and Robin Milner. Bigraphs and transitions. In Proc. of POPL 2003, pages 38-49. ACM, 2003. Google Scholar
  19. Bartek Klin, Vladimiro Sassone, and Paweł Sobociński. Labels from reductions: towards a general theory. In Proc. of CALCO '05, pages 30-50. Springer, 2005. LNCS 3629. Google Scholar
  20. Stephen Lack and Paweł Sobociński. Adhesive and quasiadhesive categories. RAIRO - Theoretical Informatics and Applications, 39(3):511-545, 2005. Google Scholar
  21. Kim Guldstrand Larsen. Context-Dependent Bisimulation between Processes. PhD thesis, University of Edinburgh, 1986. Google Scholar
  22. James J. Leifer and Robin Milner. Deriving bisimulation congruences for reactive systems. In CONCUR 2000 - Concurrency Theory: 11th International Conference University Park, PA, USA, August 22-25, 2000 Proceedings, pages 243-258. Springer Berlin Heidelberg, 2000. Google Scholar
  23. Dennis Nolte. Automatischer Nachweis von Bisimulationsäquivalenzen bei Graphtransformationssystemen. Master’s thesis, Universität Duisburg-Essen, November 2012. Google Scholar
  24. Damien Pous. Complete lattices and up-to techniques. In Proc. of APLAS '07, pages 351-366. Springer, 2007. LNCS 4807. Google Scholar
  25. Damien Pous and Davide Sangiorgi. Enhancements of the coinductive proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  26. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, 1998. Google Scholar
  27. Vladimiro Sassone and Paweł Sobociński. Reactive systems over cospans. In Proc. of LICS '05, pages 311-320. IEEE, 2005. Google Scholar
  28. Paweł Sobociński. Deriving process congruences from reaction rules. PhD thesis, University of Aarhus, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact