The Complexity of Synthesis of b-Bounded Petri Nets

For a fixed type of Petri nets τ, τ-SYNTHESIS is the task of finding for a given transition system A a Petri net N of type τ(τ-net, for short) whose reachability graph is isomorphic to A if there is one. The decision version of this search problem is called τ-SOLVABILITY. If an input A allows a positive decision, then it is called τ-solvable and a sought net N τ-solves A. As a well known fact, A is τ-solvable if and only if it has the so-called τ-event state separation property (τ-ESSP, for short) and the τ-state separation property (τ-SSP, for short). The question whether A has the τ-ESSP or the τ-SSP defines also decision problems. In this paper, for all b ∈ ℕ, we completely characterize the computational complexity of τ-SOLVABILITY, τ-ESSP and τ-SSP for the types of pure b-bounded Place/Transition-nets, the b-bounded Place/Transitionnets and their corresponding ℤb+1-extensions.

Set difference operation for regular Petri net languages for the producer/consumer problem with the bounded buffer

We consider a Petri net for the producer/consumer problem (one of the classical synchronization problems) with the bounded buffer of size n and the regular formal languages Ln, generated by the net. The objective of this paper is to obtain a regular expression for the set difference of languages Ln \ Lm, n > m. For this purpose, we give the finite automaton which accepts the set difference of mentioned languages, and then we use the state elimination method to obtain the regular expression in the recursive form. The main result is illustrated by the examples. In an appendix, we consider the problem with two producers and two consumers with the bounded buffer of size 1. We give a reachability graph and propose the method for obtaining the regular expression. The explicit formulas are given for the problem with two producers and one consumer and also for the problem with one producer and two consumers.

Behaviour equivalent max-plus automata for timed petri nets under open-loop race-policy semantics

Timed Petri nets and max-plus automata are well known modelling frameworks for timed discrete-event systems. In this paper we present an iterative procedure that constructs a max-plus automaton from a timed Petri net while retaining the timed behaviour. Regarding the Petri net, we essentially impose three assumptions: (a) the Petri net must be bounded, i.e, the reachability graph must be finite; (b) we interpret the Petri net with single server semantics; and (c) the Petri net operates according to the race policy, i.e., the earliest possible transition will fire and thereby possibly consume tokens required by other competing transitions. Under these assumptions we show that the proposed procedure terminates with a finite deterministic max-plus automaton that realises the same timed behaviour as the Petri net. As a variation of the plain race policy, we also consider that a subsequently designed supervisor may temporarily disable distinguished transitions. Again, we present a terminating procedure that constructs a behaviour equivalent deterministic max-plus automaton. We demonstrate by example how the latter automaton can be utilised as an open-loop model in the context of supervisor control.

Mobile Data Traffic Offloading through Opportunistic Vehicular Communications

To cope with an exponentially increasing demand on mobile data traffic in cellular network, proximity-based opportunistic vehicular communications can be exploited as a complementary mean to offload and reduce the load of cellular network. In this paper, we propose a two-phase approach for mobile data traffic offloading, which exploits opportunistic contact and future utility with user mobility. The proposed approach includes one phase of initial source selection and subsequent phase of data forwarding. In phase 1, we build a weighted reachability graph, which is a very useful high-level abstraction for studying vehicular communication over time. Then, we propose an initial source selection algorithm, named VRank, and apply it in the weight reachability graph to identify some influential vehicles to serve as initial sources according to the rank of VRank. In phase 2, we formulate the forwarding schedule problem as a global utility maximization problem, which takes heterogeneous user interest and future utility contribution into consideration. Then, we propose an efficient scheme MGUP to solve the problem by providing a solution that decides which object should be broadcast. The effectiveness of our algorithm is verified through extensive simulation using real vehicular trace.