Abstract
We present a formal model for multicast network protocols working on arbitrary tree structures. We give sufficient conditions under which correctness of the protocol for all structures reduces to correctness for the structures with at most one layer of internal nodes. If additional conditions hold, we can reduce further to correctness for one single structure. All these results can be applied to (an abstract version of) the Pragmatic General Multicast protocol.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bérard, B., Bouyer, P. and Petit, A. Analysing the PGM protocol with UPPAAL. In: 2nd Workshop on Real-Time Tools. Dep. Information Technology, Uppsala Univ., 2002, Tech. Report 2002-025.
Browne, M. C., Clarke, E. and Grumberg, O. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59: 115–131, 1988.
Bouajjani, A. and Touili, T. Extrapolating tree transformations. In: Proc. 14th Intl. Conf. on Computer Aided Verification. 2002, LNCS 2404.
Esparza, J. and Maidl, M. Simple representative instantiations for multicast protocols, 2002. Available at http://www.dcs.ed.ac.uk/monika.
Emerson, E. A. and Namjoshi, K. S. Reasoning about rings. In: Proc. 22th ACM Conf. on Principles of Programming Languages. 1995.
Grumberg, O. and Long, D. E. Model checking and modular verification. TOPLAS, 16(3): 843–871, 1994.
Lamport, L. What good is temporal logic? In: Proc. IFIP 9th World Computer Congress. 1983.
Maidl, M. Simple representative instantiations for the PGM protocol, 2002. Available at http://www.dcs.ed.ac.uk/monika.
Papadopoulos, C., Parulkar, G. and Varghese, G. LMS: A router assisted scheme for reliable multicast. To appear in: IEEE/ACM Transactions on Networking.
Peled, D. and Wilke, T. Stutter-invariant temporal properties are expressible without the next-operator. Information Processing Letters, 63: 243–246, 1997.
Speakman, T. et al. PGM reliable transport protocol specification, 2000. RFC 3208 (experimental) of the IETF. Available at: http://www.ietf.org/rfc.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Esparza, J., Maidl, M. (2003). Simple Representative Instantiations for Multicast Protocols. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_10
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive