Abstract
We put the program transformation method known as supercompilation in the context of works on counter systems, well-structured transition systems, Petri nets, etc. Two classic versions of the supercompilation algorithm are formulated for counter systems, using notions and notation adopted from the literature on transition systems.
A procedure to solve the coverability problem for a counter system by iterative application of a supercompiler to the system along with initial and target sets of states, is presented. Its correctness for monotonic counter systems provided the target set is upward-closed and the initial set has a certain form, is proved.
The fact that a supercompiler can solve the coverability problem for a lot of practically interesting counter systems has been discovered by A. Nemytykh and A. Lisitsa when they performed experiments on verification of cache-coherence protocols and other models by means of the Refal supercompiler SCP4, and since then theoretical explanation why this was so successful has been an open problem. Here the solution for the monotonic counter systems is given.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 27-30, pp. 313–321. IEEE Computer Society (1996)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. International Journal on Software Tools for Technology Transfer 10(5), 401–424 (2008)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Finkel, A.: The Minimal Coverability Graph for Petri Nets. In: Rozenberg, G. (ed.) APN 1993. LNCS, vol. 674, pp. 210–243. Springer, Heidelberg (1993)
Geeraerts, G.: Coverability and Expressiveness Properties of Well-Structured Transition Systems. PhD thesis, Université Libre de Bruxelles, Belgique (May 2007), http://www.ulb.ac.be/di/verif/ggeeraer/thesis.pdf
Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences 72(1), 180–203 (2006)
Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the Efficient Computation of the Minimal Coverability Set for Petri Nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 98–113. Springer, Heidelberg (2007)
Glück, R., Leuschel, M.: Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 93–100. Springer, Heidelberg (2000)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Klimov, And.V.: An approach to supercompilation for object-oriented languages: the Java Supercompiler case study. In: Nemytykh, A.P. (ed.) Proceedings of the First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp. 43–53. Ailamazyan University of Pereslavl, Pereslavl-Zalessky (2008)
Klimov, And.V.: JVer Project: Verification of Java programs by Java Supercompiler (2008), http://pat.keldysh.ru/jver/
Klimov, And.V.: A Java Supercompiler and Its Application to Verification of Cache-Coherence Protocols. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 185–192. Springer, Heidelberg (2010)
Klimov, And.V.: Yet another algorithm for solving coverability problem for monotonic counter systems. In: Nepomnyaschy, V., Sokolov, V. (eds.) Second Workshop on Program Semantics, Specification and Verification: Theory and Applications, PSSV 2011, St. Petersburg, Russia, June 12-13, pp. 59–67. Yaroslavl State University (2011)
Klyuchnikov, I.: Supercompiler HOSC 1.1: proof of termination. Preprint 21, Keldysh Institute of Applied Mathematics, Moscow (2010)
Klyuchnikov, I., Romanenko, S.: Multi-result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 210–226. Springer, Heidelberg (2012)
Leuschel, M., Lehmann, H.: Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 101–115. Springer, Heidelberg (2000)
Leuschel, M., Lehmann, H.: Solving coverability problems of Petri nets by partial deduction. In: Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Montreal, Canada, September 20-23, pp. 268–279. ACM (2000)
Lisitsa, A.P., Nemytykh, A.P.: Solving coverability problems by supercompilation. Invited talk. In: The Second Workshop on Reachability Problems in Computational Models (RP 2008), Liverpool, UK, September 15-17 (2008)
Lisitsa, A.P., Nemytykh, A.P.: Towards verification via supercompilation. In: COMPSAC (2), pp. 9–10. IEEE Computer Society (2005)
Lisitsa, A.P., Nemytykh, A.P.: Experiments on verification via supercompilation (2007), http://refal.botik.ru/protocols/
Lisitsa, A.P., Nemytykh, A.P.: Verification as a parameterized testing (experiments with the SCP4 supercompiler). Programming and Computer Software 33(1), 14–23 (2007)
Lisitsa, A.P., Nemytykh, A.P.: Reachability analysis in verification via supercompilation. Int. J. Found. Comput. Sci. 19(4), 953–969 (2008)
Luttge, K.: Zustandsgraphen von Petri-Netzen. Master’s thesis, Humboldt-Universität zu Berlin, Germany (1995)
Nemytykh, A.P.: The Supercompiler SCP4: General Structure. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 162–170. Springer, Heidelberg (2004)
Sørensen, M.H., Glück, R.: An algorithm of generalization in positive supercompilation. In: Lloyd, J.W. (ed.) International Logic Programming Symposium, Portland, Oregon, December 4-7, pp. 465–479. MIT Press (1995)
Turchin, V.F.: The Use of Metasystem Transition in Theorem Proving and Program Optimization. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 645–657. Springer, Heidelberg (1980)
Turchin, V.F.: The concept of a supercompiler. Transactions on Programming Languages and Systems 8(3), 292–325 (1986)
Turchin, V.F.: The algorithm of generalization in the supercompiler. In: Bjørner, D., Ershov, A.P., Jones, N.D. (eds.) Partial Evaluation and Mixed Computation, pp. 531–549. North-Holland (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klimov, A.V. (2012). Solving Coverability Problem for Monotonic Counter Systems by Supercompilation. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2011. Lecture Notes in Computer Science, vol 7162. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29709-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-29709-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29708-3
Online ISBN: 978-3-642-29709-0
eBook Packages: Computer ScienceComputer Science (R0)