Interleaving Based Model Checking of Concurrency and Causality

Issue title: Application and Theory of Petri Nets and Other Models of Concurrency: Special Issue of Selected Papers from Petri Nets 2017

Guest editors: Wil van der Aalst, Eike Best and Wojciech Penczek

Article type: Research Article

Authors: Wolf, Karsten^{; *}

Affiliations: Universität Rostock, Institut für Informatik, D–18051 Rostock, Germany. karsten.wolf@uni-rostock.de

Correspondence: [*] Address for correspondence: Universität Rostock, Institut für Informatik, D–18051 Rostock, Germany

Abstract: 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.

DOI: 10.3233/FI-2018-1709

Journal: Fundamenta Informaticae, vol. 161, no. 4, pp. 423-445, 2018