Abstract
We show that any regular set of basic MSCs can be implemented by a deadlock-free communicating finite-state machine with local termination: Processes stop in local dead-states independently from the contents of channels and the local states of other processes. We present a self-contained, direct, and relatively simple construction based on a new notion called context MSC.
Supported by the ANR project SOAPDC.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. TCS 331, 97–114 (2005)
Baudru, N., Morin, R.: Safe Implementability of Regular Message Sequence Charts Specifications. In: Proc. of the ACIS 4th Int. Conf. SNDP, pp. 210–217 (2003)
Bollig, B., Leucker, M.: Message-passing automata are expressively equivalent to EMSO logic. TCS 358, 150–172 (2006)
Bracho, F., Droste, M., Kuske, D.: Representations of computations in concurrent automata by dependence orders. TCS 174, 67–96 (1997)
Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific (1995)
Droste, M.: Recognizable languages in concurrency monoids. TCS 150, 77–109 (1995)
Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. I&C 204, 920–956 (2006)
Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-State High-Level MSCs: Model- Checking and Realizability. Journal of Computer and System Sciences 72, 617–647 (2006)
Gunter, E.L., Muscholl, A., Peled, D.: Compositional message sequence charts. Intern. Journal on Software Tools for Technology Transfer 5(1), 78–89 (2003)
Henriksen, J.G., Mukund, M., Narayan Kumar, K., Sohoni, M., Thiagarajan, P.S.: A Theory of Regular MSC Languages. I&C 202, 1–38 (2005)
Kuske, D.: Regular sets of infinite message sequence charts. I&C 187, 80–109 (2003)
Mukund, M., Narayan Kumar, K., Sohoni, M.: Bounded time-stamping in message-passing systems. TCS 290, 221–239 (2003)
Zielonka, W.: Safe executions of recognizable trace languages by asynchronous automata. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 278–289. Springer, Heidelberg (1989)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baudru, N., Morin, R. (2007). Synthesis of Safe Message-Passing Systems. In: Arvind, V., Prasad, S. (eds) FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2007. Lecture Notes in Computer Science, vol 4855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77050-3_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-77050-3_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77049-7
Online ISBN: 978-3-540-77050-3
eBook Packages: Computer ScienceComputer Science (R0)