Fundamenta Informaticae - Volume 146, issue 1

Authors: Devillers, Raymond | Valmari, Antti | Penczek, Wojciech

Article Type: Other

DOI: 10.3233/FI-2016-1373

Citation: Fundamenta Informaticae, vol. 146, no. 1, pp. v-vi, 2016

Authors: Triebel, Marvin | Sürmeli, Jan

Article Type: Research Article

Abstract: One way to express correctness of a Petri net N is to specify a linear inequality U , requiring each reachable marking of N to satisfy U . A linear inequality U is stable if it is preserved along steps. If U is stable, then verifying correctness reduces to checking U in the initial marking of N . In this paper, we characterize classes of stable linear inequalities of a given Petri net by means of structural properties. We generalize classical results on traps, co-traps, and invariants. We show how to decide stability of …a given inequality. For a certain class of inequalities, we present a polynomial time decision procedure. Furthermore, we show that stability is a local property and exploit this for the analysis of asynchronously interacting open net structures . Finally, we study the summation of inequalities as means of deriving valid inequalities. Show more

Keywords: Petri net analysis, inductive invariants, linear inequalities, stable properties, traps, co-traps, invariants

DOI: 10.3233/FI-2016-1374

Citation: Fundamenta Informaticae, vol. 146, no. 1, pp. 1-34, 2016

Authors: Badouel, Eric | Hélouët, Loïc | Morvan, Christophe

Article Type: Research Article

Abstract: This paper considers Structured Data Nets (StDN): a Petri net extension that describes open systems with data. The objective of this language is to serve as a formal basis for the analysis of systems that use data, accept inputs from their environment, and implement complex workflows. In StDNs, tokens are structured documents. Each transition is attached to a query, guarded by patterns, (logical assertions on the contents of its preset) and transforms tokens. We define StDNs and their semantics. We then consider their formal properties: coverability of a marking, termination and soundness of transactions. Unrestricted StDNs are Turing complete, so …coverability, termination and soundness are undecidable for StDNs. However, using an order on documents, and putting reasonable restrictions both on the expressiveness of patterns and queries and on the documents, we show that StDNs are well-structured transition systems, for which coverability, termination and soundness are decidable. We then show the expressive power of StDN on a case study, and compare StDNs and their decidable subclasses with other types of high-level nets and other formalisms adapted to data-centric approaches or to workflows design. Show more

Keywords: Petri nets, Well-Quasi Orders, Structured Data

DOI: 10.3233/FI-2016-1375

Citation: Fundamenta Informaticae, vol. 146, no. 1, pp. 35-82, 2016

Authors: Hujsa, Thomas | Delosme, Jean-Marc | Munier-Kordon, Alix

Article Type: Research Article

Abstract: Weighted Petri nets provide convenient models of many man-made systems. Real applications are often required to possess the fundamental Petri net properties of liveness and reversibility, as liveness preserves all the functionalities (fireability of all transitions) of the system and reversibility lets the system return to its initial state (marking) using only internal operations. Characterizations of both behavioral properties, liveness and reversibility, are known for well-formed weighted Choice-Free and ordinary Free-Choice Petri nets, which are special cases of Equal-Conflict Petri nets. However, reversibility is not well understood for this larger class, where choices must share equivalent preconditions, although characterizations …of liveness are known. In this paper, we provide the first characterization of reversibility for all live Equal-Conflict Petri nets by extending, in a weaker form, a known condition that applies to the Choice-Free and Free-Choice subclasses. We deduce the monotonicity of reversibility in the live Equal-Conflict class. We also give counter-examples for other classes where the characterization does not hold. Finally, we focus on well-formed Equal-Conflict Petri nets, for which we offer the first polynomial sufficient conditions for liveness and reversibility, contrasting with the previous exponential time conditions. Show more

Keywords: Reversibility, liveness, Equal-Conflict, Petri net, characterization, polynomial time sufficient condition, polynomial markings

DOI: 10.3233/FI-2016-1376

Citation: Fundamenta Informaticae, vol. 146, no. 1, pp. 83-119, 2016