Abstract
We propose a general approach to define behavioural preorders over process terms by considering the pre-congruences induced by three basic observables. These observables provide information about the initial communication capabilities of processes and about their possibility of engaging in an infinite internal chattering. We show that some of the observables-based pre-congruences do correspond to behavioral preorders long studied in the literature. The coincidence proofs shed light on the differences between the must preorder of De Nicola and Hennessy and the fair/should preorder of Cleaveland and Natarajan and of Brinksma, Rensink and Vogler, and on the rôle played in their definition by tests for internal chattering.
Work partially supported by EEC: HCM project EXPRESS, by CNR project “Specifica ad alto livello e verifica formale di sistemi digitali” and by Istituto di Elaborazione delPInformazione CNR, Pisa.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky. The lazy lambda calculus. Research Topics in Functional Programming, David Turner, ed., Addison-Wesley, 1990.
B. Bloom, S. Istrail, A.R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232–268, 1995.
E. Brinksma, A. Rensink, W. Vogler. Fair Testing. Proceedings of CONCUR'95, LNCS 962, pages 313–327, Springer, 1995.
E. Brinksma, A. Rensink, W. Vogler. Applications of Fair Testing. In R. Gotzhein and J. Bredereke, ed., Formal Description Techniques IX, Chapman & Hall, 1996.
S.D. Brookes, C.A.R. Hoare, A.W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, 1984.
R. de Nicola, M.C.B. Hennessy. Testing Equivalence for Processes. Theoretical Computers Science, 34:83–133, 1984.
R. De Nicola, M.C.B. Hennessy. CCS without τ's. Proceedings of TAPSOFT'87, LNCS 249, pages 138–152, Springer, 1987.
W. Ferreira. Semantic Theories for Concurrent ML. Ph.D. Thesis, University of Sussex, 1996.
C. Fournet, G. Gonthier, J.-L. Lévy, L. Maranget, D. Rémy. A Calculus of Mobile Agents. Proceedings of CONCUR'96, LNCS 1119, 1996.
M.C.B. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
M.C.B. Hennessy. Observing Processes. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer, 1989.
C. Laneve. May and Must Testing in the Join-Calculus. Technical Report UBLCS96-4, Università di Bologna, Dept. of Computer Science, Bologna, 1996.
M.G. Main. Trace, Failure and Testing Equivalences for Communicating Processes. Int. Journal of Parallel Programming, 16(5):383–400, 1987.
R. Milner. Communication and Concurrency. Prentice Hall International, 1989.
R. Milner, D. Sangiorgi. Barbed Bisimulation. Proceedings of ICALP'92, LNCS 623, Springer, 1992.
J.-H. Morris. Lambda Calculus Models of Programming Languages. Ph.D. Thesis, MIT, 1968.
V. Natarajan, R. Cleaveland. Divergence and Fair Testing. Proceedings of ICALP'95, LNCS 944, pages 648–659, Springer, 1995.
C.-H.L. Ong. Correspondence between operational and denotational semantics: the full abstraction problem for PCF. Handbook of Logic in Computer Science, vol.4, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, ed., Oxford Science Publ., 1995.
G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Aarhus University, Dept. of Computer Science, Aarhus, 1981.
J.H. Reppy. Concurrent ML: Design, application and semantics. Proceedings of Functional Programming, Concurrency, Simulation and Automata Reasoning, LNCS 693, pages 165–198, Springer, 1993.
W. Vogler. Failures Semantics and Deadlocking of Modular Petri Nets. Acta Informatica, 26:333–348, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boreale, M., de Nicola, R., Pugliese, R. (1997). Basic observables for processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds) Automata, Languages and Programming. ICALP 1997. Lecture Notes in Computer Science, vol 1256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63165-8_204
Download citation
DOI: https://doi.org/10.1007/3-540-63165-8_204
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63165-1
Online ISBN: 978-3-540-69194-5
eBook Packages: Springer Book Archive