Constrained Dynamic Tree Networks

Matthew Hague; Vincent Penelle

doi:10.1007/978-3-030-00250-3_4

Constrained Dynamic Tree Networks

Matthew Hague, Vincent Penelle

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

34 Downloads (Pure)

Abstract

We generalise Constrained Dynamic Pushdown Networks, introduced by Bouajjani et al, to Constrained Dynamic Tree Networks. In this model, we have trees of processes which may monitor their children. We allow the processes to be defined by any computation model for which the alternating reachability problem is decidable. We address the problem of symbolic reachability analysis for this model. More precisely, we consider the problem of computing an effective representation of their reachability sets using finite state automata. We show that backwards reachability sets starting from regular sets of configurations are always regular. We provide an algorithm for computing backwards reachability sets using tree automata.

Original language	English
Title of host publication	12th International Conference on Reachability Problems
Publisher	Springer International Publishing
Pages	45-58
Number of pages	14
ISBN (Electronic)	978-3-030-00250-3
ISBN (Print)	978-3-030-00249-7
DOIs	https://doi.org/10.1007/978-3-030-00250-3_4
Publication status	Published - 2018

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11123

Keywords

Model-checking
Dynamic Networks
Concurrency
Pushdown Systems
Alternation
Higher-order
Collapsible Pushdown Systems

Access to Document

10.1007/978-3-030-00250-3_4

Accepted ManuscriptAccepted author manuscript, 138 KB

Cite this

@inproceedings{2e5919355e5047c99666998fb6e05663,

title = "Constrained Dynamic Tree Networks",

abstract = "We generalise Constrained Dynamic Pushdown Networks, introduced by Bouajjani et al, to Constrained Dynamic Tree Networks. In this model, we have trees of processes which may monitor their children. We allow the processes to be defined by any computation model for which the alternating reachability problem is decidable. We address the problem of symbolic reachability analysis for this model. More precisely, we consider the problem of computing an effective representation of their reachability sets using finite state automata. We show that backwards reachability sets starting from regular sets of configurations are always regular. We provide an algorithm for computing backwards reachability sets using tree automata.",

keywords = "Model-checking, Dynamic Networks, Concurrency, Pushdown Systems, Alternation, Higher-order, Collapsible Pushdown Systems",

author = "Matthew Hague and Vincent Penelle",

year = "2018",

doi = "10.1007/978-3-030-00250-3_4",

language = "English",

isbn = "978-3-030-00249-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing",

pages = "45--58",

booktitle = "12th International Conference on Reachability Problems",

}

TY - GEN

T1 - Constrained Dynamic Tree Networks

AU - Hague, Matthew

AU - Penelle, Vincent

PY - 2018

Y1 - 2018

N2 - We generalise Constrained Dynamic Pushdown Networks, introduced by Bouajjani et al, to Constrained Dynamic Tree Networks. In this model, we have trees of processes which may monitor their children. We allow the processes to be defined by any computation model for which the alternating reachability problem is decidable. We address the problem of symbolic reachability analysis for this model. More precisely, we consider the problem of computing an effective representation of their reachability sets using finite state automata. We show that backwards reachability sets starting from regular sets of configurations are always regular. We provide an algorithm for computing backwards reachability sets using tree automata.

AB - We generalise Constrained Dynamic Pushdown Networks, introduced by Bouajjani et al, to Constrained Dynamic Tree Networks. In this model, we have trees of processes which may monitor their children. We allow the processes to be defined by any computation model for which the alternating reachability problem is decidable. We address the problem of symbolic reachability analysis for this model. More precisely, we consider the problem of computing an effective representation of their reachability sets using finite state automata. We show that backwards reachability sets starting from regular sets of configurations are always regular. We provide an algorithm for computing backwards reachability sets using tree automata.

KW - Model-checking

KW - Dynamic Networks

KW - Concurrency

KW - Pushdown Systems

KW - Alternation

KW - Higher-order

KW - Collapsible Pushdown Systems

UR - https://figshare.com/articles/main_pdf/6850508

U2 - 10.1007/978-3-030-00250-3_4

DO - 10.1007/978-3-030-00250-3_4

M3 - Conference contribution

SN - 978-3-030-00249-7

T3 - Lecture Notes in Computer Science

SP - 45

EP - 58

BT - 12th International Conference on Reachability Problems

PB - Springer International Publishing

ER -

Constrained Dynamic Tree Networks

Abstract

Publication series

Keywords

Access to Document

Other files and links

Verification of Concurrent and Higher-Order Recursive Programs

Cite this

Constrained Dynamic Tree Networks

Abstract

Publication series

Keywords

Access to Document

Other files and links

Projects

Verification of Concurrent and Higher-Order Recursive Programs

Cite this