Abstract | ||
---|---|---|
We consider the problem of symbolic reachability analysis of higher-order context-free processes. These models are generalizations of the context-free processes (also called BPA processes) where each process manipulates a data structure which can be seen as a nested stack of stacks. Our main result is that, for any higher-order context-free process, the set of all predecessors of a given regular set of configurations is regular and effectively constructible. This result generalizes the analogous result which is known for level 1 context-free processes. We show that this result holds also in the case of backward reachability analysis under a regular constraint on configurations. As a corollary, we obtain a symbolic model checking algorithm for the temporal logic E(U,X) with regular atomic predicates, i.e., the fragment of CTL restricted to the EU and EX modalities. |
Year | DOI | Venue |
---|---|---|
2004 | 10.1007/b104325 | Clinical Orthopaedics and Related Research |
Keywords | Field | DocType |
higher order,temporal logic,data structure | Data structure,Discrete mathematics,Model checking,Computer science,Generalization,Reachability,Symbolic data analysis,Temporal logic,Corollary,Regular constraint | Conference |
Volume | ISSN | ISBN |
3328 | FSTTCS 2004: Foundations of Software Technology and Theoretical
Computer Science (24/11/2004) 135-147 | 3-540-24058-6 |
Citations | PageRank | References |
17 | 0.85 | 24 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ahmed Bouajjani | 1 | 2663 | 184.84 |
Antoine Meyer | 2 | 79 | 4.69 |