Abstract
A communicating system is \(k\)-synchronizable if all of the message sequence charts representing the executions can be divided into slices of k sends followed by k receptions. It was previously shown that, for a fixed given k, one could decide whether a communicating system is \(k\)-synchronizable. This result is interesting because the reachability problem can be solved for \(k\)-synchronizable systems. However, the decision procedure assumes that the bound k is fixed. In this paper we improve this result and show that it is possible to decide if such a bound k exists.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91–101 (1996)
Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. 656, 60–75 (2016)
Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 372–391. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_23
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 93–106. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04420-5_10
Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: 1988 Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, pp. 44–65. ACM (1988)
Di Giusto, C., Laversa, L., Lozes, E.: On the k-synchronizability of systems. In: Goubault-Larrecq, J., König, B. (eds.) FoSSaCS 2020. LNCS, vol. 12077, pp. 157–176. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45231-5_9
Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)
Finkel, A., Lozes, É.: Synchronizability of communicating finite state machines is not decidable. In: ICALP 2017, pp. 122:1–122:14 (2017)
Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1–3), 147–167 (2007)
von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3(POPL), 59:1–59:30 (2019)
Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR 2018, vol. 118, pp. 21:1–21:17 (2018)
La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299–314. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_21
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Di Giusto, C., Laversa, L., Lozes, E. (2021). Guessing the Buffer Bound for k-Synchronizability. In: Maneth, S. (eds) Implementation and Application of Automata. CIAA 2021. Lecture Notes in Computer Science(), vol 12803. Springer, Cham. https://doi.org/10.1007/978-3-030-79121-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-79121-6_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-79120-9
Online ISBN: 978-3-030-79121-6
eBook Packages: Computer ScienceComputer Science (R0)