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
Volume6014 LNCS
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)03029743
ISSN (Electronic)16113349

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

Fingerprint

Covering Problem
Transition Systems
Mobile Systems
Terminate
Fragment
Calculus
Class

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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. (Vol. 6014 LNCS, 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

Forward analysis of depth-bounded processes. / Wies, Thomas; Zufferey, Damien; Henzinger, Thomas A.

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.. Vol. 6014 LNCS 2010. p. 94-108 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6014 LNCS).

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

Wies, T, Zufferey, D & Henzinger, TA 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.. vol. 6014 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6014 LNCS, pp. 94-108, 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, Paphos, Cyprus, 3/20/10. https://doi.org/10.1007/978-3-642-12032-9_8
Wies T, Zufferey D, Henzinger TA. 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.. Vol. 6014 LNCS. 2010. p. 94-108. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-12032-9_8
Wies, Thomas ; Zufferey, Damien ; Henzinger, Thomas A. / Forward analysis of depth-bounded processes. 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.. Vol. 6014 LNCS 2010. pp. 94-108 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{580d121806bf453c8b97bc7de196c9db,
title = "Forward analysis of depth-bounded processes",
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.",
author = "Thomas Wies and Damien Zufferey and Henzinger, {Thomas A.}",
year = "2010",
doi = "10.1007/978-3-642-12032-9_8",
language = "English (US)",
isbn = "3642120318",
volume = "6014 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "94--108",
booktitle = "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.",

}

TY - GEN

T1 - Forward analysis of depth-bounded processes

AU - Wies, Thomas

AU - Zufferey, Damien

AU - Henzinger, Thomas A.

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

SN - 3642120318

SN - 9783642120312

VL - 6014 LNCS

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.

ER -