Tool for Distributed Behavioural Analysis of Well-Structured Transition Systems

The model of well-structured transition systems became a broadly used tool for the study of concurrent and distributed systems. By means of this class of systems the following problems can be solved: coverability, inevitability, maintainability, termination, and a number of other semantic properties. Despite the fact that this model is known and studied for a few decades, the gap in practical analysis algorithms implementations and their investigation was noticed. As in reality modelled systems can have rather big number of states, approaches which are applied for their analysis should effectively utilize disposable resources to at least save researcher’s time. Goal of this work is to develop the tool for distributed behavioural analysis of well-structured transition systems. In the work the two main algorithms used for the behavioural properties analysis of well-structured transition systems are considered: saturation method and finite reachability tree, for which possible versions of concurrent implementation are presented. Based on this research the tool for the analysis of well-structured transition systems in the distributed environment is designed and developed. Applicability of the approach is demonstrated by experiment which investigates algorithms performance during analysis of Petri nets modelling dining philosophers problem of different sizes and arbitrary examples of Context-free grammars. The developed tool could be useful for the further research on different specific kinds of well-structured transition systems and the implemented analysis algorithms. The work contains 68 pages, 4 chapters, 39 figures, 19 tables, 47 references Keywords: formal verification, infinite systems, well-quasi-ordering, distributed calculations