Advertisement

Finitary Observations in Regular Algebras

  • Slawomir Lasota
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1963)

Abstract

We investigate regular algebras, admitting infinitary regular terms interpreted as least upper bounds of suitable approximation chains. We prove that finitary observable contexts are suffcient for observational indistinguishability in a regular algebra. Moreover, assumed all observable sorts to be essentially flat, observational equivalence is also completely characterized by finitary contexts. As a corollary, methods of proving behavioural properties and observational equivalence of standard algebras can be reused in the setting of regular algebras.

Keywords

Behavioural Property Observational Indistinguishability Regular Term Regular Algebra Approximation Chain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Bidoit, R. Hennicker: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science 165(1): 3–55, 1996. 403, 406zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    M. Bidoit, A. Tarlecki: Regular algebras: a framework for observational specifications with recursive definitions. Report LIENS-95-12, ENS, 1995. 402, 404Google Scholar
  3. 3.
    I. Guessarian, F. Parisi-Presicce: Iterative vs. regular factor algebras. SIGACT News 15(2), 32–44, 1983. 402CrossRefGoogle Scholar
  4. 4.
    R. Hennicker: Context induction: A proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 3(4):326–345, 1991. 403, 406zbMATHCrossRefGoogle Scholar
  5. 5.
    S. Lasota: Algebraic observational equivalence and open-maps bisimilarity. Ph.D. Thesis in Institute of Informatics of Warsaw University, March 2000. Accessible at http://www.mimuw.edu.pl/sl/work/phd.ps.gz. 403, 404, 405, 407
  6. 6.
    S. Lasota: Behavioural constructor implementation for regular algebras. To appear in Proc. 7 th International Conference on Logic for Programming and Automated Reasoning LPAR’2000, Springer-Verlag LNAI series. 403Google Scholar
  7. 7.
    D. Sannella, A. Tarlecki: Towards formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25:233–281, 1988. 402zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    D. Sannella, A. Tarlecki: Essential Concepts of Algebraic Specification and Program Development. Formal Aspects of Computing 9:229–269, 1997. 402, 403zbMATHCrossRefGoogle Scholar
  9. 9.
    O. Schoett: Data abstraction and correctness of modular programming. Ph.D. thesis, CST-42-87, Department of Computer Science, University of Edinburgh, 1987. 403, 407, 409Google Scholar
  10. 10.
    A. Tarlecki, M. Wirsing: Continuous abstract data types. Fundamenta Informaticae 9(1986), 95–126. 402zbMATHMathSciNetGoogle Scholar
  11. 11.
    J. Tiuryn: Fixed-points and algebras with infinitely long expressions. Part I. Regular algebras. Fundamenta Informaticae 2(1978), 102–128. 402Google Scholar
  12. 12.
    J. Tiuryn: Fixed-points and algebras with infinitely long expressions. Part II. Muclones of regular algebras. Fundamenta Informaticae 2(1979), 317–336. 402zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Slawomir Lasota
    • 1
  1. 1.Institute of InformaticsWarsaw UniversityWarszawaPoland

Personalised recommendations