Search

Assuming that the behavioural specification of a concurrent system is given in the form of a step transition system, where the arcs between states are labelled by steps (multisets of executed actions), we focus on the problem of synthesising a Petri net generating a reachability graph isomorphic to a given step transition system. To deal with step transition systems more complicated than those generated by standard Place/Transition nets, we consider in this paper Petri nets with wholeplace operations, localities, and a/sync places. We adapt and extend the general approach developed within the framework ofτ-nets and the theory of regions of step transition systems. Building on the results presented in [23], emphasis here is on the role of a/sync places with their potential for an instantaneous transfer of tokens within a step. In a series of results we demonstrate the robustness of the notion of region for Petri net synthesis. [ABSTRACT FROM AUTHOR]

A step trace is an equivalence class of step sequences which can be thought of as different observations of the same underlying concurrent history. Equivalence is determined on basis of a step alphabet that describes the relations between events in terms of potential simultaneity and sequentialisability. Step traces cannot be represented by standard partial orders, but require so-called invariant structures, extended order structures that capture the phenomena of mutual exclusion and weak causality. In this paper, we present an effective way of deciding whether an invariant structure represents a step trace over a given step alphabet. We also describe a method by which one can check whether a given invariant structure can represent a step trace over any step alphabet. Moreover, if the answer is positive, the method provides a suitable step alphabet. [ABSTRACT FROM AUTHOR]

Both Petri nets and differential equations are important modeling tools for biological processes. In this paper we demonstrate how these two modeling techniques can be combined to describe biological gradient formation. Parameters derived from partial differential equation describing the process of gradient formation are incorporated in an abstract Petri net model. The quantitative aspects of the resulting model are validated through a case study of gradient formation in the fruit fly. [ABSTRACT FROM AUTHOR]

Automated synthesis from behavioural specifications is an attractive way of constructing computational systems. In this paper, we look at a specific instance of this approach which aims at constructing GALS (globally asynchronous locally synchronous) systems. GALS systems are represented by Petri nets with localities, each locality defining a set of co-located actions, and specifications are given in terms of transition systems with arcs labelled by steps of executed actions. The proposed synthesis procedures are based on the regions of transition systems, and work without knowing which actions are to be co-located. We consider two basic classes of Petri nets, viz. Elementary Net System with Localities (ENL-system) and Place/Transition nets with localities (PTL-nets). In particular, we discuss ENL-systems where there is no conflict between events coming from different localities. In such a case, the synthesis problem reduces to checking just one co-location relation. This result is then extended to PTL-nets. Keywords: concurrency, Petri nets, localities, GALS, net synthesis, step sequence semantics, transition systems, theory of regions, conflict. [ABSTRACT FROM AUTHOR]

Recently, opacity has proved a promising technique for describing security properties. Much of the work has been couched in terms of Petri nets. Here, we extend the notion of opacity to the model of labelled transition systems and generalise opacity in order to better represent concepts from the literature on information flow. In particular, we establish links between opacity and the information flow concepts of anonymity and non-inference. We also investigate ways of verifying opacity when working with Petri nets. Our work is illustrated by two examples, one describing anonymity in a commercial context, and the other modelling requirements upon a simple voting system. [ABSTRACT FROM AUTHOR]

Abstract: Membrane systems (with promoters and inhibitors) are a computational model inspired by the way living cells are divided by membranes into compartments where chemical reactions may take place. We consider synchrony and asynchrony between executed reactions in the computations of such systems using Petri nets and their processes as a formal behavioural model. We first discuss different definitions of individual computational steps, and show how they can be rendered within the Petri net domain by assigning all transitions localities corresponding to the compartments, and using activator and inhibitor arcs. The non-sequential semantics of the resulting nets is formalised through processes based on occurrence nets augmented with additional information about localities and activator/inhibitor arcs. Such processes provide a convenient tool for analysing synchrony and asynchrony in the executions of membrane systems and shed light on the causal relationships between the reactions taking place. [Copyright &y& Elsevier]

We are concerned with causality semantics in the executions of Petri nets with range arcs. Range arcs combine (and subsume) the distinctive features of inhibitor and activator arcs, and each such arc provides a means of specifying a range (a finite or infinite interval of non-negative integers) for the number of tokens in a place which makes enabling of a given transition possible. We demonstrate that the existing treatment of causality developed for Petri nets with inhibitor arcs based on structures generalising partial orders can also be applied to nets with range arcs. [ABSTRACT FROM AUTHOR]

In this paper we propose a translation into high level Petri nets of the terms of a finite fragment of the π-calculus. Our construction renders in a compositional way the control flow aspects present in π-calculus process expressions, by adapting the existing graph-theoretic net composition operators. Those aspects which are related to term rewriting, as well as name binding, are handled through special inscriptions of places, transitions and arcs, together with a suitable choice of the initial marking. [ABSTRACT FROM AUTHOR]

The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for logic synthesis based on the Incremental Boolean Satisfiability (SAT) approach. Experimental results show that this technique leads not only to huge memory savings when compared with the methods based on reachability graphs, but also to significant speedups in many cases, without affecting the quality of the solution. [ABSTRACT FROM AUTHOR]

The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is that of identifying whether an STG satisties the Complete State Coding (CSC) requirement (which states that semantically different reachable states must have different binary encodings), and, if necessary, modifying the STG (by. e.g., inserting new signals helping to trace the current state) to meet this requirement. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for detection of CSC conflicts based on the Boolean Satisfiability (SAT) approach. Following the basic formulation of the state encoding conflict relationship, we present some problem-specific optimization rules. Experimental results show that this technique leads not only to huge memory savings when compared to the CSC conflicts detection methods based on reachability graphs, but also to significant speedups in many cases. [ABSTRACT FROM AUTHOR]

Abstract: interval temporal logic (itl) and Petri nets are two well developed formalisms for the specification and analysis of concurrent systems. itl allows one to specify both the system design and correctness requirements within the same logic based on intervals (sequences of states). As a result, verification of system properties can be carried out by checking that the formula describing a system implies the formula describing a requirement. Petri nets, on the other hand, have action and local state based semantics which allows for a direct expression of causality aspects in system behaviour. As a result, verification of system properties can be carried out using partial order reductions or invariant based techniques. In this paper, we investigate a basic semantical link between temporal logics and compositionally defined Petri nets. In particular, we aim at providing a support for the verification of behavioural properties of Petri nets using methods and techniques developed for itl. [Copyright &y& Elsevier]