Muutke küpsiste eelistusi

Petri Nets: Fundamental Models, Verification and Applications [Kõva köide]

Edited by
  • Formaat: Hardback, 656 pages, kõrgus x laius x paksus: 234x155x38 mm, kaal: 1021 g
  • Ilmumisaeg: 10-Jul-2009
  • Kirjastus: ISTE Ltd and John Wiley & Sons Inc
  • ISBN-10: 1848210795
  • ISBN-13: 9781848210790
Teised raamatud teemal:
Petri Nets: Fundamental Models, Verification and ApplicationsSuurem pilt
  • Formaat: Hardback, 656 pages, kõrgus x laius x paksus: 234x155x38 mm, kaal: 1021 g
  • Ilmumisaeg: 10-Jul-2009
  • Kirjastus: ISTE Ltd and John Wiley & Sons Inc
  • ISBN-10: 1848210795
  • ISBN-13: 9781848210790
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9781848210790.html
Märksõnad:
A Petri net is a mathematical representation of a network. This book first introduces the basic models including time and stochastic extensions, in particular place-transition and high level Petri nets. Their modeling and design capabilities are illustrated by a set of representations of interest in operating and communication systems. The volume then addresses the related verification problems and proposes corresponding solutions by introducing the main notions needed to fully understand the behavior and properties behind Petri nets. Particular attention is devoted to how systems can be fully represented and analyzed in terms of their behavioral, time, and stochastic aspects by using the same formal approach and semantic basis. Finally, illustrative examples are presented in the important fields of interoperability in telecommunication services, programming languages, multimedia architectures, manufacturing systems, and communication protocols.

Arvustused

"We think that this volume should greatly help any designer to build the new forthcoming generation of distributed systems." (Mathematical Reviews, 2011)  

Preface xv
Introduction xvii
PART
1. FUNDAMENTAL MODELS
1(346)
Basic Semantics
3(24)
Michel Diaz
Automata or state machines
3(5)
Automata and state machine models
3(2)
Tasks and processes
5(1)
Some models
6(2)
State machines and Petri nets (PN)
8(3)
Composing state machines
8(2)
Composition and synchronization
10(1)
Concepts and definitions
11(4)
Local states and enabling
12(1)
Definition of the semantics of parallelism
12(1)
Firing transitions
13(2)
Accessibility graph or making graph
15(3)
Some basic models
18(6)
Co-begin (parallel start) and co-end (synchronized termination)
18(1)
Synchronization by a signal
18(1)
Mutual exclusion
19(2)
The reader and writer mechanisms
21(3)
Bounded buffers
24(1)
Conclusion
24(1)
Bibliography
25(2)
Application of Petri Nets to Communication Protocols
27(14)
Michel Diaz
Basic models
27(2)
A simple establishment of a connection
29(3)
Different global semantics
29(1)
Conclusion
30(2)
The alternating bit protocol (ABP): model and verification
32(4)
Loss of messages
33(1)
Modeling losses
34(2)
Communicating state machines and PNs
36(1)
Conclusion
37(1)
Bibliography
38(3)
Analysis Methods for Petri Nets
41(46)
Serge Haddad
Francois Vernadat
Introduction
41(3)
Behavioral analysis of Petri nets
44(8)
Semantics of a net
44(1)
Usual properties
45(7)
Analysis of nets by linear invariants
52(13)
Definitions and first applications
52(6)
Flow computations
58(2)
Semiflow computation
60(2)
Application of invariants to the analysis of a net
62(3)
Net reductions
65(5)
Pre-agglomeration of transitions
66(2)
Post-agglomeration of transitions
68(1)
Deletion of redundant places
69(1)
The graph of a Petri net
70(15)
General results
70(4)
State machines
74(1)
Event graph
75(2)
Free choice net
77(8)
Bibliography
85(2)
Decidability and Complexity of Petri Net Problems
87(36)
Serge Haddad
Introduction
87(2)
Decidability and complexity notions
89(3)
Theoretical results about the reachability graph
92(3)
Analysis of unbounded Petri nets
95(10)
Construction of the covering graph
95(6)
Shortest sequences
101(2)
Backward analysis
103(2)
The reachability problem
105(4)
A necessary condition for reachability
106(1)
A sufficient condition for reachability
106(3)
Extensions of Petri nets
109(7)
Netswith inhibitor arcs
109(2)
Self-modifying nets
111(2)
Recursive nets
113(3)
Languages of Petri nets
116(4)
Bibliography
120(3)
Time Petri Nets
123(40)
Bernard Berthomieu
Marc Boyer
Michel Diaz
Introduction
123(3)
Time Petri nets
126(4)
Time nets
126(1)
States and firing rule
127(1)
Set of states, schedules
128(1)
Firing domains
129(1)
Behavior characterization - state classes' method
130(8)
State classes
130(1)
Transitions between state classes
131(3)
State class equality
134(2)
Class graph
136(1)
Marking graph and class graph
137(1)
Analysis - operating the state class graph
138(6)
Analyzing behavior of time-dependent systems
138(1)
Marking reachability
139(1)
Boundedness
139(4)
Specific properties for set of markings of firing sequences
143(1)
Time-dependent analyses, existence of schedules
143(1)
Application example
144(5)
Extensions and variations
149(7)
Interpreting multi-enabled transitions
149(5)
Other time extensions
154(2)
Implementation using the Tina tool
156(2)
Tina tool
156(1)
Application example
156(2)
Conclusion
158(1)
Bibliography
159(4)
Temporal Composition and Time Stream Petri Nets
163(22)
Michel Diaz
Patrick Senac
Time, synchronization and autonomous behaviors
163(1)
Limitation of time PNs
164(1)
Temporal composition
164(1)
Temporal composition and temporal synchronization
165(3)
The semantics of ``waiting''
165(2)
Pragmatics and time assumptions
167(1)
Time stream PNs
168(9)
Definition of the model
168(1)
The different firing semantics
169(7)
Relating times behavior
176(1)
TSPN with structured streams
177(1)
Application to multimedia systems
177(5)
Jitter in streams
177(1)
Intra- and inter-stream drifts
177(2)
Modeling stream composition
179(1)
Principle of modeling multimedia systems
180(1)
Modeling multimedia scenarios
180(1)
TSPN for designing hypermedia architectures
181(1)
Conclusion
182(1)
Bibliography
182(3)
High Level Petri Nets
185(36)
Claude Girault
Jean-Francois Pradat-Peyre
Introduction
185(1)
Informal introduction to high level nets
186(10)
A client-server model
186(2)
Client distinction
188(2)
Server distinction
190(2)
Equivalent unfolded net
192(2)
Colored model for the alternate bit protocol
194(2)
Colored net definition
196(4)
Notation
196(1)
The formalismof colored nets
197(2)
Unfolding of a colored net
199(1)
Well-formed net definition
200(12)
Color domains
201(2)
Color functions
203(2)
Guards
205(2)
The formalismofwell-formed nets
207(3)
Regular nets and ordered nets
210(2)
Other high level formalisms
212(7)
Interpreted nets
212(2)
Algebraic nets
214(5)
Conclusion
219(1)
Bibliography
219(2)
Analysis of High Level Petri Nets
221(48)
Claude Girault
Jean-Francois Pradat-Peyre
Introduction
221(1)
The symbolic reachability graph
222(16)
Symbolic markings
223(2)
Symbolic marking representation
225(5)
Symbolic firing rule
230(4)
Example of a symbolic reachability graph
234(4)
Properties of the SRG
238(1)
Colored invariants
238(15)
Definition of invariants of high level Petri nets
239(3)
Computing flows of a high level net: principles and difficulties
242(1)
Computing a non-parametrized generative flow family
243(7)
Parametrized generative family of flows for regular nets
250(2)
Computation of positive flows
252(1)
Structural reductions
253(12)
Principles of extension to high level nets
254(1)
Pre-agglomeration and post-agglomeration of transitions
255(6)
Deletion of an implicit place
261(1)
Application examples
261(4)
Conclusion
265(1)
Bibliography
266(3)
Stochastic Petri Nets
269(34)
Serge Haddad
Patrice Moreaux
Introduction
269(2)
A stochastic semantics for discrete event systems
271(9)
The stochastic model
271(2)
Analysis with renewing theory
273(1)
Discrete time Markov chains
274(2)
Continuous time Markov chains
276(2)
Semi-Markovian processes
278(1)
Regenerative Markovian processes
279(1)
Stochastic Petri nets
280(7)
Stochastic Petri nets with general distributions
280(2)
Stochastic Petri nets with exponential distributions
282(1)
Generalized stochastic Petri nets
283(1)
Deterministic stochastic Petri nets
284(2)
Phase-type stochastic Petri nets
286(1)
Some standard analysis methods
287(11)
Research of a product form
287(3)
Bound computations
290(3)
Approximation methods
293(4)
Unbounded Petri nets
297(1)
Conclusion
298(1)
Bibliography
299(4)
Stochastic Well-formed Petri Nets
303(18)
Serge Haddad
Patrice Moreaux
Introduction
303(2)
Markovian aggregation
305(2)
Presentation of stochastic well-formed Petri nets
307(6)
The stochastic process of a well-formed Petri nets
308(1)
Definition of stochastic well-formed Petri nets
309(1)
Modeling a multiprocessor system
310(3)
From the symbolic graph to Markovian aggregation
313(5)
Verification of the aggregation condition
314(2)
Computation of the parameters of the aggregated chain
316(1)
Performance indices of the multiprocessor system
317(1)
Conclusion
318(1)
Bibliography
319(2)
Tensor Methods and Stochastic Petri Nets
321(26)
Serge Haddad
Patrice Moreaux
Introduction
321(1)
Synchronized Markov chains
322(7)
Tensor products
324(2)
Tensor sum and continuous time Markov chains
326(3)
Tensor algebra and SPN
329(5)
Synchronous decomposition of generalized stochastic Petri nets
329(3)
Asychronous decomposition of generalized stochastic Petri nets
332(1)
Tensor analysis of phase-type Petri nets
333(1)
Tensor decomposition of stochastic well-formed Petri nets
334(10)
Problems
335(1)
The specification problem
335(1)
The resolution problem
336(2)
A tensor decomposition method for SWN
338(2)
Application in the asynchronous case
340(4)
Conclusion
344(1)
Bibliography
344(3)
PART
2. VERIFICATION AND APPLICATION OF PETRI NETS
347(230)
Verification of Specific Properties
349(66)
Serge Haddad
Francois Vernadat
Introduction
349(3)
Kripke structures and transitions systems
352(2)
Temporal logic
354(17)
Syntax and semantics
354(3)
Methods evaluation
357(12)
Temporal logic and Petri nets
369(2)
Behavioral approach
371(30)
Bisimulation relations
375(10)
Weak equivalences
385(10)
Modal characterizations of behavioral equivalences
395(6)
Decidability of bismulation and of evaluation of formulas
401(10)
Undecidability results
401(6)
Decidability results
407(4)
Bibliography
411(4)
Petri Net Unfoldings - Properties
415(20)
Jean-Michel Couvreur
Denis Poitrenaud
Introduction
415(1)
Elementary concepts
416(5)
Preliminary information
416(1)
Net homomorphisms
417(1)
Occurrence nets
418(3)
Branching processes and unfoldings
421(3)
Branching processes
421(2)
Unfoldings
423(1)
Finite prefixes
424(8)
Definition
424(1)
Adequate orders and complete finite prefixes
425(2)
Verification of safety properties
427(1)
Detection of infinite behaviors
428(4)
Conclusion
432(1)
Bibliography
432(3)
Symmetry and Temporal Logic
435(26)
Serge Haddad
Jean-Michel Ilie
Introduction
435(2)
Principles of the dynamic symmetry method
437(7)
Verification ofKripke structures
437(2)
Symmetric Kripke structures
439(2)
Verification of symmetric Kripke structures
441(3)
Illustration of the dynamic symmetry method
444(13)
Presentation of the model
444(8)
Specification of the property to be verified
452(2)
Building of the symbolic synchronized product
454(3)
Efficient implementations and further work
457(1)
Conclusion
458(1)
Bibliography
459(2)
Hierarchical Time Stream Petri Nets
461(20)
Patrick Senac
Michel Diaz
Introduction
461(1)
Structured time stream Petri nets
462(6)
Motivations
462(1)
From compositition to abstraction
463(3)
Verification of temporal coherence
466(2)
Combining abstraction and temporal composition
468(6)
Modularity and abstraction of temporal behaviors
468(1)
Hierarchical time stream Petri nets
468(3)
Interrupts as a combination of abstraction and temporal composition
471(1)
HTSPN state
472(2)
Examples
474(3)
Modeling hypermedia systems
474(1)
A solution to ``lip-synchronization'' using HTSPNs
475(2)
Conclusion
477(1)
Bibliography
478(3)
Petri Nets and Linear Logic
481(20)
Brigitte Pradin
Robert Valette
Nicolas Riviere
Introduction
481(2)
Linear logic
483(2)
Bases: a logic which handles resources
483(1)
Connectors and their interpretation
483(1)
Sequent calculus
484(1)
Petri nets and linear logic
485(5)
Various approaches
485(1)
Approach with marking
486(2)
Equivalence between reachability in a Petri net and provability of one sequent in linear logic
488(2)
Sequent labeling and graph of precedence relations
490(3)
Labeling
490(1)
Graph of precedence relations
491(1)
Conflicts of transitions and tokens
492(1)
Temporal evaluation of scenarios
493(6)
Introduction
493(1)
Simple temporal networks
494(2)
Temporal labeling
496(3)
Conclusion
499(1)
Bibliography
500(1)
Modeling of Multimedia Architectures: the Case of Videoconferencing with Guaranteed Quality of Service
501(26)
Philippe Owezarski
Marc Boyer
Introduction
501(1)
Problems of multimedia synchronization
502(5)
Multimedia information: characteristics and requirements
502(3)
Asynchronous distributed systems
505(2)
Modeling of multimedia synchronization constraints
507(5)
Modeling requirements
507(3)
Modeling example for a videoconference application
510(2)
Modeling of a synchronization architecture
512(10)
Introduction
512(1)
Modeling of a videoconference application
512(4)
Using a partial order transport
516(6)
Conclusion
522(1)
Bibliography
523(4)
Performance Evaluation in Manufacturing Systems
527(50)
Isabel Demongodin
Nathalie Sauer
Laurent Truffet
Introduction
527(1)
Modeling of manufacturing systems
528(16)
Discrete event systems aspects
529(4)
Cyclic aspects
533(5)
High throughput aspects
538(5)
Weighted marked graphs
543(1)
Evaluation of manufacturing systems
544(15)
Performance evaluation methods
544(5)
Deterministic and stochastic discrete marked graphs
549(2)
Discrete weighted marked graphs
551(1)
Continuous weighted marked graphs
552(7)
Optimization of manufacturing systems
559(12)
Deterministic marked graphs
560(1)
Stochastic marked graphs
561(2)
Extension to deterministic weighted marked graphs
563(8)
Applications
571(1)
Conclusions
571(1)
Bibliography
572(5)
Conclusion 577(2)
List of Authors 579(2)
Index 581
Michel Diaz is director of research at the National Center of Scientific Research (CNRS), Paris, France and leads the critical computer systems research department at LAAS-CNRS, Toulouse.