Article

A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes

Author:

Naoki KobayashiAuthors Info & Claims

FOSSACS'11/ETAPS'11: Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software

Pages 260 - 274

Published: 26 March 2011 Publication History

Abstract

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.

References

[1]

Abramsky, S., McCusker, G.: Game semantics. In: Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School, pp. 1-56. Springer, Heidelberg (1999)

[2]

Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science 3(3) (2007)

[3]

Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Proc. of POPL, pp. 1-3 (2002)

Digital Library

[4]

Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. International Journal on Software Tools for Technology Transfer 9(5-6), 505-525 (2007)

Digital Library

[5]

Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 294-309. Springer, Heidelberg (2004)

[6]

Hague, M., Murawski, A., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 452-461. IEEE Computer Society, Los Alamitos (2008)

Digital Library

[7]

Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci. 311(1-3), 1-70 (2004)

Digital Library

[8]

Knapik, T., Niwinski, D., Urzyczyn, P.: Deciding monadic theories of hyperalgebraic trees. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 253-267. Springer, Heidelberg (2001)

Digital Library

[9]

Knapik, T., Niwinski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205-222. Springer, Heidelberg (2002)

Digital Library

[10]

Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25-36. ACM Press, New York (2009), see also {13}

Digital Library

[11]

Kobayashi, N.: TRecS (2009), http://www.kb.ecei.tohoku.ac.jp/~koba/trecs/

[12]

Kobayashi, N.: Types and higher-order recursion schemes for verification of higherorder programs. In: Proc. of POPL, pp. 416-428 (2009), see also {13}

Digital Library

[13]

Kobayashi, N.: Model checking higher-order programs. A revised and extended version of {12} and {10}, available from the author's web page (2010)

Digital Library

[14]

Kobayashi, N.: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes (2010), an extended version http://www.kb.ecei.tohoku.ac.jp/~koba/gtrecs/

Digital Library

[15]

Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 223-234. Springer, Heidelberg (2009)

Digital Library

[16]

Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: Proceedings of LICS 2009, pp. 179-188. IEEE Computer Society Press, Los Alamitos (2009)

Digital Library

[17]

Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and cegar for higher-order model checking (July 2010) (unpublished manuscript)

[18]

Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proc. of POPL, pp. 495-508 (2010)

Digital Library

[19]

Lester, M.M., Neatherway, R.P., Ong, C.-H.L., Ramsay, S.J.: Model checking liveness properties of higher-order functional programs (2010) (unpublished manuscript)

[20]

Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81-90. IEEE Computer Society Press, Los Alamitos (2006)

Digital Library

[21]

Ong, C.-H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011 (to appear, 2011)

Digital Library

[22]

Rehof, J., Mogensen, T.: Tractable constraints in finite semilattices. Science of Computer Programming 35(2), 191-221 (1999)

Digital Library

Cited By

Terao TSabel DThiemann P(2018)Lazy Abstraction for Higher-Order Program VerificationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236969(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236969
Kobayashi NLozes ÉBruse F(2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicACM SIGPLAN Notices10.1145/3093333.300985452:1(246-259)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009854
Kobayashi NLozes ÉBruse FCastagna GGordon A(2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009854(246-259)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009854
Show More Cited By

Recommendations

Types and higher-order recursion schemes for verification of higher-order programs
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...
Types and higher-order recursion schemes for verification of higher-order programs
POPL '09

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...
Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes
Proceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 8301

Higher-order (HO) model checking is the problem of deciding whether the tree generated by a higher-order recursion scheme (HORS) is accepted by an alternating parity tree automaton (APT). HO model checking has been shown to be decidable by Ong and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FOSSACS'11/ETAPS'11: Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software

March 2011

472 pages

ISBN:9783642198045

Editor:
Martin Hofmann
Ludwig-Maximilians-Universität München, Institut für Informatik, München, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 26 March 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Terao TSabel DThiemann P(2018)Lazy Abstraction for Higher-Order Program VerificationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236969(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236969
Kobayashi NLozes ÉBruse F(2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicACM SIGPLAN Notices10.1145/3093333.300985452:1(246-259)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009854
Kobayashi NLozes ÉBruse FCastagna GGordon A(2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009854(246-259)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009854
Ramsay SNeatherway ROng C(2014)A type-directed abstraction refinement approach to higher-order model checkingACM SIGPLAN Notices10.1145/2578855.253587349:1(61-72)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535873
Ramsay SNeatherway ROng CJagannathan SSewell P(2014)A type-directed abstraction refinement approach to higher-order model checkingProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535873(61-72)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535873
Kobayashi N(2013)Pumping by TypingProceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/2591370.2591382(398-407)Online publication date: 25-Jun-2013
https://dl.acm.org/doi/10.5555/2591370.2591382
Broadbent CCarayol AHague MSerre O(2013)C-SHOReACM SIGPLAN Notices10.1145/2544174.250058948:9(13-24)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500589
Broadbent CCarayol AHague MSerre OMorrisett GUustalu T(2013)C-SHOReProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500589(13-24)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2500365.2500589
Kobayashi N(2013)Model Checking Higher-Order ProgramsJournal of the ACM10.1145/2487241.248724660:3(1-62)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1145/2487241.2487246
Fujima KIto SKobayashi N(2013)Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion SchemesProceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 830110.1007/978-3-319-03542-0_2(17-32)Online publication date: 9-Dec-2013
https://dl.acm.org/doi/10.1007/978-3-319-03542-0_2
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents