A Simple Algorithm for Solving the Coverability Problem for Monotonic Counter Systems
Abstract
An algorithm for solving the coverability problem for monotonic counter systems is presented. The solvability of this problem is well-known, but the algorithm is interesting due to its simplicity. The algorithm has emerged as a simplification of a certain procedure of a supercompiler application (a program specializer based on V.F. Turchin's supercompilation) to a program encoding a monotonic counter system along with initial and target sets of states and from the proof that under some conditions the procedure terminates and solves the coverability problem.
About the Author
And. V. Klimov
Институт прикладной математики им. М.В. Келдыша РАН
Russian Federation
Russian Federation
References
1. Кузьмин Е.В., Соколов В.А. Вполне структурированные системы помеченных переходов. М.: Физматлит, 2005.
2. Немытых А.П. Суперкомпилятор SCP4: общая структура. М.: Editorial URSS, 2007.
3. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems // The 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 27-30, 1996. IEEE Computer Society, 1996. P. 313-321.
4. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability //Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings. Springer, 1998. LNCS. Vol. 1443. P. 103-115.
5. Gilles Geeraerts. Coverability and Expressiveness Properties of Well-Structured Transition Systems. PhD thesis, Universite Libre de Bruxelles, Belgique, May 2007. <http://www.ulb.ac.be/di/verif/ggeeraer/thesis.pdf>.
6. Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS // Journal of Computer and System Sciences. 2006. 72(1). P. 180-203.
7. Richard M. Karp and Raymond E. Miller. Parallel program schemata // J. Comput. Syst. Sci. 1969. 3(2). P. 147-195.
8. Klimov Andrei V. An approach to supercompilation for object-oriented languages: the Java Supercompiler case study // The First International Workshop on Metacomputation in Russia, Proceedings. Pereslavl-Zalessky, Russia, July 2-5, 2008. Pereslavl-Zalessky: Ailamazyan University of Pereslavl, 2008. P. 43-53.
9. Klimov Andrei V. JVer Project: Verification of Java programs by Java Supercompiler, 2008. Электронный ресурс: <http://pat.keldysh.ru/jver/>.
10. Klimov Andrei V. A Java Supercompiler and its application to verification of cache- coherence protocols // Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. Springer, 2010. LNCS. Vol. 5947. P. 185-192.
11. Klimov Andrei V. Solving coverability problem for monotonic counter systems by supercompilation // The 8th Andrei Ershov Informatics Conference, PSI 2011, Akademgorodok, Novosibirsk, Russia, June 27 - July 01, 2011. Novosibirsk: Ershov Institute of Informatics Systems, 2011. P. 92-103.
12. Klimov Andrei V., Klimov Arkady V., Shvorin Artem B. The Java Supercompiler Project. Электронный ресурс: <http://www.supercompilers.ru>.
13. Klyuchnikov I., Romanenko S. Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions. // The 8th Andrei Ershov Informatics Conference, PSI 2011, Novosibirsk, Russia, June 27 - July 01, 2011. Novosibirsk: Ershov Institute of Informatics Systems, 2011. P. 104-115.
14. Lisitsa Alexei P., Nemytykh Andrei P. Experiments on verification via supercompilation, 2007. Электронный ресурс: <http://refal.botik.ru/protocols/>.
15. Lisitsa Alexei P., Nemytykh Andrei P. Verification as a parameterized testing (experiments with the SCP4 supercompiler) //Programming and Computer Software. 2007. 33(1). P. 14-23.
16. Lisitsa Alexei P., Nemytykh Andrei P. Reachability analysis in verification via supercompilation //Int. J. Found. Comput. Sci. 2008. 19(4). P. 953-969.
17. Turchin Valentin F. The use of metasystem transition in theorem proving and program optimization // ICALP. Springer, 1980. LNCS. Vol. 85. P. 645-657.
18. Turchin Valentin F. The concept of a supercompiler // Transactions on Programming Languages and Systems. 1986. 8(3). P. 292-325.
19. Turchin Valentin F. Metacomputation: Metasystem transitions plus supercompilation // Dagstuhl Seminar on Partial Evaluation. Springer, 1996. LNCS. Vol. 1110. P. 481-509.
20. Turchin Valentin F. Supercompilation: techniques and results // Perspectives of System Informatics, Second International Andrei Ershov Memorial Conference, Akademgorodok, Novosibirsk, Russia, June 25-28, 1996. Proceedings. Springer, 1996. LNCS. Vol. 1181. P. 227-248.
Review
For citations:
Klimov A.V. A Simple Algorithm for Solving the Coverability Problem for Monotonic Counter Systems. Modeling and Analysis of Information Systems. 2011;18(4):106-117. (In Russ.)
Views:
532
Email this article 