Exhibition of a Structural Bug with Wings
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. Further minimizing the length or the number of distinct arcs in pathological paths is NP-hard.
In this paper we propose to represent pathological cycles in the form of a multiset of particular cycles called wings. We present an algorithm that builds in polynomial time a multiset of wings with a common starting point from the multiset of arcs that represents a pathological cycle. Interestingly the number of distinct wings we need is at most equal to the dimension of vectors which helps to describe in a concise way the underlying bug and to analyse it.
Next we tackle the problem of computing a pathological multiset built over wings with a bounded length. We show how to solve this problem in polynomial time by a reduction to a linear program using a separation algorithm.
KeywordsPolynomial Time Integral Solution Structural Termination Simple Path Separation Algorithm
Unable to display preview. Download preview PDF.
- 1.Avellaneda, F., Morin, R.: Checking partial-order properties of vector addition systems with states. In: International Conference on Application of Concurrency to System Design, pp. 100–109 (2013)Google Scholar
- 3.Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: DAC, pp. 427–432 (1995)Google Scholar
- 4.Cohen, E., Megiddo, N.: Strongly polynomial-time and NC algorithms for detecting cycles in dynamic graphs (preliminary version). In: Johnson, D.S. (ed.) STOC, pp. 523–534. ACM (1989)Google Scholar
- 7.Holzmann, G.: The Spin model checker: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)Google Scholar
- 9.Iwano, K., Steiglitz, K.: Testing for cycles in infinite graphs with periodic structure (extended abstract). In: Aho, A.V. (ed.) STOC, pp. 46–55. ACM (1987)Google Scholar
- 11.Kosaraju, S.R., Sullivan, G.F.: Detecting cycles in dynamic graphs in polynomial time (preliminary version). In: Simon, J. (ed.) STOC, pp. 398–406. ACM (1988)Google Scholar
- 13.Lipton, R.J.: The reachability problem requires exponential space. Technical Report 63, Yale University (1976)Google Scholar
- 17.Sleator, D.D.: Data structures and terminating Petri nets. In: Simon, I. (ed.) LATIN 1992. LNCS, vol. 583, pp. 488–497. Springer, Heidelberg (1992)Google Scholar