Abstract
Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. This paper identifies a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to the class of systems in which an agent’s state evolves continuously over time. The proof technique has been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm.
The work is funded in part by the Caltech Information Science and Technology Center and AFOSR MURI FA9550-06-1-0303.
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
Tempo toolset, version 0.2.2 beta (January 2008), http://www.veromodo.com/
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Archer, M., Heitmeyer, C., Sims, S.: TAME: A PVS interface to simplify proofs for automata models. In: Proceedings of UITP 1998 (July 1998)
Archer, M., Lim, H., Lynch, N., Mitra, S., Umeno, S.: Specifying and proving properties of timed I/O automata using Tempo. Design Aut. for Emb. Sys (to appear, 2008)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL in 1995. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 431–434. Springer, Heidelberg (1996)
Blondel, V., Hendrickx, J., Olshevsky, A., Tsitsiklis, J.: Convergence in multiagent coordination consensus and flocking. In: CDC-ECC, pp. 2996–3000 (2005)
Blondel, V., Hendrickx, J., Olshevsky, A., Tsitsiklis, J.: Formations of mobile agents with message loss and delay (preprint, 2007), http://www.ist.caltech.edu/~mitras/research/2008/asynchcoord.pdf
Chatterjee, S., Seneta, E.: Towards consensus: some convergence theorems on repeated averaging. J. Applied Probability 14(1), 89–97 (1977)
Clavaski, S., Chaves, M., Day, R., Nag, P., Williams, A., Zhang, W.: Vehicle networks: achieving regular formation. In: ACC (2003)
Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288–323 (1988)
Hendriks, M.: Model checking the time to reach agreement. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 98–111. Springer, Heidelberg (2005)
Kaynar, D., Lynch, N., Mitra, S., Garland, S.: TIOA Language. MIT Computer Science and Artificial Intelligence Laboratory, Cambridge (2005)
Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I/O Automata. Synthesis Lectures on CS. Morgan Claypool (November 2005)
Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)
Lim, H., Kaynar, D., Lynch, N., Mitra, S.: Translating timed I/O automata specifications for theorem proving in PVS. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 17–31. Springer, Heidelberg (2005)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)
Mitra, S., Chandy, K.M.: A formalized theory for verifying stability and convergence of automata in pvs. In: TPHOLs 2008 (to appear, 2008)
Olfati-Saber, R., Fax, J., Murray, R.: Consensus and cooperation in networked multi-agent systems. Proc. of the IEEE 95(1), 215–233 (2007)
Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)
Tsitsiklis, J.N.: On the stability of asynchronous iterative processes. Theory of Computing Systems 20(1), 137–153 (1987)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chandy, K.M., Mitra, S., Pilotto, C. (2008). Convergence Verification: From Shared Memory to Partially Synchronous Systems. In: Cassez, F., Jard, C. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2008. Lecture Notes in Computer Science, vol 5215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85778-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-85778-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85777-8
Online ISBN: 978-3-540-85778-5
eBook Packages: Computer ScienceComputer Science (R0)