Sciweavers

Share
FOSSACS
2011
Springer

A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes

8 years 2 months ago
A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes
The model checking of higher-order recursion schemes has been actively studied and is now becoming a basis of higher-order program verification. We propose a new algorithm for trivial automata model checking of higher-order recursion schemes. To our knowledge, this is the first practical model checking algorithm for recursion schemes that runs in time linear in the size of the higher-order recursion scheme, under the assumption that the size of trivial automata and the largest order and arity of functions are fixed. The previous linear time algorithm was impractical due to a huge constant factor, and the only practical previous algorithm suffers from the hyper-exponential worst-case time complexity, under the same assumption. The new algorithm is remarkably simple, consisting of just two fixed-point computations. We have implemented the algorithm and confirmed that it outperforms Kobayashi’s previous algorithm in a certain case.
Naoki Kobayashi
Added 28 Aug 2011
Updated 28 Aug 2011
Type Journal
Year 2011
Where FOSSACS
Authors Naoki Kobayashi
Comments (0)
books