Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

2 2008

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: State class graph

Sortuj według:

Ogranicz wyniki do:

Towards Building the State Class Graph of the TSPN Model

Abdelli A., Badache N.

Fundamenta Informaticae

2008

Vol. 86, nr 4

371-409

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.

A More Efficient Time Petri Net State Space Abstraction Useful to Model Checking Timed Linear Properties

Bouchene H., Rakkay H.

Fundamenta Informaticae

2008

Vol. 88, nr 4

469-495

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.