Interleaving Based Model Checking of Concurrency and Causality

• Autorzy: Wolf, K.
• Konferencja: International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Petri Nets 2017) (31; School of Engineering and Architecture of Zaragoza University; 25.30.07.2017; Spain)
• Języki publikacji: EN

Abstrakty

EN

We consider a spectrum of properties proposed in [14]. It is related to causality and concurrency between a pair of given transitions in a place/transition net. For each of these properties, we ask whether it can be verified using an ordinary, interleaving based, model checker. With a systematic approach based on two constructions, we reduce most properties in the spectrum to a reachability problem. Only one problem needs to be left open completely. Some problems can be solved only under the assumption of absent auto-concurrency.

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 161, nr 4
• Strony: 423--445
• Opis fizyczny: Bibliog. 21 poz., rys., tab.

Twórcy

autor

Wolf, K.

• Universität Rostock, Institut für Informatik, D–18051 Rostock, Germany,

Bibliografia

• [1] Best E and Devillers R. Sequential and concurrent behaviour in Petri net theory. Theoretical Computer Science, 1987;55(1):87-136. URL https://doi.org/10.1016/0304-3975(87)90090-9.
• [2] Best E and Fernandez C. Nonsequential Processes: A Petri Net View. EATCS Monographs on Theoretical Computer Science. Springer, 1988. ISBN-3540190309, 9783540190301.
• [3] Brauer W and Reisig W. Carl Adam Petri and “Petri nets”. Fundamental Concepts in Computer Science, 2009;3:129-139. URL https://doi.org/10.1142/9781848162914_0007.
• [4] Esparza J and Heljanko K. Unfoldings - A Partial-Order Approach to Model Checking. EATCS Monographs in Theoretical Computer Science. Springer, 2008. doi:10.1007/978-3-540-77426-6.
• [5] Goltz U and Reisig W. The non-sequential behaviour of Petri nets. Information and Control, 1983;57(2-3):125-147. URL https://doi.org/10.1016/S0019-9958(83)80040-0.
• [6] Grahlmann B. The PEP tool. In Computer Aided Verification CAV. Lecture Notes in Computer Science, vol. 1254. Springer, 1997, pp. 440-443. doi:10.1007/3-540-63166-6_43.
• [7] Heiner M, Rohr C, Schwarick M, and Tovchigrechko AA. Marcie’s secrets of efficient model checking. In Transactions on Petri Nets and Other Models of Concurrency IX. Lecture Notes in Computer Science, vol. 9930. Springer, 2016, pp. 286-296. doi:10.1007/978-3-662-53401-4_14.
• [8] Jensen JF, Nielsen T, Oestergaard LK, and Srba J. TAPAAL and reachability analysis of P/T nets. Transactions on Petri Nets and Other Models of Concurrency XI. Lecture Notes in Computer Science, vol. 9930, 2016, pp. 307-318. doi:/10.1007/978-3-662-53401-4_16.
• [9] Jensen K. Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use - Volume 1, Second Edition. EATCS Monographs in Theoretical Computer Science. Springer, 1996. doi:10.1007/978-3-662-03241-1.
• [10] Khomenko V. PUNF—Petri net unfolder. http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/.
• [11] McMillan KL. A technique of state space search based on unfolding. Formal Methods in System Design, 1995;6(1):45-65. doi:10.1007/BF01384314.
• [12] Nielsens M, Plotkin GD, and Winskel G. Petri nets, event structures and domains. Theoretical Computer Science, 1981;13(1):85-108. URL https://doi.org/10.1016/0304-3975(81)90112-2.
• [13] Petri CA. Kommunikation mit Automaten. Dissertation, Schriften des IIM 2, Rheinisch-Westfälisches Institut für Instrumentelle Mathematik an der Universität Bonn, Bonn, 1962.
• [14] Polyvyanyy A, Weidlich M, Conforti R, La Rosa M, and ter Hofstede AHM. The 4C spectrum of fundamental behavioral relations for concurrent systems. In PETRI NETS. Lecture Notes in Computer Science, vol 8489. Springer, 2014, pp. 210-232. doi:10.1007/978-3-319-07734-5_12.
• [15] Polyvyanyys A, Cornos L, Conforti R, Raboczi S, La Rosa M, and Fortino G. Process querying in Apromore. In BPM Demo Session, CEUR Workshop Proceedings 1418. 2015, pp. 105-109.
• [16] Schwoon S. Mole—a Petri net unfolder. http://www.lsv.ens-cachan.fr/~schwoon/tools/mole/.
• [17] Thierry-Mieg Y. Symbolic model-checking using ITS-Tools. In TACAS. Lecture Notes in Computer Science, vol. 9035. Springer. 2015, pp. 231-237. doi:10.1007/978-3-662-46681-0_20.
• [18] Weidlich M. Behavioural profiles: a relational approach to behaviour consistency. PhD thesis, University of Potsdam, 2011.
• [19] Wimmel H and Wolf K. Applying CEGAR to the Petri net state equation. In TACAS. Lecture Notes in Computer Science, vol. 6605. Springer, 2011, pp. 224-238. doi:10.1007/978-3-642-19835-9_19.
• [20] Wolf K. Generating Petri net state spaces. In PETRI NETS. Lecture Notes in Computer Science, vol. 4546. Springer. 2007, pp. 29-42.
• [21] Wolf K. Model checking concurrency and causality. In Proc. PETRI NETS. Lecture Notes in Computer Science, vol. 10258. Springer. 2017, pp. 159-178.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).

Identyfikatory

DOI

10.3233/FI-2018-1709