Muutke küpsiste eelistusi

E-raamat: Petri Net Algebra

Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 159,93 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

In modern society services and support provided by computer-based systems have become ubiquitous and indeed have started to fund amentally alter the way people conduct their business. Moreover, it has become apparent that among the great variety of computer technologies available to potential users a crucial role will be played by concurrent systems. The reason is that many commonly occurring phenomena and computer applications are highly con­ current : typical examples include control systems, computer networks, digital hardware, business computing, and multimedia systems. Such systems are characterised by ever increasing complexity, which results when large num­ bers of concurrently active components interact. This has been recognised and addressed within the computing science community. In particular, sev­ eral form al models of concurrent systems have been proposed, studied, and applied in practice. This book brings together two of the most widely used formalisms for de­ scribing and analysing concurrent systems: Petri nets and process algebras. On the one hand , process algebras allow one to specify and reason about the design of complex concurrent computing systems by means of algebraic operators corresponding to common programming constructs. Petri nets, on the other hand, provide a graphical representation of such systems and an additional means of verifying their correctness efficiently, as well as a way of expressing properties related to causality and concurrency in system be­ haviour.

Arvustused

From the reviews:









"The monograph presents a step-by step development of rigorous framework for the specification and verification of concurrent systems. The book contains full proofs, carefully chosen examples and several possible directions for further research. The development of the Petri net algebra is handled in such a way that it allows for further application-oriented extensions and modifications. The book is self-contained in the sense that no previous knowledge of Petri nets and process algebras is required." (Ryszard Janicki, Mathematical Reviews, Issue 2003 g)



"This monograph combines two theories of concurrency: process algebras and Petri nets. The book can serve researches and practitioners working in concurrency theory or in formalization of parallel and distributed systems. It can also be used in an advanced graduate course as a textbook or as a reference. The book contains numerous examples and exercises included in the text immediately following the relevant material. it is well organized and coherent both in structure and content." (Boleslaw Mikolajczak, SIGACT News, Vol. 33 (2), 2002)

Introduction
1(7)
The Petri Box Calculus
7(22)
An Informal Introduction to CCS
8(1)
An Informal Introduction to Petri Nets
9(2)
The Structure and Behaviour of PBC Expressions
11(3)
Sequential Composition
14(1)
Synchronisation
15(6)
Synchronisation and Parallel Composition
21(3)
Other PBC Operators
24(1)
Modelling a Concurrent Programming Language
25(3)
Literature and Background
28(1)
Syntax and Operational Semantics
29(44)
Standard PBC Syntax
29(4)
Structured Operational Semantics
33(29)
The Basic Setup
35(2)
Equivalence Notions
37(4)
Elementary Actions
41(1)
Parallel Composition
42(3)
Choice Composition
45(1)
Sequential Composition
46(1)
Synchronisation
47(1)
Standard PBC Synchronisation
47(3)
Auto-synchronisation and Multilink-synchronisation
50(2)
Step-synchronisation
52(1)
Basic Relabelling
53(1)
Restriction
54(1)
Scoping
55(3)
Iteration
58(1)
Recursion
59(3)
Extensions
62(7)
Generalised Iterations
62(2)
Data Variables
64(2)
Generalised Control Flow Operators
66(1)
Generalised Communication Interface Operators
67(2)
Extended PBC Syntax
69(1)
Examples of Transition Systems
69(2)
Literature and Background
71(2)
Petri Net Semantics
73(60)
Compositionality and Nets
73(2)
Labelled Nets and Boxes
75(15)
An Example
75(1)
Actions and Relabellings
76(1)
Labelled Nets
77(5)
Equivalence Notions
82(4)
Boxes
86(4)
Net Refinement
90(14)
Operator Boxes
90(2)
Intuition Behind Net Refinement
92(3)
Place and Transition Names
95(2)
Formal Definition of Net Refinement
97(2)
Remarks on Net Refinement
99(2)
Properties
101(2)
Discussion
103(1)
Petri Net Semantics of PBC
104(25)
Elementary Actions
106(1)
Parallel Composition
106(1)
Choice Composition
107(2)
Sequential Composition
109(1)
Basic Relabelling
110(1)
Synchronisation
110(9)
Restriction
119(1)
Scoping
120(1)
Iteration
120(3)
Data Variables
123(1)
Generalised Control Flow Operators
124(2)
Generalised Communication Interface Operators
126(1)
Generalised Iterations
127(2)
Refined Operators
129(3)
Literature and Background
132(1)
Adding Recursion
133(40)
Inclusion Order on Labelled Nets
133(2)
Solving Recursive Equations
135(22)
Using Fixpoints to Solve Recursive Equations
137(3)
Places and Transitions in Net Solutions
140(4)
An Example of the Limit Construction
144(1)
Deriving Seed Boxes
145(6)
A Closed Form of the Maximal Solution
151(2)
Minimal Solutions
153(4)
Finitary Equations and Finite Operator Boxes
157(4)
Finitary Equation
157(2)
Finite Operator Box
159(2)
Further Examples
161(6)
Unbounded Parallel Composition
161(1)
Rear-unguardedness
162(2)
Concurrency Within Unbounded Choice
164(2)
Extreme Unguardedness
166(1)
(Non)use of Empty Nets in the Limit Construction
167(1)
Solving Systems of Recursive Equations
167(5)
Approximations, Existence, and Uniqueness
168(1)
A Closed Form of the Maximal Solution
169(2)
Guarded Systems
171(1)
Literature and Background
172(1)
S-invariants
173(54)
S-invariants, S-components, and S-aggregates
174(9)
S-invariants
176(5)
S-components
181(1)
S-aggregates
182(1)
The Synthesis Problem for Net Refinement
183(17)
Composing S-invariants
185(5)
Multiplicative Distribution Functions
190(3)
Ex-binary S-invariants
193(2)
Rational Groupings
195(5)
The Synthesis Problem for Recursive Systems
200(16)
Name Trees of Nets in the Maximal Solution
201(1)
Composing S-invariants for Recursive Boxes
202(7)
Coverability Results
209(7)
Finite Precedence Properties
216(10)
Process Semantics
218(4)
Finite Precedence of Events
222(3)
Finiteness of Complete Processes
225(1)
Literature and Background
226(1)
The Box Algebra
227(68)
SOS-operator Boxes
227(14)
A Running Example
232(1)
Properties of Factorisations
232(2)
The Domain of Application of an SOS-operator Box
234(1)
Static Properties of Refinements
235(4)
Markings of Nets
239(2)
Structured Operational Semantics of Composite Boxes
241(18)
Soundness
243(2)
Similarity Relation on Tuples of Boxes
245(3)
Completeness
248(5)
Solutions of Recursive Systems
253(2)
Behavioural Restrictions
255(4)
A Process Algebra and its Semantics
259(35)
A Running Example: the DIY Algebra
262(2)
Infinite Operators
264(3)
Denotational Semantics
267(3)
Structural Similarity Relation on Expressions
270(9)
Transition-based Operational Semantics
279(7)
Consistency of the Two Semantics
286(1)
Label-based Operational Semantics
287(3)
Partial Order Semantics of Box Expressions
290(4)
Literature and Background
294(1)
PBC and Other Process Algebras
295(18)
(Generalised) PBC is a Box Algebra
295(13)
PBC Without Loops
295(4)
Safe Translation of the Ternary PBC Iteration
299(7)
PBC with Generalised Loops
306(2)
Other Process Algebras
308(4)
CCS
310(1)
TCSP
311(1)
COSY
311(1)
Literature and Background
312(1)
A Concurrent Programming Language
313(36)
Syntax of Razor
313(5)
Programs and Blocks
315(1)
Declarations
315(1)
Commands and Actions
316(1)
Guarded Commands
316(1)
Expressions and Operators
317(1)
Syntactic Variations
317(1)
Semantics of Razor
318(11)
Programs, Blocks, and Declarations
319(2)
Basic Channel Processes
321(3)
Command Connectives
324(1)
Actions and Guarded Commands
325(4)
Three Razor Programs
329(3)
Adding Recursive Procedures
332(4)
Some Consequences of the Theory
336(4)
Proofs of Distributed Algorithms
340(7)
A Final Set of Petri-Net-Related Definitions
340(2)
Peterson's Mutual Exclusion Algorithm
342(4)
Dekker's and Morris's Mutual Exclusion Algorithms
346(1)
Literature and Background
347(2)
Conclusion
349(2)
Appendix: Solutions of Selected Exercises 351(11)
References 362(7)
Index 369