Abstract
In this extended abstract, we briefly recall the abstract (categorical) notion of bisimulation from open morphisms, as introduced by Joyal, Nielsen and Winskel. The approach is applicable across a wide range of models of computation, and any such bisimulation comes automatically with characteristic logics and games, which in their general formulations treat the future and the past (of computations) on an equal footing. This raises a number of questions concerning properties of such logics and games for concrete well known models from concurrency theory, in particular questions on the power of reasoning about the past.
Preview
Unable to display preview. Download preview PDF.
References
Bednarczyk, M., Categories of Asynchronous Systems. Ph.D. Thesis in Computer Science, Univ. of Sussex, Report No. 1/88, 1988.
Cattani, G.L., Fiore, M., Winskel,G., A Theory of Recursive Domains with Applications to Concurrency. To appear in Proceedings of LICS'98.
De Nicola, R., Montanari, U., and Vaandrager, F., Back and Forth Bisimulations. Proceedings of CONCUR'90, Springer Lecture Notes in Computer Science 458, pp. 152–165, 1990.
Hoare, C.A.R., Communicating Sequential Processes. Prentice Hall,1985.
Hune, T., Nielsen, M., Timed Bisimulation and Open Maps. In this volume.
Joyal, A., Nielsen, M. and Winskell, G., Bisimulation from Open Maps. Information and Computation, 127, no. 2, pp. 164–185, 1996.
Jurdzinski, M., Nielsen, M., On the Power of Past Modalities. In preparation.
Keller, R.M., Formal Verification of Parallel Programs. CACM, 19(7), pp. 371–384, 1976.
Lichtenstein, O., Pnueli, A., and Zuck, L., The Glory of the Past. Springer Lecture Notes in Computer Science 193, pp. 196–218, 1985.
MacLane, S., and Moerdijk, I., Sheaves in geometry and logic: a first introduction to topos theory, Springer, 1992.
Mazurkiewicz, A., Basic notions of trace theory. In de Bakker, de Roever and Rozenberg (eds.), Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency, Springer Lecture Notes in Computer Science 354, pp. 285–363, 1988.
Milner,A.J.R.G., Communication and concurrency. Prentice Hall, 1989.
Nielsen, M., Plotkin, G. and Winskel, G., Petri nets, Event structures and Domains, part 1. Theoretical Computer Science 13, pp. 85–108, 1981.
Nielsen, M., Cheng, A., Observing Behaviour Categorically. Proc. of FST&TCS'15, Springer Lecture Notes in Computer Science 1026, pp. 263–278, 1995.
Nielsen, M., and Clausen, C., Bisimulations, Games, and Logic. Proc. of CONCUR'94, Springer Lecture Notes in Computer Science 836, pp. 385–400, 1994.
Nielsen, M., and Winskel, G., Petri nets and bisimulations. Theoretical Computer Science, 153, pp. 211–244, 1996.
Penczek, W., Kuiper, R., Traces and Logic. In The Book of Traces, eds. Diekert, V., Rozenberg, G., World Scientific, pp. 307–390, 1994.
Petri, C.A. Kommunikation mit Automaten. PhD thesis, Institut für Instrumentelle Mathematik, Bonn, Germany, 1962.
Pratt, V.R., Modelling concurrency with partial orders. International Journal of Parallel Programming, 15(1), pp. 33–71, 1986.
Shields, M.W., Concurrent Machines, Comput. J., 28, pp. 449–465, 1985.
Stirling, C., Games and Modal Mu-Calculus. Lecture Notes in Computer Science 1055, pp. 298 ff., 1996.
Thiagarajan, P.S., Elementary Net Systems. Springer Lecture Notes in Computer Science 254, pp. 26–59, 1986.
Vardi, M.Y., The Taming of the Converse: Reasoning about Two-way Computations. Springer Lecture Notes in Computer Science 193, pp. 413–424, 1985.
Winskel, G., Event structures. Springer Lecture Notes in Computer Science 255, pp. 325–392, 1987.
Winskel, G., and Nielsen, M., Models for concurrency. In the Handbook of Logic in Computer Science, vol. IV, ed. Abramsky, Gabbay and Maibaum, Oxford University Press, pp. 1–148, 1995.
Winskel, G., A Presheaf Semantics of Value-Passing Processes. In the proc. of CONCUR'96, Springer Lecture Notes in Computer Science 1119, pp. 98–114, 1996.
Winskel, G., and Nielsen, M., Presheaves as Transition Systems, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 29, pp. 129–140, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielsen, M. (1998). Reasoning about the past. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055761
Download citation
DOI: https://doi.org/10.1007/BFb0055761
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive