Tool for Behavioral Analysis of Well-Structured Transition Systems
https://doi.org/10.15514/ISPRAS-2017-29(4)-11
Abstract
Well-structured transition systems (WSTS) became a well-known tool in the study of concurrency systems for proving decidability of properties based on coverability and boundedness. Each year brings new formalisms proven to be WSTS systems. Despite the large body of theoretical work on the WSTS theory, there has been a notable gap of empirical research of well-structured transition systems. In this paper, the tool for behavioural analysis of such systems is presented. We suggest the extension of SETL language to describe WSTS systems (WSTSL). It makes the description of new formalisms very close to the formal definition. Therefore, it is easy to introduce and modify new formalisms as well as conduct analysis of the behavioural properties without much programming efforts. It is highly convenient when a new formalism is still under active development. Two most studied algorithms for analysis of well-structured transition systems behavior (backward reachability and the Finite Reachability Tree analyses) have been implemented; and, their performance was measured through the runs on such models as Petri Nets and Lossy Channel Systems. The developed tool can be useful for incorporating and testing analysis methods to formalisms that occur to be well-structuredness transition systems.
About the Authors
L. V. Dworzanski
National Research University Higher School of Economics
Russian Federation
Russian Federation
V. E. Mikhaylov
National Research University Higher School of Economics
Russian Federation
Russian Federation
References
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.
Review
For citations:
Dworzanski L.V., Mikhaylov V.E. Tool for Behavioral Analysis of Well-Structured Transition Systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):175-190. https://doi.org/10.15514/ISPRAS-2017-29(4)-11
Email this article 