Finitary Observations in Regular Algebras
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.
KeywordsBehavioural Property Observational Indistinguishability Regular Term Regular Algebra Approximation Chain
Unable to display preview. Download preview PDF.
- 2.M. Bidoit, A. Tarlecki: Regular algebras: a framework for observational specifications with recursive definitions. Report LIENS-95-12, ENS, 1995. 402, 404Google Scholar
- 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.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
- 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
- 11.J. Tiuryn: Fixed-points and algebras with infinitely long expressions. Part I. Regular algebras. Fundamenta Informaticae 2(1978), 102–128. 402Google Scholar