Fundamenta Informaticae - Volume 161, issue 4

Authors: van der Aalst, Wil | Best, Eike | Penczek, Wojciech

Article Type: Other

DOI: 10.3233/FI-2018-1705

Citation: Fundamenta Informaticae, vol. 161, no. 4, pp. i-ii, 2018

Authors: Bérard, Béatrice | Haar, Stefan | Schmitz, Sylvain | Schwoon, Stefan

Article Type: Research Article

Abstract: Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL -complete for finite state systems, PSPACE -complete for safe convergent …Petri nets (even with fairness), and EXPSPACE -complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE -complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness. Show more

Keywords: Diagnosability, Opacity, Verification, Complexity, Petri nets

DOI: 10.3233/FI-2018-1706

Citation: Fundamenta Informaticae, vol. 161, no. 4, pp. 317-349, 2018

Authors: Dalsgaard, Andreas E. | Enevoldsen, Søren | Fogh, Peter | Jensen, Lasse S. | Jensen, Peter G. | Jepsen, Tobias S. | Kaufmann, Isabella | Larsen, Kim G. | Nielsen, Søren M. | Olesen, Mads Chr. | Pastva, Samuel | Srba, Jiří

Article Type: Research Article

Abstract: Equivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verification problems) suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate, in certain scenarios, the domain value 0, in …addition to the standard back-propagation of the value 1. Finally, we design a distributed version of the algorithm, implement it in our open-source tool TAPAAL, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest. Show more

DOI: 10.3233/FI-2018-1707

Citation: Fundamenta Informaticae, vol. 161, no. 4, pp. 351-381, 2018

Authors: Hujsa, Thomas | Devillers, Raymond

Article Type: Research Article

Abstract: Liveness, (non-)deadlockability and reversibility are behavioral properties of Petri nets that are fundamental for many real-world systems. Such properties are often required to be monotonic, meaning preserved upon any increase of the marking. However, their checking is intractable in general and their monotonicity is not always satisfied. To simplify the analysis of these features, structural approaches have been fruitfully exploited in particular subclasses of Petri nets, deriving the behavior from the underlying graph and the initial marking only, often in polynomial time. In this paper, we further develop these efficient structural methods to analyze deadlockability, liveness, reversibility and their …monotonicity in weighted Petri nets. We focus on the join-free subclass, which forbids synchronizations, and on the homogeneous asymmetric-choice subclass, which allows conflicts and synchronizations in a restricted fashion. For the join-free nets, we provide several structural conditions for checking liveness, (non-)deadlockability, reversibility and their monotonicity. Some of these methods operate in polynomial time. Furthermore, in this class, we show that liveness, non-deadlockability and reversibility, taken together or separately, are not always monotonic, even under the assumptions of structural boundedness and structural liveness. These facts delineate more sharply the frontier between monotonicity and non-monotonicity of the behavior in weighted Petri nets, present already in the join-free subclass. In addition, we use part of this new material to correct a flaw in the proof of a previous characterization of monotonic liveness and boundedness for homogeneous asymmetric-choice nets, published in 2004 and left unnoticed. Show more

Keywords: Structural analysis, Weighted Petri net, Deadlockability, Liveness, Reversibility, Boundedness, Monotonicity, Fork-attribution, Join-free, Communication-free, Synchronization-free, Asymmetric-choice

DOI: 10.3233/FI-2018-1708

Citation: Fundamenta Informaticae, vol. 161, no. 4, pp. 383-421, 2018

Authors: Wolf, Karsten

Article Type: Research Article

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

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