Abstract
This paper investigates the connection between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we reduce the problem of generating linear and polynomial certificates of non-reachability for the Orbit Problem for linear transformations with coefficients in \(\mathbb Q\) to the generalized eigenvector problem. Also, we prove the existence of such certificates for any transformation with integer coefficients, which is not the case with rational coefficients.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The existence of such a family with \(N>1\) is guaranteed by the non diagonalisability of A.
References
Blazy, S., Bühler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112–130. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_7
Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_23
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)
de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479–494. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_30
de Oliveira, S., Bensalem, S., Prevosto, V.: Synthesizing invariants by solving solvable loops. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 327–343. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_22
de Oliveira, S., Prevosto, V., Habermehl, P., Bensalem, S.: Left-eigenvectors are certificates of the orbit problem. http://steven-de-oliveira.fr/content/publis/certificates_2018.pdf
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw. Eng. 27(2), 99–123 (2001)
Fijalkow, N., Ohlmann, P., Ouaknine, J., Pouly, A., Worrell, J.: Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem. In: STACS 2017. LIPIcs, vol. 66, pp. 29:1–29:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Kannan, R., Lipton, R.J.: The orbit problem is decidable. In: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing, pp. 252–261. ACM (1980)
Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM (JACM) 33(4), 808–821 (1986)
Kovács, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249–264. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_18
Rocha, H., Ismail, H., Cordeiro, L., Barreto, R.: Model checking embedded C software using k-induction and invariants. In: 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 90–95. IEEE (2015)
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443–476 (2007)
Schinzel, A., Zassenhaus, H.: A refinement of two theorems of Kronecker. Michigan Math. J 12, 81–85 (1965)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
de Oliveira, S., Prevosto, V., Habermehl, P., Bensalem, S. (2018). Left-Eigenvectors Are Certificates of the Orbit Problem. In: Potapov, I., Reynier, PA. (eds) Reachability Problems. RP 2018. Lecture Notes in Computer Science(), vol 11123. Springer, Cham. https://doi.org/10.1007/978-3-030-00250-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-00250-3_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00249-7
Online ISBN: 978-3-030-00250-3
eBook Packages: Computer ScienceComputer Science (R0)