Forward analysis of depth-bounded processes

Thomas Wies, Damien Zufferey, Thomas A. Henzinger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationFoundations 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.
Pages94-108
Number of pages15
DOIs
StatePublished - 2010
Event13th 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 - Paphos, Cyprus
Duration: Mar 20 2010Mar 28 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6014 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th 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
CountryCyprus
CityPaphos
Period3/20/103/28/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Forward analysis of depth-bounded processes'. Together they form a unique fingerprint.

  • Cite this

    Wies, T., Zufferey, D., & Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In 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. (pp. 94-108). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6014 LNCS). https://doi.org/10.1007/978-3-642-12032-9_8