Abstract
We consider the problem of reasoning about message based systems in finite state environments. Two notions of finite state environments are discussed: bounded buffers and implicit buffers. The former notion is standard, whereby the sender gets blocked when the buffer is full. In the latter, the sender proceeds as if the buffer were unbounded, but the system has bounded memory and hence “forgets” some of the messages. The computations of such systems are given as communication diagrams. We present a linear time temporal logic which is interpreted on n-agent diagrams. The formulas of the logic specify local properties using standard temporal modalities and a basic communication modality. The satisfiability and model checking problems for the logic are shown to be decidable for both buffered products and implicit products. An example of system specification in the logic is discussed.
We thank Kamal Lodaya and the reviewers for helpful discussions, and Laura Semini for bringing to our attention [MS99] on which Section 5 is based.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R. and Yannakakis, M., “Model checking of message sequence charts”, Springer LNCS 1664, 1999, 114–129.
Ciancarini, P., Nierstrasz, O. and Tolksdorf, R., “A case study in co-ordination: conference management on the internet”, Available at: http://malvasia.di.fct.unl.pt/activity/coordina/working/case-studies.
Huhn, M., Niebert, P. and Wallner, F., “Model checking logics for communicating sequential agents”, Springer LNCS 1578, 1999, 227–242.
Lamport, L., “Time, clocks, and the ordering of events in a distributed system”, Comm. ACM21(7), 1978, 558–565.
Lamport, L. and Lynch, N., “Distributed computing: Models and methods” in J. van Leeuwen (ed.), North-Holland Handbook of Theoretical Computer Science, Volume B, 1990, 1157–1199.
Lodaya, K., Ramanujam, R. and Thiagarajan, P.S., “Temporal logics for communicating sequential agents”, Int. Journal of FOCS 3(2), 1992, 117–159.
Lynch, N., Distributed algorithms, Morgan Kaufmann, 1996.
Manna, Z. and Pnueli, A., Temporal verification of reactive systems, vol 1: Specification, vol 2: Verification, Springer, 1995.
Montangero, C., and Semini, L., “Composing specifications for coordination”, Springer LNCS 1594, 1999.
Ramanujam, R., “Locally linear time temporal logic”, Proc. LICS, 1996, 118–127.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meenakshi, B., Ramanujam, R. (2000). Reasoning about Message Passing in Finite State Environments. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_41
Download citation
DOI: https://doi.org/10.1007/3-540-45022-X_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67715-4
Online ISBN: 978-3-540-45022-1
eBook Packages: Springer Book Archive