The introduction of Well Structured Transition Systems (WSTS) in 1987 [8], i.e. transition systems that satisfies a monotony property with respect to some well-quasi-ordering (wqo), has led to an important number of decidability results of verification problems for several natural models: Petri Nets and VASS and a large number of their extensions, lossy channel systems, string rewrite systems, process algebra, communicating automaton, and so on. Surveys of results and applications obtained with this theory can be found in [9, 3, 1, 2]. The main idea behind these decidability results is a generic algorithm that explores a tree that must be finite by the wqo property: every infinite sequence of configurations of the system (xi)i∈N has an increasing pair, that is a pair i < j such that xi ≤ xj . Moreover, wqo theory has provided upper bound to these algorithms by bounding the length of so called bad sequences, (finite) sequences that do not have an increasing pair. The bounds obtained are non-primitive-recursive, which is unusual in verification. In addition, matching lower bounds has been proved for several models [19, 6].
分享
引用
