Forward Analysis of Depth-Bounded Processes

Depth-bounded processes form the most expressive known fragment of the π-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.

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: Thomas Wies, Damien Zufferey, Thomas A. Henzinger
• Keywords: Applied Computing, Depth-bounded Processes, Forward Algorithm Terminates, Forward Algorithms, FOSSACS 2010