Reachability for dynamic parametric processes

Anca Muscholl; Helmut Seidl; Igor Walukiewicz

doi:10.1007/978-3-319-52234-0_23

Reachability for dynamic parametric processes

Anca Muscholl, Helmut Seidl, Igor Walukiewicz

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

6 Scopus citations

Abstract

In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.

Original language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings
Editors	Ahmed Bouajjani, David Monniaux
Publisher	Springer Verlag
Pages	424-441
Number of pages	18
ISBN (Print)	9783319522333
DOIs	https://doi.org/10.1007/978-3-319-52234-0_23
State	Published - 2017
Event	18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 - Paris, France Duration: 15 Jan 2017 → 17 Jan 2017

Publication series

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

Conference

Conference	18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
Country/Territory	France
City	Paris
Period	15/01/17 → 17/01/17

Access to Document

10.1007/978-3-319-52234-0_23

Cite this

Muscholl, A., Seidl, H., & Walukiewicz, I. (2017). Reachability for dynamic parametric processes. In A. Bouajjani, & D. Monniaux (Eds.), Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings (pp. 424-441). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10145 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-52234-0_23

Muscholl, Anca ; Seidl, Helmut ; Walukiewicz, Igor. / Reachability for dynamic parametric processes. Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. editor / Ahmed Bouajjani ; David Monniaux. Springer Verlag, 2017. pp. 424-441 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6940990542b44fe5920ee20fb05920ef,

title = "Reachability for dynamic parametric processes",

abstract = "In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.",

author = "Anca Muscholl and Helmut Seidl and Igor Walukiewicz",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 ; Conference date: 15-01-2017 Through 17-01-2017",

year = "2017",

doi = "10.1007/978-3-319-52234-0_23",

language = "English",

isbn = "9783319522333",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "424--441",

editor = "Ahmed Bouajjani and David Monniaux",

booktitle = "Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings",

}

Muscholl, A, Seidl, H & Walukiewicz, I 2017, Reachability for dynamic parametric processes. in A Bouajjani & D Monniaux (eds), Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10145 LNCS, Springer Verlag, pp. 424-441, 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, Paris, France, 15/01/17. https://doi.org/10.1007/978-3-319-52234-0_23

Reachability for dynamic parametric processes. / Muscholl, Anca; Seidl, Helmut; Walukiewicz, Igor.
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. ed. / Ahmed Bouajjani; David Monniaux. Springer Verlag, 2017. p. 424-441 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10145 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Reachability for dynamic parametric processes

AU - Muscholl, Anca

AU - Seidl, Helmut

AU - Walukiewicz, Igor

N1 - Publisher Copyright: © Springer International Publishing AG 2017.

PY - 2017

Y1 - 2017

N2 - In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.

AB - In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.

UR - http://www.scopus.com/inward/record.url?scp=85010669564&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-52234-0_23

DO - 10.1007/978-3-319-52234-0_23

M3 - Conference contribution

AN - SCOPUS:85010669564

SN - 9783319522333

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 424

EP - 441

BT - Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings

A2 - Bouajjani, Ahmed

A2 - Monniaux, David

PB - Springer Verlag

T2 - 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017

Y2 - 15 January 2017 through 17 January 2017

ER -

Muscholl A, Seidl H, Walukiewicz I. Reachability for dynamic parametric processes. In Bouajjani A, Monniaux D, editors, Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Springer Verlag. 2017. p. 424-441. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-52234-0_23

Reachability for dynamic parametric processes

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this