Abstract
This paper studies the complexity of the reachability problem (a typical and practically important instance of the model-checking problem) for simply-typed call-by-value programs with recursion, Boolean values, and non-deterministic branch, and proves the following results. (1) The reachability problem for order- 3 programs is nonelementary. Thus, unlike in the call-by-name case, the order of the input program does not serve as a good measure of the complexity. (2) Instead, the depth of types is an appropriate measure: the reachability problem for depth- n programs is n -EXPTIME complete. In particular, the previous upper bound given by the CPS translation is not tight. The algorithm used to prove the upper bound result is based on a novel intersection type system, which we believe is of independent interest.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)
Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: CSL 2013. LIPIcs, vol. 23, pp. 129–148, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)
Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP 2000, pp. 198–208. ACM (2000)
Engelfriet, J.: Iterated stack automata and complexity classes. Inf. Comput. 95(1), 21–75 (1991)
Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Trans. Program. Lang. Syst. 27(2), 264–313 (2005)
Knapik, T., Niwiński, 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)
Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: POPL 2009, pp. 416–428. ACM (2009)
Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3), 20 (2013)
Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS 2009, pp. 179–188. IEEE Computer Society (2009)
Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science 7(4) (2011)
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI 2011, pp. 222–233. ACM (2011)
Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: POPL 2010, pp. 495–508. ACM (2010)
Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Electr. Notes Theor. Comput. Sci. 1, 370–392 (1995)
Nielsen, L.R.: A selective cps transformation. Electr. Notes Theor. Comput. Sci. 45, 311–331 (2001)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90. IEEE Computer Society (2006)
Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: PEPM 2013, pp. 53–62. ACM (2013)
Tobita, Y., Tsukada, T., Kobayashi, N.: Exact flow analysis by higher-order model checking. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 275–289. Springer, Heidelberg (2012)
van Bakel, S.: Intersection type assignment systems. Theor. Comput. Sci. 151(2), 385–435 (1995)
Zeilberger, N.: Refinement types and computational duality. In: PLPV 2009, pp. 15–26. ACM (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tsukada, T., Kobayashi, N. (2014). Complexity of Model-Checking Call-by-Value Programs. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)