E-Book, Englisch, 181 Seiten
Bollig Formal Models of Communicating Systems
1. Auflage 2006
ISBN: 978-3-540-32923-7
Verlag: Springer Berlin Heidelberg
Format: PDF
Kopierschutz: 1 - PDF Watermark
Languages, Automata, and Monadic Second-Order Logic
E-Book, Englisch, 181 Seiten
ISBN: 978-3-540-32923-7
Verlag: Springer Berlin Heidelberg
Format: PDF
Kopierschutz: 1 - PDF Watermark
This book studies the relationship between automata and monadic second-order logic, focusing on classes of automata that describe the concurrent behavior of distributed systems. It provides a unifying theory of communicating automata and their logical properties. Based on Hanf's Theorem and Thomas's graph acceptors, it develops a result that allows characterization of many popular models of distributed computation in terms of the existential fragment of monadic second-order logic.
Autoren/Hrsg.
Weitere Infos & Material
1;Preface;5
2;Contents;7
3;1 Introduction;10
3.1;1.1 Formal Methods;10
3.2;1.2 Partial Orders and Graphs;12
3.3;1.3 High-Level Specifications;14
3.4;1.4 Towards an Implementation;15
3.5;1.5 An Overview of the Book;16
4;2 Preliminaries;20
4.1;2.1 Words and Partial Orders;20
4.2;2.2 Monoids and Languages;21
4.3;2.3 Turing Machines and the Halting Problem;23
4.4;2.4 Bibliographic Notes;24
5;3 Graphs, Logics, and Graph Acceptors;26
5.1;3.1 Graphs;26
5.2;3.2 Monadic Second-Order Logic over Graphs;27
5.3;3.3 Hanf’s Theorem;32
5.4;3.4 Graph Acceptors;36
5.5;3.5 Directed Acyclic Graphs;39
5.6;3.6 Pictures and Grids;40
5.7;3.7 Bibliographic Notes;43
6;4 Words and Finite Automata;44
6.1;4.1 Words;44
6.2;4.2 Finite Automata;45
6.3;4.3 Summary;49
6.4;4.4 Bibliographic Notes;50
7;5 Dags and Asynchronous Cellular Automata;52
7.1;5.1 ( S,C)-Dags;52
7.2;5.2 The Operational Behavior of ( S,C)-Dags;59
7.3;5.3 Asynchronous Cellular Automata with Types;61
7.4;5.4 ACATs vs. ACAs;65
7.5;5.5 The Expressive Equivalence of ACATs and EMSO Logic;69
7.6;5.6 Summary;83
7.7;5.7 Bibliographic Notes;84
8;6 Mazurkiewicz Traces and Asynchronous Automata;86
8.1;6.1 Mazurkiewicz Traces;86
8.2;6.2 Trace Languages;87
8.3;6.3 Asynchronous Automata;89
8.4;6.4 Asynchronous Automata vs. ACAs and EMSO Logic;93
8.5;6.5 Product Automata;96
8.6;6.6 Summary;98
8.7;6.7 Bibliographic Notes;99
9;7 Message Sequence Charts;100
9.1;7.1 Message Sequence Charts;100
9.2;7.2 Universal and Existential Bounds;104
9.3;7.3 High-Level Message Sequence Charts;105
9.4;7.4 Message Contents and Non-Fifo Behavior;112
9.5;7.5 Live Sequence Charts;114
9.6;7.6 Regular MSC Languages;116
9.7;7.7 (E)MSO-Definable MSC Languages;116
9.8;7.8 Product MSC Languages;118
9.9;7.9 Relationships to Mazurkiewicz Traces;119
9.10;7.10 Bibliographic Notes;123
10;8 Communicating Finite-State Machines;126
10.1;8.1 Communicating (Finite-State) Machines;126
10.2;8.2 Channel-Bounded and Deadlock-Free CMs;131
10.3;8.3 Undecidability Results;133
10.4;8.4 Lossy Channel Systems;137
10.5;8.5 Non-Fifo Channel Systems;139
10.6;8.6 CMs vs. Product MSC Languages;140
10.7;8.7 CFMs vs. Regular MSC Languages;141
10.8;8.8 CFMs vs. ACAs and EMSO Logic;142
10.9;8.9 CFMs vs. Graph Acceptors;147
10.10;8.10 CFMs vs. EMSO-Definable Product Languages;153
10.11;8.11 The Complete Hierarchy;154
10.12;8.12 Bibliographic Notes;158
11;9 Beyond Implementability;160
11.1;9.1 EMSO vs. MSO in the Bounded Setting;160
11.2;9.2 EMSO vs. MSO in the Unbounded Setting;162
11.3;9.3 Determinism vs. Nondeterminism;167
11.4;9.4 CFMs vs. Recognizability;168
11.5;9.5 CFMs vs. Rational MSC Languages;169
11.6;9.6 Summary;172
11.7;9.7 Bibliographic Notes;173
12;References;174
13;Symbols and Notation;182
13.1;Chapter 2;182
13.2;Chapter 3;182
13.3;Chapter 4;183
13.4;Chapter 5;183
13.5;Chapter 6;184
13.6;Chapter 7;184
13.7;Chapter 8;185
14;Index;188
