Forward analysis of depth-bounded processes. (English) Zbl 1284.68419

Wies, Thomas; Zufferey, Damien; Henzinger, Thomas A.

Ong, Luke (ed.), Foundations of software science and computational structures. 13th international conference, FOSSACS 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12031-2/pbk). Lecture Notes in Computer Science 6014, 94-108 (2010).

Summary: Depth-bounded processes form the most expressive known fragment of the \(\pi \)-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems.
For the entire collection see [Zbl 1185.68013].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)