Symbolic Reachability Analysis of Higher-Order Context-Free Processes
| dc.creator | Bouajjani, Ahmed | |
| dc.creator | Meyer, Antoine | |
| dc.date | 2007-05-28 | |
| dc.date.accessioned | 2026-07-07T08:03:19Z | |
| dc.date.available | 2026-07-07T08:03:19Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/0705.3888 | |
| dc.identifier | http://arxiv.org/abs/0705.3888 | |
| dc.identifier | FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science (24/11/2004) 135-147 | |
| dc.identifier | doi:10.1007/b104325 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/129535 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Symbolic Reachability Analysis of Higher-Order Context-Free Processes | |
| dc.type | text |