Fundamenta Informaticae - Volume 137, issue 1

Authors: Colom, José Manuel | Desel, Jörg | Kleijn, Jetty

Article Type: Other

DOI: 10.3233/FI-2015-1167

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. v-vi, 2015

Authors: Fraca, Estíbaliz | Haddad, Serge

Article Type: Research Article

Abstract: At the end of the eighties, continuous Petri nets were introduced for: (1) alleviating the combinatory explosion triggered by discrete Petri nets (i.e. usual Petri nets) and, (2) modelling the behaviour of physical systems whose state is composed of continuous variables. Since then several works have established that the computational complexity of deciding some standard behavioural properties of Petri nets is reduced in this framework. Here we first establish the decidability of additional properties like coverability, boundedness and reachability set inclusion. We also design new decision procedures for reachability and lim-reachability problems with a better computational complexity. Finally we provide …lower bounds characterising the exact complexity class of the reachability, the coverability, the boundedness, the deadlock freeness and the liveness problems. A small case study is introduced and analysed with these new procedures. Show more

Keywords: Continuous Petri nets, structural analysis, complexity

DOI: 10.3233/FI-2015-1168

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. 1-28, 2015

Authors: Geeraerts, Gilles | Heußner, Alexander | Praveen, M. | Raskin, Jean-François

Article Type: Research Article

Abstract: We introduce ω-Petri nets (ωPN), an extension of plain Petri nets with ω-labeled input and output arcs, that is well-suited to analyse parametric concurrent systems with dynamic thread creation. Most techniques (such as the Karp and Miller tree or the Rackoff technique) that have been proposed in the setting of plain Petri nets do not apply directly to ωPN because ωPN define transition systems that have infinite branching. This motivates a thorough analysis of the computational aspects of ωPN. We show that an ωPN can be turned into a plain Petri net that allows us to recover the reachability set …of the ωPN, but that does not preserve termination (an ωPN terminates iff it admits no infinitely long execution). This yields complexity bounds for the reachability, boundedness, place boundedness and coverability problems on ωPN. We provide a practical algorithm to compute a coverability set of the ωPN and to decide termination by adapting the classical Karp and Miller tree construction. We also adapt the Rackoff technique to ωPN, to obtain the exact complexity of the termination problem. Finally, we consider the extension of ωPN with reset and transfer arcs, and show how this extension impacts the decidability and complexity of the aforementioned problems. Show more

DOI: 10.3233/FI-2015-1169

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. 29-60, 2015

Authors: Mayr, Ernst W. | Weihmann, Jeremias

Article Type: Research Article

Abstract: We investigate several computational problems of communication-free Petri nets, and develop very efficient (mostly linear time) algorithms for different variations of the boundedness and liveness problems of cf-PNs. For several more complex notions of boundedness, as well as for the covering problem, we show NP-completeness. In the last part, we use our results for cf-PNs to give linear time algorithms for related problems of context-free (commutative) grammars, and, in turn, use known results for such grammars to give a coNEXPTIME-upper bound for the equivalence problem of cf-PNs.

DOI: 10.3233/FI-2015-1170

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. 61-86, 2015

Authors: Marechal, Alexis | Buchs, Didier

Article Type: Research Article

Abstract: Modularity is a mandatory principle to apply Petri nets to real world-sized systems. Modular extensions of Petri nets allow to create complex models by combining smaller entities. They facilitate the modeling and verification of large systems by applying a divide and conquer approach and promoting reuse. Modularity includes a wide range of notions such as encapsulation, hierarchy and instantiation. Over the years, Petri nets have been extended to include these mechanisms in many different ways. The heterogeneity of such extensions and their definitions makes it difficult to reason about their common features at a general level. We propose in this …article an approach to standardize the semantics of modular Petri nets formalisms, with the objective of gathering even the most complex modular features from the literature. This is achieved with a new Petri nets formalism, called the LLAMAS Language for Advanced Modular Algebraic Nets (LLAMAS). We focus principally on the composition mechanism of LLAMAS, while introducing the rest of the language with an example. The composition mechanism is introduced both informally and with formal definitions. Our approach has two positive outcomes. First, the definition of new formalisms is facilitated, by providing common ground for the definition of their semantics. Second, it is possible to reason at a general level on the most advanced verification techniques, such as the recent advances in the domain of decision diagrams. Show more

Keywords: System design and verification, Modularity, High-Level Petri nets, Standardization, Composition Mechanism, LLAMAS

DOI: 10.3233/FI-2015-1171

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. 87-116, 2015

Authors: Bergenthum, Robin | Lorenz, Robert

Article Type: Research Article

Abstract: In this paper we tackle the problem of verifying whether a scenario is executable in a Petri net. In contrast to sequentially ordered runs, a scenario includes both information about dependencies and independencies of events. Consequently, a scenario allows a precise and intuitive specification of a run of a concurrent or distributed system. In this paper we consider Petri nets with arc weights, namely marked place/transition-nets (p/t-nets) and p/t-nets with inhibitor arcs (pti-nets). A scenario of a p/t-net is a labelled partial order (lpo). A scenario of a pti-net is a labelled stratified order structure (lso). Accordingly, the question is …either whether a given lpo is in the language of a given p/t-net or whether an lso is in the language of a given pti-net. Different approaches exist to define the partial language of a Petri net. Each definition yields a different verification algorithm, but existing algorithms perform quite poorly in terms of runtime for most examples. We introduce a new compact characterization of the partial language of a Petri net. This characterization is optimized with respect to the verification problem. The paper is a revised and extended version of the conference paper [10]. Show more

DOI: 10.3233/FI-2015-1172

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. 117-142, 2015

Authors: Fernandes, Johnson | Koutny, Maciej | Mikulski, Łukasz | Pietkiewicz-Koutny, Marta | Sokolov, Danil | Yakovlev, Alex

Article Type: Research Article

Abstract: A concurrent system is persistent if throughout its operation no activity which became enabled can subsequently be prevented from being executed by any other activity. This is often a highly desirable (or even necessary) property; in particular, if the system is to be implemented in hardware. Over the past 40 years, persistence has been investigated and applied in practical implementations assuming that each activity is a single atomic action which can be represented, for example, by a single transition of a Petri net. In this paper we investigate the behaviour of GALS (Globally Asynchronous Locally Synchronous) systems in the context …of VLSI circuits. The specification of a system is given in the form of a Petri net. Our aim is to re-design the system to optimise signal management, by grouping together concurrent events. Looking at the concurrent reachability graph of the given Petri net, we are interested in discovering events that appear in ‘bundles’, so that they all can be executed in a single clock tick. The best candidates for bundles are sets of events that appear and re-appear over and over again in the same configurations, forming ‘persistent’ sets of events. Persistence was considered so far only in the context of sequential semantics. In this paper, we move to the realm of step based execution and consider not only steps which are persistent and cannot be disabled by other steps, but also steps which are nonviolent and cannot disable other steps. We then introduce a formal definition of a bundle and propose an algorithm to prune the behaviour of a system, so that only bundled steps remain. The pruned reachability graph represents the behaviour of a re-engineered system, which in turn can be implemented in a new Petri net using the standard techniques of net synthesis. The proposed algorithm prunes reachability graphs of persistent and safe nets leaving bundles that represent maximally concurrent steps. Show more

Keywords: asynchronous and synchronous circuit, GALS system, persistence, nonviolence, step transition system, step semantics, Petri net

DOI: 10.3233/FI-2015-1173

Citation: Fundamenta Informaticae, vol. 137, no. 1, pp. 143-170, 2015