Geodesic
A simple algorithm for solving the coverability problem for monotonic counter systems
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 106-117.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: well-structured transition systems, counter systems, reachability, coverability, supercompilation. 
@article{MAIS_2011_18_4_a9,
     author = {A. V. Klimov},
     title = {A simple algorithm for solving the coverability problem for monotonic counter systems},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {106--117},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a9/}
}
TY  - JOUR
AU  - A. V. Klimov
TI  - A simple algorithm for solving the coverability problem for monotonic counter systems
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 106
EP  - 117
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a9/
LA  - ru
ID  - MAIS_2011_18_4_a9
ER  - 
%0 Journal Article
%A A. V. Klimov
%T A simple algorithm for solving the coverability problem for monotonic counter systems
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 106-117
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a9/
%G ru
%F MAIS_2011_18_4_a9
A. V. Klimov. A simple algorithm for solving the coverability problem for monotonic counter systems. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 106-117. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a9/

[1] E. V. Kuzmin, V. A. Sokolov, Vpolne strukturirovannye sistemy pomechennykh perekhodov, Fizmatlit, M., 2005 | Zbl

[2] A. P. Nemytykh, Superkompilyator SCP4: obschaya struktura, Editorial URSS, M., 2007

[3] Aziz Abdulla Parosh, Kārlis Čerāns, 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, 313–321 | MR

[4] Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen, “Reset nets between decidability and undecidability”, Automata, Languages and Programming, 25th International Colloquium, Proceedings (ICALP'98, Aalborg, Denmark, July 13–17, 1998), LNCS, 1443, Springer, 1998, 103–115 | MR

[5] Gilles Geeraerts, Coverability and Expressiveness Properties of Well-Structured Transition Systems, PhD thesis, Université Libre de Bruxelles, Belgique, 2007 http://www.ulb.ac.be/di/verif/ggeeraer/thesis.pdf

[6] Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin, “Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS”, Journal of Computer and System Sciences, 72(1) (2006), 180–203 | DOI | MR

[7] Richard M. Karp and Raymond E. Miller, “Parallel program schemata”, J. Comput. Syst. Sci., 3(2) (1969), 147–195 | DOI | MR | Zbl

[8] Andrei V. Klimov, “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), Ailamazyan University of Pereslavl, Pereslavl-Zalessky, 2008, 43–53

[9] Andrei V. Klimov, JVer Project: Verification of Java programs by Java Supercompiler, 2008 http://pat.keldysh.ru/jver/

[10] Andrei V. Klimov, “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), LNCS, 5947, Springer, 2010, 185–192 | Zbl

[11] Andrei V. Klimov, “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), Ershov Institute of Informatics Systems, Novosibirsk, 2011, 92–103

[12] Andrei V. Klimov, Arkady V. Klimov, Artem B. Shvorin, The Java Supercompiler Project http://www.supercompilers.ru

[13] I. Klyuchnikov, S. Romanenko, “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), Ershov Institute of Informatics Systems, Novosibirsk, 2011, 104–115

[14] Alexei P. Lisitsa, Andrei P. Nemytykh, Experiments on verification via supercompilation, 2007 http://refal.botik.ru/protocols/

[15] Alexei P. Lisitsa, Andrei P. Nemytykh, “Verification as a parameterized testing (experiments with the SCP4 supercompiler)”, Programming and Computer Software, 33(1) (2007), 14–23 | DOI

[16] Alexei P. Lisitsa, Andrei P. Nemytykh, “Reachability analysis in verification via supercompilation”, Int. J. Found. Comput. Sci., 19(4) (2008), 953–969 | DOI | MR | Zbl

[17] Valentin F. Turchin, “The use of metasystem transition in theorem proving and program optimization”, ICALP, LNCS, 85, Springer, 1980, 645–657 | MR

[18] Valentin F. Turchin, “The concept of a supercompiler”, Transactions on Programming Languages and Systems, 8(3) (1986), 292–325 | DOI | Zbl

[19] Valentin F. Turchin, “Metacomputation: Metasystem transitions plus supercompilation”, Dagstuhl Seminar on Partial Evaluation, LNCS, 1110, Springer, 1996, 481–509

[20] Valentin F. Turchin, “Supercompilation: techniques and results”, Perspectives of System Informatics, Second International Andrei Ershov Memorial Conference (Akademgorodok, Novosibirsk, Russia, June 25–28, 1996. Proceedings), LNCS, 1181, Springer, 1996, 227–248