caa a22 4500 605516413 CHVBK 20210128100714.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s00165-014-0330-y doi (NATIONALLICENCE)springer-10.1007/s00165-014-0330-y Model checking dynamic pushdown networks [Elektronische Daten] [Fu Song, Tayssir Touili] A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. Thus, it is important to have model checking algorithms for DPNs. We consider in this work model checking DPNs against single-indexed LTL and CTL properties of the form $${\bigwedge f_i}$$ ⋀ f i such that f i is a LTL/CTL formula over the PDS i. We consider the model checking problems w.r.t. simple valuations (i.e., whether a configuration satisfies an atomic proposition depends only on its control location) and w.r.t. regular valuations (i.e., the set of the configurations satisfying an atomic proposition is a regular set of configurations). We show that these model checking problems are decidable. We propose automata-based approaches for computing the set of configurations of a DPN that satisfy the corresponding single-indexed LTL/CTL formula. British Computer Society, 2015 Model checking nationallicence Dynamic pushdown networks nationallicence LTL nationallicence CTL nationallicence Song Fu Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, No. 3663 Zhongshan Road(N), Shanghai, People's Republic of China aut Touili Tayssir Liafa, CNRS and Université Paris Diderot, Paris, France aut Formal Aspects of Computing Springer London 27/2(2015-03-01), 397-421 0934-5043 27:2<397 2015 27 165 https://doi.org/10.1007/s00165-014-0330-y text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0330-y text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Song Fu Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, No. 3663 Zhongshan Road(N), Shanghai, People's Republic of China aut NATIONALLICENCE 700 1- Touili Tayssir Liafa, CNRS and Université Paris Diderot, Paris, France aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/2(2015-03-01), 397-421 0934-5043 27:2<397 2015 27 165