TY - GEN
T1 - Forward analysis of depth-bounded processes
AU - Wies, Thomas
AU - Zufferey, Damien
AU - Henzinger, Thomas A.
N1 - Copyright:
Copyright 2010 Elsevier B.V., All rights reserved.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77951495561&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77951495561&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-12032-9_8
DO - 10.1007/978-3-642-12032-9_8
M3 - Conference contribution
AN - SCOPUS:77951495561
SN - 3642120318
SN - 9783642120312
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 94
EP - 108
BT - Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.
T2 - 13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010
Y2 - 20 March 2010 through 28 March 2010
ER -