articles scientifiques non accessibles?!!

[hhabla 10]

Bonjours les FAistes, je reécrit le même topic pour voir s'il y'a des membres avec accés plus important aux articles sur le net notamment le IEEE et Springer...ou d'autres qui sont un peu vieux...

J'en ai besoin ....:confused:

Merci d'avance:)

[MonGeneral75 10]

Bonjours les FAistes, je reécrit le même topic pour voir s'il y'a des membres avec accés plus important aux articles sur le net notamment le IEEE et Springer...ou d'autres qui sont un peu vieux...

J'en ai besoin ....:confused:

Merci d'avance:)

 

Bonjour,

Met les références exactes des papiers que tu veux ...

[hhabla 10]

Bonjour,

Met les références exactes des papiers que tu veux ...

 

Merci bcp mon ami,

PS: MP

[hhabla 10]

t'as pas encore de MP?? bon pas grave...

[PAX 10]

IEICE SEARCH SYSTEM

 

c'est cela??

Utilise Google scholar pour tous les textes scientifiques

[PAX 10]

Google Scholar

[hhabla 10]

IEICE SEARCH SYSTEM

 

c'est cela??

Utilise Google scholar pour tous les textes scientifiques

 

Y'a pas déja essayé!!!!!!

[hhabla 10]

IEICE SEARCH SYSTEM

 

c'est cela??

Utilise Google scholar pour tous les textes scientifiques

 

faut un login c payant:( je pense...

Aloooo y'a quelqu'un??

[PAX 10]

pas sur que ce soit payant, il faut s'inscrire sur le site....essaye

[samir0278 12]

Model checking of time Petri nets

Hanifa Boucheneb and Rachid Hadjidj

Department of Computer Engineering

´

Ecole Polytechnique de Montr´eal

P.O. Box 6079, Station Centre-ville

Montr´eal, Qu´ebec

{hanifa.boucheneb,rachid.hadjidj**@polymtl.ca

Abstract

This paper considers time Petri nets (TPN model) for model checking. The main challenge

in model checking techniques is to construct, with lesser resources (time and space), a

muchcoarserabstractionpreservingpropertiesofinterest.Thesepropertiescanbeverified

using standard model checking techniques. In this paper, we review some techniques,

proposed in the literature, to model check untimed and timed properties of the TPN.

Keywords: Time Petri nets, state explosion problem, abstraction, model checking, TCTL properties.

[samir0278 12]

1. INTRODUCTION

Temporal logic model checking is a very attractive and automatic verification technique of systems.

It is applied by representing the behavior of a system as a finite state transition system, specifying

properties of interest in a temporal logic (LTL, CTL, CTL*, MITL, TCTL) and finally exploring the

statetransition system to determine whether they hold or not. To use this technique with timed systems,

an extra e?ort is required to abstract their generally infinite state spaces. The abstraction must generate

a finite graph while preserving properties of interest. For best performances, the graph should also be

the smallest possible and computed with minor resources too (time and space). Several abstractions of

the TPN state space have been proposed in the literature which preserves di?erent kinds of properties

(reachability, LTL, MITL, CTL*, TCTL properties). The preserved properties are verified using standard

model checking techniques [1, 11, 13, 15].

This paper reviews some techniques, proposed in the literature, to model check untimed and timed

properties of the TPN. The rest of the paper is organized as follows. Section 2 introduces the TPN and

its semantics. Section 3 is devoted to the state space abstraction. Section 4 is devoted to the model

checking techniques.

[samir0278 12]

2. TIME PETRI NETS

A TPN is a Petri net with time intervals attached to its transitions. Formally, a TPN is a tuple

N = (P,T,Pre,Post,m ,Is) where P is a finite set of places, T is a finite set of transitions, such

0

1

that P nT = Ø, Pre and Post are the backward and the forward incidence functions: P ×T ? N ,

2 + +

m : P ? N, is the initial marking, Is : T ? Q ×(Q ?{8**) associates with each transition t an

0

interval called static firing interval of t.

Let M be the set of all markings of a TPN, m ? M a marking, and t,t

? T two transitions. t is said

f

to be enabled in m, i? all tokens required for its firing are present in m, i.e.: ?p ? P,m(p) = Pre(p,t).

We denote by En(m) the set of all transitions enabled in m. If m results from firing transition t from

f

another marking, New(m,t ) denotes the set of all transitions newly enabled in m, i.e.:

f

New(m,t ) = {t ? En(m)|t = t ?(?p ? P,m(p) Post(p,t ) < Pre(p,t))**.

f f f

There are two known characterizations of the TPN state. The first one, based on clocks, associates with

each transition t of the model a clock to measure the time elapsed since t became enabled most recently

[7, 8, 13, 18]. The TPN clock state is a couple (m,v), where m is a marking and v is a clock valuation

+

function, v : En(m) ? R . When a transition t becomes enabled, its clock is initialized to zero. The

value of this clock increases synchronously with time until t is fired or disabled by the firing of another

1

N is the set of nonnegative integers.

2 +

Q is the set of nonnegative rational numbers.

[samir0278 12]

transition. t can fire, if the value of its clock is inside its static firing interval Is(t) = [tmin(t),tmax(t)].

It must be fired immediately, without any additional delay, when the clock reaches tmax(t). The second

characterization, based on intervals, defines the TPN state as a marking and a function which associates

with each enabled transition a firing interval [2]. The TPN interval state is a couple (m,I), where m is

+ +

a marking and I is an interval function, I : En(m) ? Q ×(Q ?{8**). When a transition t becomes

enabled, its firing interval is set to its static firing interval Is(t). The bounds of this interval decrease

synchronously with time, until t is fired or disabled by another firing. t can fire, if the lower bound of

its firing interval reaches 0, but must be fired, without any additional delay, if the upper bound of its

firing interval reaches 0.

Despite their relatedness, the two state characterizations still show some major di?erences. The origin

of these di?erences stems from the relationship between the two characterizations of states which

can be stated as follows: Let (m,v) be a clock state. Its corresponding interval state is (m,I) such

that: ?t ? En(m),I(t) = [max(0,tmin(t) v(t)),tmax(t) v(t)]. Note that for any real value

u = tmin(t), if tmax(t) = 8, tmax(t) u = 8 and max(0,tmin(t) u) = 0. This means that

for TPN models with unbounded firing intervals, infinitely many clock states may map to the same

interval state. In such a case, all these states will obviously exhibit the same future behavior. The

same remark extends also to state classes, where several state classes based on clocks (sometimes an

infinity) may map to a single state class based on intervals. Note also that states in a clock state class

can be distinguished one by one, whereas it is impossible with an interval state class. The reason is

that the firing domain of an interval state class is the union of firing domains of all its states, and

the union is known to be an irreversible operation. Together, the mentioned remarks suggest that the

interval characterization of states has a more abstracting power than the clock characterization, and

allows to construct more compact abstractions of the TPN state space, preserving linear properties.

In addition, abstractions based on clocks do not enjoy naturally the finiteness property for bounded

TPNs with unbounded intervals as it is the case for abstractions based on intervals. The finiteness is

enforced using an approximation operation on state classes [2, 7, 10], which may involve some overhead

computation. However, abstractions based on intervals are not appropriate for constructing abstractions

preserving branching properties (ASCGs). Indeed, this construction, based on splitting state classes (a

set of states), is not possible with the characterization interval of state classes.

The semantics of the TPN can be defined using either the clock state or interval state characterization.

+

Let ? ? R be a nonnegative reel number, t a transition of T, s and s two states of a TPN. We write

? t

s ? s , i? state s is reachable from state s after a time progression of ? time units. We write s ? s

i? state s is immediately reachable from state s by firing transition t.

The state space of a TPN is defined as a structure (S,?,s ), where s is the initial state of the model,

0 0

* *

? s** is the set of reachable states (? is the reflexive and transitive closure of ?).

and S = {s|s

0

The state space of the TPN model is generally infinite and then not suitable for enumerative analysis.

Hence, further abstractions are needed.

[samir0278 12]

3. TPN STATE SPACE ABSTRACTIONS

Abstraction techniques aim to construct by removing some irrelevant details, a contraction of the state

space of the model, which preserves properties of interest. We can find, in the literature, several state

space abstractions for the TPN model. These abstractions may di?er mainly in the agglomeration

criteria of states, the characterization of states and state classes (interval states or clock states), the

kind of properties (linear or branching) they preserve and their size.

In abstractions preserving linear properties, states reachable by the same firing sequence independently

of their firing times are usually agglomerated in the same node. States reachable via time progression

may be either included (ZBG [7]) or abstracted (SCG [2], GRG [18], SSCG [2], CSZG [10]). The

agglomerated states are then considered modulo some relation of equivalence (firing domain of the

SCG [2], k-approximation of the ZBG [7], approximation of the SSCG [2], and k-normalization of the

CSZG [7]). These abstractions, except the GRG, are finite for all bounded time Petri nets. The SCG is,

in general, more smaller than others [2] and then more appropriate to model checking linear properties.

The reason is that the SCG is an interval state abstraction while the others are clock state abstractions.

In addition, we obtain coarser abstractions when we add to each state class all states reachable from

it by time progression (relaxing state classes). Indeed, two di?erent state classes may have identical

relaxed state class. As an example, consider the two interval state classes of a SCG a = (m,2 = t = 3)

1

[samir0278 12]

CSZG ZBG

TPN RSCG SCG CSZG SSCG ? ZBG ?

RSCG RSCG

P(2) 593/1922 748/2460 1773/6131 7963/42566 2.99/3.19 12280/42280 20.70/22

cpu(s) 0.02 0.04 0.06 0.51 3 0.49 24.5

P(3) 3240/15200 4604/21891 16600/82834 122191/1111887 5.12/5.45 ? -

cpu(s) 0.14 0.40 1.73 20.04 12.36 -

P(4) 9504/56038 14086/83375 68451/429014 659377/7987583 7.20/7.66 ? -

cpu(s) 0.62 1.83 12.15 183.87 19.60 -

P(5) 20877/145037 31657/217423 196707/1447269 9.42/9.98 - ? -

cpu(s) 2.01 5.67 51.04 25.40 -

TABLE 1: Comparison of di?erent abstractions

[samir0278 12]

and a = (m,1 = t = 3). We have relax(a ) = relax(a ) = (m,0 = t = 3) while a= a . As an

2 1 2 1 2

3

example, we report in table 1 sizes and computing times of the RSCG , SCG, SSCG, CSZG and ZBG

for some producer and consumer model. A question mark in the table indicates a situation where the

computation has not completed after an hour of time, or aborted due to a lack of memory.

Abstractions preserving branching properties (CTL* properties) are built using a partition refinement

technique [14] in two steps [2, 3, 4, 8, 9, 10, 13, 18]. An abstraction, which does not necessarily

preserve branching properties, is first built then refined in order to restore the condition AE, i.e.: 4

?(a,t,a ) ?=? , (a ? Pred(a ,t)), where Pred(a ,t) is the set of all states which may lead after

possibly some time progression and firing transition t to some states in a . To verify the atomicity of

class a for the transition (a,t,a ), it su?ces to verify that a is equal or included in Pred(a ,t). In

case a is not atomic, it is partitioned into a set of convex subclasses so as to isolate the predecessors

of a by t in a, from those which are not. This refinement operation is repeated until all state classes

are atomic. The refinement process generates a finite graph i? the intermediate abstraction is finite

[2, 3]. The intermediate abstractions used in the literature are all based on clock states but may

di?er in agglomeration criteria of states and state classes (equality [2, 18] , inclusion [3, 4] or convex-

combination [9, 10]). The choice of the abstraction to be refined has a significant impact on the

refinement process. Indeed, in [6, 10], authors showed that the refinement process is significantly

improved when we use coarser abstractions. Such abstractions may be obtained using relaxation,

inclusion or convex-combination as an additional agglomeration criterium of state classes. Experimental

results have shown an important reduction in refinement times (more than ten times for some tested

models) and memory usage, resulting in graphs closer in size to the optimal. Despite the simplicity of

the used models, they allowed to illustrate some interesting features related to the computation pattern

followed by the refinement procedure, depending on which abstraction is refined. If an inclusion or a

5

convex-combination abstraction is used, the refinement follows a linear pattern . When an abstraction

preserving linear properties is refined, the size of the computed graph starts first to grow up to a peek

size then decreases until an atomic state class space is obtained. In certain cases, the peek size grows

out of control, leading to a state explosion (see figure 1.S(5)).

[samir0278 12]

4. MODEL CHECKING TIMED PROPERTIES

To verify some timed properties, in [14], authors used observers to express them in the form of TPNs

andreducethemto reachability properties. However, properties onmarkings arequitedi?cult toexpress

with observers [14]. Other techniques define translation procedures from the TPN model into timed

automata [5, 12], in order to make use of available model checking tools [11, 13, 15]. Model checking

is then performed on the resulting timed automata, with results interpreted back on the original TPN

model. The translation into timed automata may be either structural (each transition is translated into

a timed automata using the same pattern) [5] or semantic (the state class graph of the TPN is first

*

constructed and then translated into a timed automaton)[9]. Such translations show that CTL , TCTL,

LTL, MITL model checking are decidable for bounded TPNs and that developed algorithms on timed

automata may be extended to TPNs. Though e?ective, these techniques face the di?culty to interpret

back and forth properties between the two models.

Virbitskaite and Pokozy in [17] proposed a method to model check TCTL properties on TPN. The

method is based on the region graph method and is similar to the one proposed by Alur [1] for timed

3

RSCG is computed like SCG but each computed state class is relaxed before comparing it with other computed state

classes.

[samir0278 12]

3

RSCG is computed like SCG but each computed state class is relaxed before comparing it with other computed state

classes.

4

Relation =? is the transition relation of the abstraction.

5

The size of the graph grows linearly in time during its construction

[samir0278 12]

j'espère que c'est ça que vous chercher.

[Guest Black Hawk]

Bonjours les FAistes, je reécrit le même topic pour voir s'il y'a des membres avec accés plus important aux articles sur le net notamment le IEEE et Springer...ou d'autres qui sont un peu vieux...

J'en ai besoin ....:confused:

Merci d'avance:)

 

Donne-moi les titres des articles que tu cherches

[hhabla 10]

Model checking of time Petri nets

Hanifa Boucheneb and Rachid Hadjidj

Department of Computer Engineering

´

Ecole Polytechnique de Montr´eal

P.O. Box 6079, Station Centre-ville

Montr´eal, Qu´ebec

{hanifa.boucheneb,rachid.hadjidj**@polymtl.ca

Abstract

This paper considers time Petri nets (TPN model) for model checking. The main challenge

in model checking techniques is to construct, with lesser resources (time and space), a

muchcoarserabstractionpreservingpropertiesofinterest.Thesepropertiescanbeverified

using standard model checking techniques. In this paper, we review some techniques,

proposed in the literature, to model check untimed and timed properties of the TPN.

Keywords: Time Petri nets, state explosion problem, abstraction, model checking, TCTL properties.

 

Merci, mais celui la je l'ai y'a longtemps, et je l'ai gardé!!!merci mon ami, c celui de dessus qui me complique la vie:boxing:

[hhabla 10]

Donne-moi les titres des articles que tu cherches

 

Re, si t la répond moi ;)

je te l'envoi par MP???:o

[Guest Black Hawk]

Re, si t la répond moi ;)

je te l'envoi par MP???:o

 

Oui je suis là mais je n'ai pas d'MP :confused::D

[hhabla 10]

Donne-moi les titres des articles que tu cherches

 

MP pas possible ?!! t'en a pas?, cmt faire missiouuuuuuuuuuuu

[hhabla 10]

Oui je suis là mais je n'ai pas d'MP :confused::D

 

Je viens de voir ça!!prkoi?? et cmt je fé moi?heinnnnnnnn:confused::04: