Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship

by E. -R. Olderog

• ISBN13: 9780521018456
• ISBN10: 0521018455
• Format: Paperback
• Copyright: 2005-08-22
• Publisher: Cambridge University Press

Summary

The author presents a theory of concurrent processes where three different semantic description methods that are usually studied in isolation are brought together. Petri nets describe processes as concurrent and interacting machines; algebraic process terms describe processes as abstract concurrent processes; and logical formulas specify the intended communication behaviour of processes. At the heart of this theory are two sets of transformation rules for the top-down design of concurrent processes. The first set can be used to transform stepwise logical formulas into process terms, whilst process terms can be transformed into Petri nets by the second set. These rules are based on novel techniques for the operational and denotational semantics of concurrent processes. Various results and relationships between nets, terms and formulas starting with formulas and illustrated by examples. The use of transformations is demonstrated in a series of case studies, and the author also identifies directions for future research. The book is written for graduate students and researchers in computer science; the author assumes a basic understanding of mathematical terminology, predicate logic and programming, but develops the semantic concepts used in a self-contained manner. The core of the material can be used for a one-semester course on concurrent processes.

Table of Contents

PREFACE	v
How to use this Book	vi
1 INTRODUCTION	1	(18)
1.1 Three Views: an Example	2	(10)
1.2 Outline of this Book	12	(7)
2 PETRI NETS	19	(24)
2.1 Automata	20	(6)
2.2 Place/Transition Nets	26	(6)
2.3 Causal Nets	32	(7)
2.4 Problems with Nets	39	(4)
3 PROCESS TERMS	43	(54)
3.1 Syntax	44	(3)
3.2 Informal Semantics	47	(2)
3.3 Operational Net Semantics	49	(9)
3.4 Safeness	58	(3)
3.5 Finiteness and Algebraic Properties	61	(9)
3.6 What is a Good Net Semantics?	70	(3)
3.7 Retrievability	73	(16)
3.8 Compositionality	89	(8)
4 LOGICAL FORMULAS	97	(72)
4.1 Trace Logic	99	(11)
4.2 Trace Specifications	110	(4)
4.3 Process Correctness	114	(10)
4.4 Modified Readiness Semantics	124	(12)
4.5 Denotational Approach	136	(7)
4.6 Equivalence	143	(17)
4.7 Full Abstraction	160	(9)
5 PROCESS CONSTRUCTION	169	(58)
5.1 Transformations on Mixed Terms	171	(9)
5.2 Soundness	180	(10)
5.3 Counters	190	(13)
5.4 Binary Variable	203	(5)
5.5 Scheduling Problem	208	(6)
5.6 Access Control	214	(6)
5.7 Completeness Issues	220	(7)
6 EXTENSIONS	227	(14)
6.1 Nondeterminism	228	(8)
6.2 Fairness	236	(1)
6.3 Concurrency	237	(2)
6.4 Structured Communications	239	(1)
6.5 Further Research Topics	239	(2)
BIBLIOGRAPHY	241	(12)
AUTHOR INDEX	253	(3)
SUBJECT INDEX	256	(5)
SYMBOL INDEX	261