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. 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
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)
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)
Diestel, R.: Graph Theory. Springer, Heidelberg (2010)
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)
Holzmann, G.: The Spin model checker: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)
Hopcroft, J.E., Pansiot, J.-J.: On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science 8, 135–159 (1979)
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)
Karp, R.M., Miller, R.E.: Parallel program schemata. Journal of Computer and System Sciences 3(2), 147–195 (1969)
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)
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)
Lipton, R.J.: The reachability problem requires exponential space. Technical Report 63, Yale University (1976)
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)
Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., New York (1986)
Sifakis, J.: Structural properties of Petri nets. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 474–483. Springer, Heidelberg (1978)
Sleator, D.D.: Data structures and terminating Petri nets. In: Simon, I. (ed.) LATIN 1992. LNCS, vol. 583, pp. 488–497. Springer, Heidelberg (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avellaneda, F., Morin, R. (2014). Exhibition of a Structural Bug with Wings. In: Ciardo, G., Kindler, E. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2014. Lecture Notes in Computer Science, vol 8489. Springer, Cham. https://doi.org/10.1007/978-3-319-07734-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-07734-5_14
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07733-8
Online ISBN: 978-3-319-07734-5
eBook Packages: Computer ScienceComputer Science (R0)