Catching a Structural Bug with a Flower

• Autorzy: Avellaneda F. , Morin R.

Identyfikatory

DOI

10.3233/FI-2015-1245

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

vector addition system with states; structural properties; counterexample; dynamic graph; zero-cycle

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 140, nr 1
• Strony: 61--87
• Opis fizyczny: Bibliogr. 26 poz.

Twórcy

autor

Avellaneda F.

• LAAS - CNRS, 7 avenue du colonel Roche, F-31077 Toulouse, France

autor

Morin R.

• Aix Marseille Université, CNRS, LIF UMR 7279, F-13288,Marseille, France

Bibliografia

• [1] F. Avellaneda and R. Morin. Checking partial-order properties of vector addition systems with states. In Josep Carmona, Mihai T. Lazarescu, and Marta Pietkiewicz-Koutny, editors, 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013, pages 100–109. IEEE, 2013.
• [2] F. Avellaneda and R. Morin. Exhibition of a structural bug with wings. In Gianfranco Ciardo and Ekkart Kindler, editors, Application and Theory of Petri Nets and Concurrency - 35th International Conference, PETRI NETS 2014, Tunis, Tunisia, June 23-27, 2014. Proceedings, volume 8489 of Lecture Notes in Computer Science, pages 253–272. Springer, 2014.
• [3] D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323–342, 1983.
• [4] H. Carstensen. Decidability questions for fairness in Petri nets. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, STACS, volume 247 of Lecture Notes in Computer Science, pages 396–407. Springer, 1987.
• [5] E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the 32Nd Annual ACM/IEEE Design Automation Conference, DAC ’95, pages 427–432, New York, NY, USA, 1995. ACM.
• [6] E. Cohen and N. Megiddo. Strongly polynomial-time and NC algorithms for detecting cycles in dynamic graphs (preliminary version). In David S. Johnson, editor, STOC, pages 523–534. ACM, 1989.
• [7] R. Diestel. Graph Theory. Springer-Verlag, Heidelberg, 2010.
• [8] J. Esparza and M. Nielsen. Decidability issues for Petri nets - a survey. Bulletin of the EATCS, 52:244–262, 1994.
• [9] B. Genest, D. Kuske, and A. Muscholl. A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput., 204(6):920–956, 2006.
• [10] J. G. Henriksen, M. Mukund, K. Narayan Kumar, M. A. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Information and Computation, 202(1):1–38, 2005.
• [11] J.E. Hopcroft and J-J. Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135–159, 1979.
• [12] K. Iwano and K. Steiglitz. Testing for cycles in infinite graphs with periodic structure (extended abstract). In Alfred V. Aho, editor, STOC, pages 46–55. ACM, 1987.
• [13] R.M. Karp and R.E.Miller. Parallel programschemata. Journal of Computer and System Sciences, 3(2):147–195, 1969.
• [14] D. König. Theorie der endlichen und unendlichen Graphen. Leipzig: Akademische Verlagsgesellschaft, 1936.
• [15] S. R. Kosaraju and G. F. Sullivan. Detecting cycles in dynamic graphs in polynomial time (preliminary version). In Janos Simon, editor, STOC, pages 398–406. ACM, 1988.
• [16] O. Kupferman and S. Sheinvald-Faragy. Finding shortest witnesses to the nonemptiness of automata on infinite words. In Christel Baier and Holger Hermanns, editors, CONCUR, volume 4137 of Lecture Notes in Computer Science, pages 492–508. Springer, 2006.
• [17] S. Leue, R. Mayr, and W. Wei. A scalable incomplete test for the boundedness of UML RT models. In Kurt Jensen and Andreas Podelski, editors, TACAS, volume 2988 of Lecture Notes in Computer Science, pages 327–341. Springer, 2004.
• [18] S. Leue andW.Wei. Integer linear programming-based property checking for asynchronous reactive systems. IEEE Trans. Software Eng., 39(2):216–236, 2013.
• [19] R.J. Lipton. The reachability problem requires exponential space. Technical Report 63, Yale University, 1976.
• [20] R. Mayr. Undecidable problems in unreliable computations. Theor. Comput. Sci., 297(1-3):337–354, 2003.
• [21] G. Memmi and G. Roucairol. Linear algebra in net theory. InWilfried Brauer, editor, Advanced Course: Net Theory and Applications, volume 84 of Lecture Notes in Computer Science, pages 213–223. Springer, 1980.
• [22] A. Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., New York, NY, USA, 1986.
• [23] J. Sifakis. Structural properties of Petri nets. In J´ozefWinkowski, editor,MFCS, volume 64 of Lecture Notes in Computer Science, pages 474–483. Springer, 1978.
• [24] D.D. Sleator. Data structures and terminating Petri nets. In Imre Simon, editor, LATIN, volume 583 of Lecture Notes in Computer Science, pages 488–497. Springer, 1992.
• [25] A. Trivedi. Interesting title for Vardi’s 1986 paper. http://blogs.warwick.ac.uk/atrivedi/entry/interesting_title_for, 2005.
• [26] M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In LICS, pages 332–344. IEEE Computer Society, 1986.