Model checking dynamic pushdown networks
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516413 | ||
| 003 | CHVBK | ||
| 005 | 20210128100714.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150301xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0330-y |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0330-y | ||
| 245 | 0 | 0 | |a Model checking dynamic pushdown networks |h [Elektronische Daten] |c [Fu Song, Tayssir Touili] |
| 520 | 3 | |a 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. | |
| 540 | |a British Computer Society, 2015 | ||
| 690 | 7 | |a Model checking |2 nationallicence | |
| 690 | 7 | |a Dynamic pushdown networks |2 nationallicence | |
| 690 | 7 | |a LTL |2 nationallicence | |
| 690 | 7 | |a CTL |2 nationallicence | |
| 700 | 1 | |a Song |D Fu |u Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, No. 3663 Zhongshan Road(N), Shanghai, People's Republic of China |4 aut | |
| 700 | 1 | |a Touili |D Tayssir |u Liafa, CNRS and Université Paris Diderot, Paris, France |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/2(2015-03-01), 397-421 |x 0934-5043 |q 27:2<397 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0330-y |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0330-y |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Song |D Fu |u Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, No. 3663 Zhongshan Road(N), Shanghai, People's Republic of China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Touili |D Tayssir |u Liafa, CNRS and Université Paris Diderot, Paris, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/2(2015-03-01), 397-421 |x 0934-5043 |q 27:2<397 |1 2015 |2 27 |o 165 | ||