Model checking trees generated by Higher-Order Recursion Schemes (HORS) of order k against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong’06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT, such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is \(k{-}1\) -EXPSPACE-complete. The upper bound is achieved by converting the problem into an alternating reachability game, the lower one via reduction from a tiling problem.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Space-Efficient Model-Checking of Higher-Order Recursion Schemes

  • Florian Bruse

摘要

Model checking trees generated by Higher-Order Recursion Schemes (HORS) of order k against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong’06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT, such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is \(k{-}1\) -EXPSPACE-complete. The upper bound is achieved by converting the problem into an alternating reachability game, the lower one via reduction from a tiling problem.