Abstract
Broadcast protocols are systems composed of a finite but arbitrarily large number of processes that communicate by rendezvous (two processes exchange a message) or by broadcast (a process sends a message to all other processes). The paper describes an optimized algorithm for the automatic verification of safety properties in broadcast protocols. The algorithm checks whether a property holds for any number of processes.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. 14th IEEE Int. Symp. on Logic in Computer Science, 1998.
A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Technical Report LSV-98-4, Laboratoire Spécification et Vérification, Ecole Normale Supérieure de Cachan. April 1998. To appear in Theoretical Computer Science, 1999.
M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-completeness. Freeman, 1978.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech:a Model Checker for Hybrid Systems. In Orna Grumberg, editor, Proc. 9th Conf. on Computer Aided Verification (CAV’97), LNCS 1254, pp. 460–463. Springer-Verlag, 1997.
M. Kindahl. Verification of Infinite State Systems: Decision Problems and Efficient Algorithms. Ph.D. thesis, Department of Computer Systems, Uppsala University, June 1999. Available as report DoCS 110.
R. M. Karp and R. E. Miller. Parallel Program Schemata. Journal of Computer and System Sciences, 3, pp. 147–195, 1969.
K. McAloon. Petri Nets and Large Finite Sets. Theoretical Computer Science 32, pp. 173–183, 1984.
D. Srivistava. Subsumption and indexing in constraint query languages with linear arithmetic constraints. In 2nd Int. Symp. on Artificial Intelligence and Mathematics, Fort Lauderdale, 1992.
E. Teruel. Structure Theory ofWeighte d Place/Transition Net Systems: The Equal Conflict Hiatus. Ph.D. Thesis, University of Zaragoza, 1994.
M. Y. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of Programs. Journal ofComputer and System Sciences. 32(2), pp. 183–221, April, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delzanno, G., Podelski, A., Esparza, J. (1999). Constraint-Based Analysis of Broadcast Protocols. In: Flum, J., Rodriguez-Artalejo, M. (eds) Computer Science Logic. CSL 1999. Lecture Notes in Computer Science, vol 1683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48168-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-48168-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66536-6
Online ISBN: 978-3-540-48168-3
eBook Packages: Springer Book Archive