Exhibition of a Structural Bug with Wings

  • Florent Avellaneda
  • Rémi Morin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8489)


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.


Polynomial Time Integral Solution Structural Termination Simple Path Separation Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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
  2. 2.
    Carstensen, H.: Decidability questions for fairness in Petri nets. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 396–407. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  3. 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. 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
  5. 5.
    Diestel, R.: Graph Theory. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Henriksen, J.G., Mukund, M., Narayan Kumar, K., Sohoni, M.A., Thiagarajan, P.S.: A theory of regular MSC languages. Information and Computation 202(1), 1–38 (2005)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Holzmann, G.: The Spin model checker: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)Google Scholar
  8. 8.
    Hopcroft, J.E., Pansiot, J.-J.: On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science 8, 135–159 (1979)MathSciNetCrossRefGoogle Scholar
  9. 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
  10. 10.
    Karp, R.M., Miller, R.E.: Parallel program schemata. Journal of Computer and System Sciences 3(2), 147–195 (1969)MathSciNetCrossRefGoogle Scholar
  11. 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
  12. 12.
    Kupferman, O., Sheinvald-Faragy, S.: Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 492–508. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Lipton, R.J.: The reachability problem requires exponential space. Technical Report 63, Yale University (1976)Google Scholar
  14. 14.
    Memmi, G., Roucairol, G.: Linear algebra in net theory. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol. 84, pp. 213–223. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  15. 15.
    Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., New York (1986)zbMATHGoogle Scholar
  16. 16.
    Sifakis, J.: Structural properties of Petri nets. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 474–483. Springer, Heidelberg (1978)CrossRefGoogle Scholar
  17. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Florent Avellaneda
    • 1
  • Rémi Morin
    • 1
  1. 1.Aix Marseille Université, CNRS, LIF UMR 7279MarseilleFrance

Personalised recommendations