maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1102Research ArticleОригинальные статьиArticlesПростой алгоритм решения задачи покрытия для монотонных счетчиковых системA Simple Algorithm for Solving the Coverability Problem for Monotonic Counter SystemsКлимовАндрей ВалентиновичKlimovAnd. V.klimov@keldysh.ruИнститут прикладной математики им. М.В. Келдыша РАНRussian Federation201120122011184106117Copyright © Климов А.В., 20112011Климов А.В.Klimov A.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1102

Предложен алгоритм решения задачи покрытия для монотонных счетчиковых систем. Разрешимость этой задачи хорошо известна, но данный алгоритм интересен своей простотой. Он возник из упрощения некоторой итеративной процедуры применения суперкомпилятора (специализатора программ, основанного на методе суперкомпиляции В.Ф. Турчина) к программе, кодирующей счетчиковую систему и начальное и целевое множества состояний, и из доказательства, что при определенных условиях эта процедура завершается и решает задачу покрытия.

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.

хорошо-структурированные системы переходовсчетчиковые системызадача достижимостизадача покрытиясуперкомпиляцияwell-structured transition systemscounter systemsreachabilitycoverabilitysupercompilationReferencesКузьмин Е.В., Соколов В.А. Вполне структурированные системы помеченных переходов. М.: Физматлит, 2005.Кузьмин Е.В., Соколов В.А. Вполне структурированные системы помеченных переходов. М.: Физматлит, 2005.Немытых А.П. Суперкомпилятор SCP4: общая структура. М.: Editorial URSS, 2007.Немытых А.П. Суперкомпилятор SCP4: общая структура. М.: Editorial URSS, 2007.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.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.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.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.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>.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>.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.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.Richard M. Karp and Raymond E. Miller. Parallel program schemata // J. Comput. Syst. Sci. 1969. 3(2). P. 147-195.Richard M. Karp and Raymond E. Miller. Parallel program schemata // J. Comput. Syst. Sci. 1969. 3(2). P. 147-195.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.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.Klimov Andrei V. JVer Project: Verification of Java programs by Java Supercompiler, 2008. Электронный ресурс: <http://pat.keldysh.ru/jver/>.Klimov Andrei V. JVer Project: Verification of Java programs by Java Supercompiler, 2008. Электронный ресурс: <http://pat.keldysh.ru/jver/>.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.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.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.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.Klimov Andrei V., Klimov Arkady V., Shvorin Artem B. The Java Supercompiler Project. Электронный ресурс: <http://www.supercompilers.ru>.Klimov Andrei V., Klimov Arkady V., Shvorin Artem B. The Java Supercompiler Project. Электронный ресурс: <http://www.supercompilers.ru>.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.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.Lisitsa Alexei P., Nemytykh Andrei P. Experiments on verification via supercompilation, 2007. Электронный ресурс: <http://refal.botik.ru/protocols/>.Lisitsa Alexei P., Nemytykh Andrei P. Experiments on verification via supercompilation, 2007. Электронный ресурс: <http://refal.botik.ru/protocols/>.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.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.Lisitsa Alexei P., Nemytykh Andrei P. Reachability analysis in verification via supercompilation //Int. J. Found. Comput. Sci. 2008. 19(4). P. 953-969.Lisitsa Alexei P., Nemytykh Andrei P. Reachability analysis in verification via supercompilation //Int. J. Found. Comput. Sci. 2008. 19(4). P. 953-969.Turchin Valentin F. The use of metasystem transition in theorem proving and program optimization // ICALP. Springer, 1980. LNCS. Vol. 85. P. 645-657.Turchin Valentin F. The use of metasystem transition in theorem proving and program optimization // ICALP. Springer, 1980. LNCS. Vol. 85. P. 645-657.Turchin Valentin F. The concept of a supercompiler // Transactions on Programming Languages and Systems. 1986. 8(3). P. 292-325.Turchin Valentin F. The concept of a supercompiler // Transactions on Programming Languages and Systems. 1986. 8(3). P. 292-325.Turchin Valentin F. Metacomputation: Metasystem transitions plus supercompilation // Dagstuhl Seminar on Partial Evaluation. Springer, 1996. LNCS. Vol. 1110. P. 481-509.Turchin Valentin F. Metacomputation: Metasystem transitions plus supercompilation // Dagstuhl Seminar on Partial Evaluation. Springer, 1996. LNCS. Vol. 1110. P. 481-509.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.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.

The authors declare that there are no conflicts of interest present.