Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
3 results

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

Naoki Kobayashi ; C. -H. Luke Ong.
Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees generated by order-n recursion schemes is n-EXPTIME complete. We consider two subclasses of APT and investigate the&nbsp;[&hellip;]
Published on January 18, 2012

The Safe Lambda Calculus

William Blum ; C. -H. Luke Ong.
Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the&nbsp;[&hellip;]
Published on February 19, 2009

Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

Matthew Hague ; C. -H. Luke Ong.
Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested "stack of stacks" structure. These systems may be used to model higher-order programs and are closely related to the Caucal hierarchy of infinite graphs and safe higher-order&nbsp;[&hellip;]
Published on December 5, 2008

  • < Previous
  • 1
  • Next >