Affiliations: [a] LAAS - CNRS, 7 avenue du colonel Roche, F-31077 Toulouse, France. [email protected]; [email protected] | [b] Aix Marseille Université, CNRS, LIF UMR 7279, F-13288,Marseille, France. [email protected]
Note: [*] Address for correspondence: LAAS - CNRS, 7 avenue du colonel Roche, F-31077 Toulouse, France
Abstract: Checking the structural boundedness and the structural termination of vector addition systems with states boils down to detecting pathological cycles. As opposed to their non-structural variants which require exponential space, these properties need polynomial time only. The algorithm searches for a counter-example in the form of a multiset of arcs computed by means of linear programming. Yet the minimal length of a pathological cycle can be exponential in the size of the system which makes it difficult to visualize and to analyze the detected bug in details. We propose to describe pathological cycles in the form of particular cycles called flowers. The latter are made of petals which are iterated circuits connected by simple paths that form a calyx. We present an algorithm that builds in polynomial time a flower from the multiset of arcs that represents a pathological cycle. Interestingly the number of petals within a flower is at most equal to the dimension of vectors which helps to describe in a concise way the underlying bug and to analyse it.
Keywords: Vector addition system with states, structural properties, counter-example, dynamic graph, zero-cycle
