Abstract
Many recent systems tackling Distributed Constraint Satisfaction Problems (DCSPs) lack a theoretically founded specification and safety or liveness property proofs. This may be due to the difficulty of modeling and verifying concurrently running threads and their interaction. In this article we will briefly sketch an approach to the modeling and verification of concurrent algorithms tailored to DCSP solving and based on algebraic Petri nets. We will present a realistic case study on distributed agreement finding and state according termination and consistency properties.
An extention of this paper can be found in [1]. Many thanks to Wolfgang Reisig, Armin Wolf and Ulrich Geske for fruitful discussions on this paper.
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
M. Hannebauer. Their problems are my problems — The transition between internal and external conflict. In Conflicting Agents: Conflict Management in Multi-Agent Systems. Kluwer, 2000.
T. Nguyen, Y. Deville. A distributed arc-consistency algorithm. Science of Computer Programming, 30(1–2):227–250, 1998.
W. Reisig. Elements of Distributed Algorithms — Modeling and Analysis with Petri Nets. Springer, 1998.
G. Solotorevsky, E. Gudes, A. Meisels. Modeling and solving distributed constraint satisfaction problems (DCSPs). In Proc. of CP-96, 1996.
M. Yokoo, E. Durfee, T. Ishida, K. Kuwabara. The distributed constraint satisfaction problem: Formalization and algorithms. IEEE Trans. KDE, 10(5), 1998.
Y. Zhang, A. Mackworth. Parallel and distributed algorithms for finite constraint satisfaction problems. In Proc. of the IEEE-Symposium on Parallel and Distributed Processing, pages 394–397, 1991.
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
Hannebauer, M. (2000). How to Model and Verify Concurrent Algorithms for Distributed CSPs. In: Dechter, R. (eds) Principles and Practice of Constraint Programming – CP 2000. CP 2000. Lecture Notes in Computer Science, vol 1894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45349-0_40
Download citation
DOI: https://doi.org/10.1007/3-540-45349-0_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41053-9
Online ISBN: 978-3-540-45349-9
eBook Packages: Springer Book Archive