Program for Behavioral Analysis of Well-Structured Transition Systems

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. The WSTS systems are described via the extension of SETL language. It makes the description of the formalism as close to the formal definition as possible. It allow.s easily introduce new formalisms and conduct analysis of the behavioural properties without programming efforts. 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 analysis of different subclasses of well-structured transition systems. Keywords: formal verification; infinite systems; well-quasi-ordering; Petri net