Инструмент для анализа поведения вполне структурированных систем переходов

Вполне структурированные системы переходов являются хорошо известным инструментом для доказательства разрешимости свойств покрываемости и ограниченности. Каждый год появляются новые формализмы, которые оказываются вполне структурированными системами переходов. Несмотря на большой объем теоретической работы, существует большая потребность в эмпирических изучении вполне структурированных систем переходов. В данной работе представлен инструмент для анализа таких систем. Мы предлагаем расширение высокоуровневого языка SETL для описания вполне-структурированных систем переходов. Это позволяет описывать новые формализмы близко к их формальному определению. Таким образом упрощается создание и изменение новых формализмов, а также осуществление анализа поведенческих свойств без большого объема программистских усилий. Это удобно, когда новый формализм находится в стадии изучения и разработки. Были реализованы два самых изученных алгоритма анализа поведения вполне структурированных систем переходов (обратный алгоритм и анализ конечных деревьев достижимости). Их производительность была измерена на моделях сетей Петри и систем с потерей сигналов. Разработанный инструмент может быть полезным при внедрении и тестировании методов анализа формализмов, которые оказываются вполне структурированными системами переходов.

формальная верификация, системы с бесконечным числом состояний, вполне структурированные системы Переходов, сети Петри

1. J. Burch, E. Clarke, K. McMillan, D. Dill and L. Hwang, "Symbolic model checking: 1020 States and beyond", Information and Computation, vol. 98, no. 2, pp. 142-170, 1992.

2. A. Finkel, “Well structured transition systems,” Univ. Paris-Sud, Orsay, France, Res. Rep. 365, Aug. 1987.

3. A. Finkel and P. Schnoebelen, "Well-structured transition systems everywhere!", Theoretical Computer Science, vol. 256, no. 1-2, pp. 63-92, 2001.

4. P. Abdulla, K. Čerāns, B. Jonsson and Y. Tsay, "Algorithmic Analysis of Programs with Well Quasi-ordered Domains", Information and Computation, vol. 160, no. 1-2, pp. 109-127, 2000.

5. R. Karp and R. Miller, "Parallel program schemata", Journal of Computer and System Sciences, vol. 3, no. 2, pp. 147-195, 1969.

6. E. Kouzmin and V. Sokolov, Well-Structured Labeled Transition Systems, Moscow: Fizmatlit, 2005.

7. J. Kruskal, "The theory of well-quasi-ordering: A frequently discovered concept", Journal of Combinatorial Theory, Series A, vol. 13, no. 3, pp. 297-305, 1972.

8. T. Parr, The definitive ANTLR 4 reference, Raleigh, NC and Dallas, TX: The Pragmatic Bookshelf, 2013.

9. L. Dickson, "Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors", American Journal of Mathematics, vol. 35, no. 4, pp. 413-422, 1913.

10. E. Dijkstra, "Hierarchical ordering of sequential processes", Acta Informatica, vol. 1, no. 2, pp. 115-138, 1971.

11. S. Akshay, B. Genest, L. Hélouët, Decidable Classes of Unbounded Petri Nets with Time and Urgency. In: F. Kordon, D. Moldt (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2016. Lecture Notes in Computer Science, vol 9698. Springer, Cham

12. L. W. Dworzanski, Consistent Timed Semantics for Nested Petri Nets with Restricted Urgency, in: Formal Modeling and Analysis of Timed Systems Vol. 9884. Switzerland : Springer International Publishing, 2016. doi Ch. 1. pp. 3-18.

13. J. T. Schwartz, "Set Theory as a Language for Program Specification and Programming". Courant Institute of Mathematical Sciences, New York University, 1970.

14. R. Dewar, "SETL and the Evolution of Programming." In From Linear Operators to Computational Biology, pp. 39-46. Springer London, 2013.