×

zbMATH — the first resource for mathematics

Quantales, finite observations and strong bisimulation. (English) Zbl 0972.68122
Summary: It has often been claimed that bisimulation makes distinctions that cannot be observed in practice. Abramsky and Vickers proposed an algebraic framework based on quantales for describing observations on concurrent processes without hidden transitions and used it in order to provide an “observational explanation” of several process equivalences, ranging from Hoare trace equivalence to ready-simulation. We follow their approach and argue that (strong) bisimulation can be explained in the same way, at least in the case of “image-computable” labelled transition systems.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abramsky, S., Domain theory and the logic of observable properties, ph.D. thesis, (1987), Queen Mary College University of London
[2] Abramsky, S., Observation equivalence as a testing equivalence, Theoret. comput. sci., 53, 225-241, (1987) · Zbl 0626.68016
[3] Abramsky, S., A domain equation for bisimulation, Inform. comput., 92, 161-218, (1991) · Zbl 0718.68057
[4] Abramsky, S., Domain theory in logical form, Ann. pure appl. logic, 51, 1-77, (1991) · Zbl 0737.03006
[5] Abramsky, S.; Vickers, S., Quantales, observational logic and process semantics, Math. struct. comput. sci., 3, 161-227, (1993) · Zbl 0823.06011
[6] Arnold, A., Verification and comparison of transition systems, (), 121-135
[7] B. Bloom, S. Istrail, A.R. Meyer, Bisimulation can’t be traced (preliminary report), in: Conf. Record of the 15th ACM Symp. on Principles of Programming Languages, 1988, pp. 229-239. · Zbl 0886.68027
[8] Bloom, B.; Istrail, S.; Meyer, A.R., Bisimulation can’t be traced, J. ACM, 42, 232-268, (1995) · Zbl 0886.68027
[9] Davey, B.; Priestley, H., Introduction to lattices and order, (1990), Cambridge University Press Cambridge · Zbl 0701.06001
[10] van Glabbeek, R.J., The linear time — branching time spectrum, (), 278-297
[11] van Glabbeek, R.J., The linear time-branching time spectrum II; the semantics of sequential systems with silent moves, tech. report, Stanford university, 1993. extended abstract, (), 66-81
[12] van Glabbeek, R.J.; Vaandrager, F., Petri net models for algebraic theories of concurrency, (), 224-242
[13] van Glabbeek, R.J.; Weijland, P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 555-600, (1996) · Zbl 0882.68085
[14] Groote, J.F., Transition system specifications with negative premises, Theoret. comput. sci., 118, 263-299, (1993) · Zbl 0778.68057
[15] Groote, J.F.; Vaandrager, F., Structured operational semantics and bisimulation as a congruence, Inform. comput., 100, 202-260, (1992) · Zbl 0752.68053
[16] Hennessy, M., Algebraic theory of processes, (1988), The MIT Press Cambridge, MA · Zbl 0744.68047
[17] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 137-161, (1985) · Zbl 0629.68021
[18] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall New York · Zbl 0637.68007
[19] Johnstone, P., Stone spaces, (1982), Cambridge University Press Cambridge · Zbl 0499.54001
[20] A. Joyal, M. Tierney, An Extension of the Galois Theory of Grothendieck, Memoirs of the AMS, Vol. 309, American Mathematical Society, Providence, RI, 1984. · Zbl 0541.18002
[21] Larsen, K.G.; Skou, A., Bisimulation through probabilistic testing, Inform. comput., 94, 1-28, (1991) · Zbl 0756.68035
[22] Mac Lane, S., Categories for the working Mathematician, (1971), Springer New York · Zbl 0232.18001
[23] Milner, R., A modal characterisation of observable machine behaviour, (), 25-34 · Zbl 0474.68074
[24] Milner, R., Communication and concurrency, (1989), Prentice-Hall New York · Zbl 0683.68008
[25] C. Mulvey, & Rend. Circ. Mat. Palermo (2) Suppl. 12 (1986) 99-104.
[26] de Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. comput. sci., 34, 83-133, (1984) · Zbl 0985.68518
[27] Park, D.M.R., Concurrency and automata on infinite sequences, (), 167-183
[28] Phillips, I., Refusal testing, Theoret. comput. sci., 50, 241-284, (1987) · Zbl 0626.68011
[29] P. Resende, Observational system specification, in: R. Wieringa, R. Feenstra (Eds.), Selected Papers of ISCORE’94, World Scientific, Singapore, 1995, pp. 135-151. Revised version available by ftp at
[30] P. Resende, Tropological systems and observational logic in concurrency and specification, Ph.D. Thesis, Universidade Técnica de Lisboa, 1997.
[31] Resende, P., Modular specification of concurrent systems with observational logic, (), 307-321
[32] Rosenthal, K., Quantales and their applications, (1990), Longman Scientific & Technical London · Zbl 0703.06007
[33] Vickers, S., Topology via logic, (1989), Cambridge University Press Cambridge · Zbl 0668.54001
[34] G. Winskel, M. Nielsen, Models for concurrency, in: Handbook of Logic in Computer Science, Vol. 4, Oxford University Press, Oxford, 1995. A draft appeared as BRICS Report RS-94-12, 1994.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.