Простой алгоритм решения задачи покрытия для монотонных счетчиковых систем
Аннотация
Предложен алгоритм решения задачи покрытия для монотонных счетчиковых систем. Разрешимость этой задачи хорошо известна, но данный алгоритм интересен своей простотой. Он возник из упрощения некоторой итеративной процедуры применения суперкомпилятора (специализатора программ, основанного на методе суперкомпиляции В.Ф. Турчина) к программе, кодирующей счетчиковую систему и начальное и целевое множества состояний, и из доказательства, что при определенных условиях эта процедура завершается и решает задачу покрытия.
Ключевые слова
хорошо-структурированные системы переходов,
счетчиковые системы,
задача достижимости,
задача покрытия,
суперкомпиляция
MSC2020: 519.681.3
Список литературы
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.
Рецензия
Для цитирования:
Климов А.В. Простой алгоритм решения задачи покрытия для монотонных счетчиковых систем. Моделирование и анализ информационных систем. 2011;18(4):106-117.
For citation:
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.)
Просмотров: 310
Послать статью по эл. почте 