Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 9

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  Time Petri Net
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Time-independent Liveness in Time Petri Nets
EN
In this paper we consider a class of Time Petri nets defined by structural restrictions. Each Time Petri net which belongs to this class has the property that their liveness behaviour does not depend on the time. Therefore, the Time Petri net is live when its skeleton is live.
2
Content available remote Expressiveness of Petri Nets with Stopwatches. Discrete-time Part
EN
With this contribution, we aim to draw a comprehensive classification of Petri nets with stopwatches w.r.t. expressiveness and decidability issues. This topic is too ambitious to be summarized in a single paper. That is why we present our results in two different parts. In the first part of our work, we established new results regarding to both dense-time and discrete-time semantics. We now focus on the discrete-time specificities. We address the class of bounded Petri nets with stopwatches and reset arcs (rSwPNs), which is an extension of T-time Petri nets (TPNs) where time is associated with transitions. Stopwatches can be reset, stopped and started. We recall the formal dense-time and discrete-time semantics of these models in terms of Transition Systems. We study the expressiveness of rSwPNs and its subclasses w.r.t. (weak) bisimilarity (behavioral semantics). The main results are following: 1) Discrete-time bounded TPNs, discrete-time bounded rSwPNs and untimed Petri nets are equally expressive; 2) The resulting (final) classification of models is given by a set of relations explained in Fig. 7. While investigating expressiveness, we exhibit proofs that can be easily extended to the resolution of decidability issues. Among other results, we prove that, for bounded rSwPNs, the state and marking reachability problems - undecidable with dense-time semantics - are decidable when discrete-time is considered. Table 1 gives a synthesis of the main decidability results for these models. For the sake of simplicity, our results are explained on a model such that the stopwatches behaviors are expressed using inhibitor arcs. Our conclusions can however be easily extended to the general class of Stopwatch Petri nets.
3
Content available remote Expressiveness of Petri Nets with Stopwatches. Dense-time Part
EN
With this contribution, we aim to draw a comprehensive classification of Petri nets with stopwatches w.r.t. expressiveness and decidability issues. This topic is too ambitious to be summarized in a single paper. That is why we present our results in two different parts. The scope of this first paper is to address the general results that apply for both dense-time and discrete-time semantics. We study the class of bounded Petri nets with stopwatches and reset arcs (rSwPNs), which is an extension of T-time Petri nets (TPNs) where time is associated with transitions. Stopwatches can be reset, stopped and started. We give the formal dense-time and discrete-time semantics of these models in terms of Transition Systems. We study the expressiveness of rSwPNs and its subclasses w.r.t. (weak) bisimilarity (behavioral semantics). The main results are following: 1) bounded rSw- PNs and 1-safe rSwPNs are equally expressive; 2) For all models, reset arcs add expressiveness. 3) The resulting partial classification of models is given by a set of relations explained in Fig. 7: in the forthcoming paper, we will complete these results by covering expressiveness and decidability issues when discrete-time nets are considered. For the sake of simplicity, our results are explained on a model such that the stopwatches behaviors are expressed using inhibitor arcs. Our conclusions can however be easily extended to the general class of Stopwatch Petri nets.
4
Content available remote Towards Building the State Class Graph of the TSPN Model
EN
In this paper, we propose an enumerative approach to build the state class graph of the TSPN (Time Stream Petri Net) model. A TSPN model is a Petri net augmented with intervals on arcs and synchronization rules on transitions. It can be used to model complex systems, and it is proved to be more expressive than TPN (Time Petri Nets). In contrast with TPN where each class accessible in the graph is given as a pair (M,D) where M is a marking and D is a system of DBM inequalities, a TSPN class in this form is much complex to compute. To tackle this issue, we introduce a new formalism called the time distance function to define a TSPN class. This function makes it possible to determine an efficient algorithm to compute each class of the graph in a square complexity time. Finally, we show how to exploit the TSPN state class graph (when finite), to check over either linear properties of the model, or to compute minimal and maximal time distances of any firing sequence.
5
Content available remote On the Compared Expressiveness of Arc, Place and Transition Time Petri Nets
EN
In this paper, we consider safe Time Petri Nets where time intervals (strict and large) are associated with places (P-TPN), arcs (A-TPN) or transitions (T-TPN). We give the formal strong and weak semantics of these models in terms of Timed Transition Systems. We compare the expressiveness of the six models w.r.t. (weak) timed bisimilarity (behavioral semantics). The main results of the paper are : (i) with strong semantics, A-TPN is strictly more expressive than P-TPN and T-TPN ; (ii) with strong semantics P-TPN and T-TPN are incomparable ; (iii) T-TPN with strong semantics and T-TPN with weak semantics are incomparable. Moreover, we give a complete classification by a set of 9 relations explained in Fig. 19 (p. 247).
EN
We consider here time Petri nets (TPN model). We first propose an abstraction to its generally infinite state space which preserves linear properties of the TPN model. Comparing with TPN abstractions proposed in the literature, our abstraction produces graphs which are both smaller and faster to compute. In addition, our characterization of agglomerated states allows a significant gain in space. Afterwards, we show how to apply Yoneda's partial order reduction technique to construct directly reduced graphs useful to verify LTL_x properties of the model. Using our approach, both time and space complexities are reduced. Finally, we propose a time extension for Büchi automata which is useful to model checking timed linear properties of the model, using the abstraction proposed here.
7
Content available remote Time Petri Nets for Modelling and Analysis of Biochemical Networks
EN
Biochemical networks are modelled at different abstraction levels. Basically, qualitative and quantitative models can be distinguished, which are typically treated as separate ones. In this paper, we bridge the gap between qualitative and quantitative models and apply time Petri nets for modelling and analysis of molecular biological systems. We demonstrate how to develop quantitative models of biochemical networks in a systematic manner, starting from the underlying qualitative ones. For this purpose we exploit the well-established structural Petri net analysis technique of transition invariants, which may be interpreted as a characterisation of the system's steady state behaviour. For the analysis of the derived quantitative model, given as time Petri net, we present structural techniques to decide the time-dependent realisability of a transition sequence and to calculate its shortest and longest time length. All steps of the demonstrated approach consider systems of integer linear inequalities. The crucial point is the total avoidance of any state space construction. Therefore, the presented technology may be applied also to infinite systems, i.e. unbounded Petri nets.
8
Content available remote Disassembly Scheduling with Parts Commonality Using Petri Nets with Timestamps
EN
This paper considers the application of Petri nets with timestamps to the problem of disassembly scheduling with parts commonality, which is the problem of determining time and quantity of ordering the used product to fulfill the demands of individual disassembled parts. Unlike the simple case, parts commonality creates dependencies of components and makes them difficult to solve. A comparison of methods using an example problem from a previous research shows that the method suggested in this paper is much simpler and more extendable than the previous one. Also, we show that the solutions obtained from the previous algorithm are not optimal in general.
9
Content available remote Analyzing paths in Time Petri Nets
EN
In this paper, a parametric description of a transition sequence in a Time Petri net is introduced. The minimal and maximal time duration of a transition sequence are shown to be integers and furthermore the mni/max path passes only integer-states. A necessary condition for the reachability of an arbitrary state is given.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.