Skip to main content
SpringerLink
Log in

Linking Algebraic Observational Equivalence and Bisimulation

  • Conference paper
Developments in Language Theory (DLT 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6224))

Included in the following conference series:

  • 593 Accesses

Abstract

Observability concepts allow to focus on the observable behaviour of a system while abstracting internal details of implementation. In this context, formal verification techniques use behavioural equivalence notions formalizing the idea of indistinguishability of system states. In this paper, we investigate the relation between two behavioural equivalences: the algebraic observational equivalence in the framework of observational algebras with many hidden sorts and automata bisimulation. For that purpose, we propose a transformation of an observational algebra into an infinite deterministic automaton. Consequently, we obtain a subclass of deterministic automata, equivalent to (infinite) Mealy automata, which we call Observational Algebra Automata (OAA). We use a categorical setting to show the equivalence between bisimulation on OAA and algebraic observational equivalence. Therefore we extend the hidden algebras result concerning observational equivalence and bisimulation coincidence to the non-monadic case.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Asperti, A., Longo, G.: Categories, types, and structures: an introduction to category theory for the working computer scientist. MIT Press, Cambridge (1991)

    MATH  Google Scholar 

  2. Bernot, G., Bidoit, M., Knapik, T.: Behavioural Approaches to Algebraic Specifications: A Comparative Study. Acta Inf. 31(7), 651–671 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bidoit, M., Hennicker, R.: Constructor-Based Observational Logic. Journal of Logic and Algebraic Programming 67(1-2), 3–51 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bidoit, M., Hennicker, R., Kurz, A.: Observational logic, constructor-based logic, and their duality. Theoretical Computer Science 298(3), 471–501 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer Programming 25(2-3), 149–186 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  6. Buchholz, P.: Bisimulation relations for weighted automata. Theoretical Computer Science 393(1-3), 109–123 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  7. Caucal, D.: Bisimulation of Context-Free Grammars and of Pushdown Automata. CSLI Lecture Notes 53, 85–106 (1995)

    MathSciNet  Google Scholar 

  8. Diaconescu, R., Futatsugi, K.: Behavioural Coherence in Object-Oriented Algebraic Specification. In: Calude, C.S., Stefanescu, G. (eds.) Journal of Universal Computer Science, vol. 6(1), pp. 74–96 (2000)

    Google Scholar 

  9. Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification I. Springer, New Work (1985)

    Google Scholar 

  10. Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  11. Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  13. Jacobs, B.: Objects and classes, co-algebraically, Object orientation with parallelism and persistence. Kluwer Academic Publishers, Norwell (1996)

    Google Scholar 

  14. Joyal, A., Nielsen, M., Winskel, G.: Bisimulation and open maps. In: LICS: IEEE Symposium on Logic in Computer Science, Montreal, Canada, pp. 418–427 (2003)

    Google Scholar 

  15. Kumar, R., Zhou, C., Basu, S.: Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata with Variables. In: Proc. of 2006 American Control Conference, Minneapolis, MN, pp. 6057–6062 (2006)

    Google Scholar 

  16. Lasota, S.: Open maps as a bridge between algebraic observational equivalence and bisimilarity. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 285–299. Springer, Heidelberg (1998)

    Google Scholar 

  17. Malcolm, G.: Behavioural Equivalence, Bisimulation, and Minimal Realisation. In: Selected papers from the 11th Workshop on Specification of Abstract Data Types, vol. 1130(3), pp. 359–378. Springer, Heidelberg (1996)

    Google Scholar 

  18. Mealy, G.H.: A Method to Synthesizing Sequential Circuits. Bell Systems Technical Journal 34 (1955)

    Google Scholar 

  19. Milner, R.: A Calculus of Communicating Systems. Springer, Secaucus (1982)

    Google Scholar 

  20. Milner, R.: Communicating and mobile systems: the π-calculus. Cambridge University Press, New York (1999)

    Google Scholar 

  21. Nivela, M.P., Orejas, F.: Initial behavior semantics for algebraic specifications. In: Recent Trends in Data Type Specification, pp. 184–207. Springer, Heidelberg (1988)

    Google Scholar 

  22. Reichel, H.: Behavioural equivalence — a unifying concept for initial and final specification methods. In: Proc. of the 3rd. Hungarian Computer Science Conference, Akadémia kiadó, pp. 27–39 (1981)

    Google Scholar 

  23. Reichel, H.: Initial computability, algebraic specifications, and partial algebras. Oxford University Press Inc., New York (1987)

    MATH  Google Scholar 

  24. Rosu, G., Goguen, J.: Hidden Congruent Deduction. In: Selected Papers from Automated Deduction in Classical and Non-Classical Logics, pp. 251–266. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  25. Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1), 3–80 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  26. Rutten, J.J.M.M.: A calculus of transition systems (towards universal coalgebra), Thechnical report, Centrum voor Wiskunde en Informatica (CWI), Amsterdam, The Netherlands (1995)

    Google Scholar 

  27. Rutten, J.J.M.M.: Coalgebra, concurrency, and control, Thechnical report, Centrum voor Wiskunde en Informatica (CWI), Amsterdam, The Netherlands (1999)

    Google Scholar 

  28. Sannella, D., Wirsing, M.: A Kernel Language for Algebraic Specification and Implementation - Extended Abstract. In: The Proc. of the 1983 International FCT-Conference on Fundamentals of Computation Theory, pp. 413–427. Springer, Heidelberg (1983)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIP2, Faculté des Sciences de Tunis,  

    Mouhebeddine Berrima

  2. LIP2, Institut National des Sciences Appliquées et de Technologie, Tunis

    Narjes Ben Rajeb

Authors
  1. Mouhebeddine Berrima
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Narjes Ben Rajeb
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Computer Science, University of Western Ontario, N6A 5B7, London, ON, Canada

    Yuan Gao , Hanlin Lu , Shinnosuke Seki  & Sheng Yu , ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Berrima, M., Ben Rajeb, N. (2010). Linking Algebraic Observational Equivalence and Bisimulation. In: Gao, Y., Lu, H., Seki, S., Yu, S. (eds) Developments in Language Theory. DLT 2010. Lecture Notes in Computer Science, vol 6224. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14455-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14455-4_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14454-7

  • Online ISBN: 978-3-642-14455-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation