@inproceedings{BouajjaniMeyer:Higher:2007,
    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.},
    Author = {Bouajjani, Ahmed and Meyer, Antoine},
    BookTitle = {Proc. of FSTTCS'04},
    EPrint = {0705.3888v1},
    Editor = {Lodaya, Kamal and Mahajan, Meena},
    File = {Symbolic Reachability Analysis of Higher-Order Context-Free Processes - Bouajjani, Meyer (0) (0) - a - a - g.pdf},
    ISBN = {978-3-540-24058-7},
    Keywords = {higher-order model checking and higher-order pushdown automata and saturation method},
    Pages = {135--147},
    Publisher = {Springer Berlin Heidelberg},
    Series = {LNCS},
    Title = {Symbolic Reachability Analysis of Higher-Order Context-Free Processes},
    URL = {http://dx.doi.org/10.1007/978-3-540-30538-5\_12},
    Volume = {3328},
    Year = {2004},
    bdsk-url-1 = {http://arxiv.org/abs/0705.3888v1},
    bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-540-30538-5\_12},
    date-added = {2012-03-06 19:10:35 +0100},
    date-modified = {2014-05-29 11:09:01 +0000},
    doi = {10.1007/978-3-540-30538-5_12}
}

@inproceedings{BouajjaniMeyer:Higher:2007, 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.}, Author = {Bouajjani, Ahmed and Meyer, Antoine}, BookTitle = {Proc. of FSTTCS'04}, EPrint = {0705.3888v1}, Editor = {Lodaya, Kamal and Mahajan, Meena}, File = {Symbolic Reachability Analysis of Higher-Order Context-Free Processes - Bouajjani, Meyer (0) (0) - a - a - g.pdf}, ISBN = {978-3-540-24058-7}, Keywords = {higher-order model checking and higher-order pushdown automata and saturation method}, Pages = {135--147}, Publisher = {Springer Berlin Heidelberg}, Series = {LNCS}, Title = {Symbolic Reachability Analysis of Higher-Order Context-Free Processes}, URL = {http://dx.doi.org/10.1007/978-3-540-30538-5_12}, Volume = {3328}, Year = {2004}, bdsk-url-1 = {http://arxiv.org/abs/0705.3888v1}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-540-30538-5_12}, date-added = {2012-03-06 19:10:35 +0100}, date-modified = {2014-05-29 11:09:01 +0000}, doi = {10.1007/978-3-540-30538-5_12} }