Простой алгоритм решения задачи покрытия для монотонных счетчиковых систем
Аннотация
Ключевые слова
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.)