Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
426490 | Information and Computation | 2014 | 16 Pages |
Abstract
We propose a new approach to analyzing higher-order recursive schemes. Many results in the literature use automata models generalizing pushdown automata, most notably higher-order pushdown automata with collapse (CPDA). Instead, we propose to use the Krivine machine model. Compared to CPDA, this model is closer to lambda-calculus, and incorporates nicely many invariants of computations, as for example the typing information. The usefulness of the proposed approach is demonstrated with new proofs of two central results in the field: the decidability of the local and global model checking problems for higher-order schemes with respect to the mu-calculus.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Sylvain Salvati, Igor Walukiewicz,