Muutke küpsiste eelistusi

E-raamat: Concurrency Theory: Calculi an Automata for Modelling Untimed and Timed Concurrent Systems

  • Formaat: PDF+DRM
  • Ilmumisaeg: 28-Feb-2006
  • Kirjastus: Springer London Ltd
  • Keel: eng
  • ISBN-13: 9781846283369
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.
  • Formaat: PDF+DRM
  • Ilmumisaeg: 28-Feb-2006
  • Kirjastus: Springer London Ltd
  • Keel: eng
  • ISBN-13: 9781846283369
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. 

Concurrency Theory is a synthesis of one of the major threads of theoretical computer science research focusing on languages and graphical notations for describing collections of simultaneously evolving components that interact through synchronous communication. The main specification notation focused on in this book is LOTOS. An extensive introduction to this particular process calculus is given, highlighting how the approach differs from competitor techniques, such as CCS and CSP.The book covers linear-time semantics, based on traces; branching-time semantics, using both labeled transition systems and refusals; and true concurrency semantics, using (bundle) event structures. In addition, the book discusses communicating automata approaches (both finite and infinite state); how the theory can be generalised to the timed setting; and, finally the authors generalise the (finite and infinite state) communicating automata notations to yield timed automata and discrete timed automata.This book represents a comprehensive pass through the spectrum of concurrency theory research: From untimed to timed syntax and semantics and process calculi to automata. Researchers and practitioners in the field of concurrency theory, as well as MSc and PhD students, will find the comprehensive coverage in this book essential reading.

The field of concurrency theory is becoming increasingly important, with the problem of formally verifying concurrent distributed systems a critical consideration and a major topic for the software industries. This book, with its extensive applications of the techniques involved in the field of concurrency theory, is the first to adopt this new approach.

Arvustused

From the reviews:









"This book covers a wide range of results from works in concurrency theory . scientists and students doing research in various related areas such as concurrency control or parallel computing will find this book quite useful. the book represents a comprehensive coverage of the development of concurrency theory reflecting the historical progression of the field. The book undoubtedly will suit students and specialists doing research in concurrency theory ." (Alekber Aliyev, Zentralblatt MATH, Vol. 1140, 2008)

Part I Introduction
Background on Concurrency Theory
3(16)
Concurrency Is Everywhere
3(1)
Characteristics of Concurrent Systems
4(2)
Classes of Concurrent Systems
6(3)
Basic Event Ordering
6(1)
Timing Axis
7(1)
Probabilistic Choice Axis
8(1)
Mobility Axis
9(1)
Mathematical Theories
9(4)
Overview of Book
13(6)
Part II Concurrency Theory -- Untimed Models
Process Calculi: LOTOS
19(36)
Introduction
19(1)
Example Specifications
20(2)
A Communication Protocol
20(2)
The Dining Philosophers
22(1)
Primitive Basic LOTOS
22(30)
Abstract Actions
26(2)
Action Prefix
28(1)
Choice
29(1)
Nondeterminism
30(4)
Process Definition
34(7)
Concurrency
41(6)
Sequential Composition and Exit
47(3)
Syntax of pbLOTOS
50(2)
Example
52(3)
Basic Interleaved Semantic Models
55(50)
A General Perspective on Semantics
55(8)
Why Semantics?
55(2)
Formal Definition
57(4)
Modelling Recursion
61(2)
What Makes a Good Semantics?
63(1)
Trace Semantics
63(13)
The Basic Approach
63(3)
Formal Semantics
66(7)
Development Relations
73(2)
Discussion
75(1)
Labelled Transition Systems
76(25)
The Basic Approach
76(2)
Formal Semantics
78(7)
Development Relations
85(16)
Verification Tools
101(4)
Overview of CADP
102(1)
Bisimulation Checking in CADP
103(2)
True Concurrency Models: Event Structures
105(36)
Introduction
105(2)
The Basic Approach -- Event Structures
107(5)
Event Structures and pbLOTOS
112(3)
An Event Structures Semantics for pbLOTOS
115(8)
Relating Event Structures to Labelled Transition Systems
123(3)
Development Relations
126(8)
Alternative Event Structure Models
134(4)
Summary and Discussion
138(3)
Testing Theory and the Linear Time -- Branching Time Spectrum
141(44)
Trace-refusals Semantics
141(19)
Introduction
141(2)
The Basic Approach
143(2)
Deriving Trace-refusal Pairs
145(1)
Internal Behaviour
146(6)
Development Relations: Equivalences
152(2)
Nonequivalence Development Relations
154(4)
Explorations of Congruence
158(1)
Summary and Discussion
159(1)
Testing Justification for Trace-refusals Semantics
160(1)
Testing Theory in General and the Linear Time -- Branching Time Spectrum
161(5)
Sequence-based Testing
162(1)
Tree-based Testing
163(3)
Applications of Trace-refusals Relations in Distributed Systems
166(19)
Relating OO Concepts to LOTOS
166(1)
Behavioural Subtyping
167(10)
Viewpoints and Consistency
177(8)
Part III Concurrency Theory -- Further Untimed Notations
Beyond pbLOTOS
185(30)
Basic LOTOS
185(7)
Disabling
185(3)
Generalised Choice
188(1)
Generalised Parallelism
189(1)
Verbose Specification Syntax
190(1)
Verbose Process Syntax
190(1)
Syntax of bLOTOS
191(1)
Full LOTOS
192(15)
Guarded Choice
193(1)
Specification Notation
193(1)
Process Definition and Invocation
194(1)
Value Passing Actions
194(8)
Local Definitions
202(1)
Selection Predicates
202(1)
Generalised Choice
203(1)
Parameterised Enabling
204(2)
Syntax of fLOTOS
206(1)
Comments
206(1)
Examples
207(6)
Communication Protocol
207(3)
Dining Philosophers
210(3)
Extended LOTOS
213(2)
Comparison of LOTOS with CCS and CSP
215(18)
CCS and LOTOS
217(5)
Parallel Composition and Complementation of Actions
217(3)
Restriction and Hiding
220(1)
Internal Behaviour
221(1)
Minor Differences
221(1)
CSP and LOTOS
222(11)
Alphabets
222(2)
Internal Actions
224(1)
Choice
225(2)
Parallelism
227(1)
Hiding
227(1)
Comparison of LOTOS Trace-refusals with CSP Failures-divergences
228(5)
Communicating Automata
233(28)
Introduction
233(1)
Networks of Communicating Automata
234(16)
Component Automata
234(2)
Parallel Composition
236(3)
Example Specifications
239(1)
Semantics and Development Relations
240(1)
Verification of Networks of Communicating Automata
241(5)
Relationship to Process Calculi
246(4)
Infinite State Communicating Automata
250(11)
Networks of Infinite State Communicating Automata
251(3)
Semantics of ISCAs as Labelled Transition Systems
254(7)
Part IV Concurrency Theory -- Timed Models
Timed Process Calculi, a LOTOS Perspective
261(26)
Introduction
261(1)
Timed LOTOS -- The Issues
262(16)
Timed Action Enabling
262(5)
Urgency
267(3)
Persistency
270(1)
Nondeterminism
271(1)
Synchronisation
272(1)
Timing Domains
273(1)
Time Measurement
273(1)
Timing of Nonadjacent Actions
274(1)
Timed Interaction Policies
275(1)
Forms of Internal Urgency
276(2)
Discussion
278(1)
Timed LOTOS Notation
278(5)
The Language
278(3)
Example Specifications
281(2)
Timing Anomalies in tLOTOS
283(2)
E-LOTOS, the Timing Extensions
285(2)
Semantic Models for tLOTOS
287(34)
Branching Time Semantics
287(17)
Timed Transition Systems
287(2)
Operational Semantics
289(10)
Branching Time Development Relations
299(5)
True Concurrency Semantics
304(17)
Introduction
304(1)
Timed Bundle Event Structures
305(3)
Causal Semantics for tLOTOS
308(10)
Anomalous Behaviour
318(2)
Discussion
320(1)
Timed Communicating Automata
321(26)
Introduction
321(2)
Timed Automata -- Formal Definitions
323(9)
Syntax
324(1)
Semantics
325(7)
Real-time Model-checking
332(15)
Forward Reachability
333(8)
Example: Reachability Analysis on the Multimedia Stream
341(1)
Issues in Real-time Model-checking
342(5)
Timelocks in Timed Automata
347(30)
Introduction
347(2)
A Classification of Deadlocks in Timed Automata
349(3)
Discussion: Justifying the Classification of Deadlocks
350(1)
Discussion: Timelocks in Process Calculi
351(1)
Time-actionlocks
352(7)
Timed Automata with Deadlines
353(5)
Example: A TAD Specification for the Multimedia Stream
358(1)
Zeno-timelocks
359(15)
Example: Zeno-timelocks in the Multimedia Stream
359(2)
Nonzenoness: Syntactic Conditions
361(7)
Nonzenoness: A Sufficient-and-Necessary Condition
368(6)
Timelock Detection in Real-time Model-checkers
374(3)
Uppaal
374(2)
Kronos
376(1)
Discrete Timed Automata
377(20)
Infinite vs. Finite States
377(3)
Preliminaries
380(4)
Fair Transition Systems and Invariance Proofs
381(2)
The Weak Monadic Second-order Theory of 1 Successor (WS1S) and MONA
383(1)
Discrete Timed Automata -- Formal definitions
384(5)
Syntax
384(2)
Example: A DTA Specification for the Multimedia Stream
386(1)
Semantics
387(2)
Verifying Safety Properties over DTAs
389(5)
Discussion: Comparing DTAs and TIOAs with Urgency
394(3)
References
397(12)
Appendix
409(20)
Enabling as a Derived Operator
409(1)
Strong Bisimulation Is a Congruence
409(5)
Weak Bisimulation Congruence
414(5)
Timed Enabling as a Derived Operator
419(1)
Hiding is Not Substitutive for Timed Bisimulations
420(1)
Substitutivity of Timed Strong Bisimulation
420(2)
Substitutivity of Timed Rooted Weak Bisimulation
422(7)
Index 429