Formal Models of Communicating Systems (eBook)

Languages, Automata, and Monadic Second-Order Logic

Benedikt Bollig (Autor)

eBook Download: PDF

2006
IX, 181 Seiten
Springer Berlin (Verlag)
9783540329237 (ISBN)

Infos

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.

Inhalt

Preface 5
Contents 7
1 Introduction 10
1.1 Formal Methods 10
1.2 Partial Orders and Graphs 12
1.3 High-Level Specifications 14
1.4 Towards an Implementation 15
1.5 An Overview of the Book 16
2 Preliminaries 20
2.1 Words and Partial Orders 20
2.2 Monoids and Languages 21
2.3 Turing Machines and the Halting Problem 23
2.4 Bibliographic Notes 24
3 Graphs, Logics, and Graph Acceptors 26
3.1 Graphs 26
3.2 Monadic Second-Order Logic over Graphs 27
3.3 Hanf’s Theorem 32
3.4 Graph Acceptors 36
3.5 Directed Acyclic Graphs 39
3.6 Pictures and Grids 40
3.7 Bibliographic Notes 43
4 Words and Finite Automata 44
4.1 Words 44
4.2 Finite Automata 45
4.3 Summary 49
4.4 Bibliographic Notes 50
5 Dags and Asynchronous Cellular Automata 52
5.1 ( S,C)-Dags 52
5.2 The Operational Behavior of ( S,C)-Dags 59
5.3 Asynchronous Cellular Automata with Types 61
5.4 ACATs vs. ACAs 65
5.5 The Expressive Equivalence of ACATs and EMSO Logic 69
5.6 Summary 83
5.7 Bibliographic Notes 84
6 Mazurkiewicz Traces and Asynchronous Automata 86
6.1 Mazurkiewicz Traces 86
6.2 Trace Languages 87
6.3 Asynchronous Automata 89
6.4 Asynchronous Automata vs. ACAs and EMSO Logic 93
6.5 Product Automata 96
6.6 Summary 98
6.7 Bibliographic Notes 99
7 Message Sequence Charts 100
7.1 Message Sequence Charts 100
7.2 Universal and Existential Bounds 104
7.3 High-Level Message Sequence Charts 105
7.4 Message Contents and Non-Fifo Behavior 112
7.5 Live Sequence Charts 114
7.6 Regular MSC Languages 116
7.7 (E)MSO-Definable MSC Languages 116
7.8 Product MSC Languages 118
7.9 Relationships to Mazurkiewicz Traces 119
7.10 Bibliographic Notes 123
8 Communicating Finite-State Machines 126
8.1 Communicating (Finite-State) Machines 126
8.2 Channel-Bounded and Deadlock-Free CMs 131
8.3 Undecidability Results 133
8.4 Lossy Channel Systems 137
8.5 Non-Fifo Channel Systems 139
8.6 CMs vs. Product MSC Languages 140
8.7 CFMs vs. Regular MSC Languages 141
8.8 CFMs vs. ACAs and EMSO Logic 142
8.9 CFMs vs. Graph Acceptors 147
8.10 CFMs vs. EMSO-Definable Product Languages 153
8.11 The Complete Hierarchy 154
8.12 Bibliographic Notes 158
9 Beyond Implementability 160
9.1 EMSO vs. MSO in the Bounded Setting 160
9.2 EMSO vs. MSO in the Unbounded Setting 162
9.3 Determinism vs. Nondeterminism 167
9.4 CFMs vs. Recognizability 168
9.5 CFMs vs. Rational MSC Languages 169
9.6 Summary 172
9.7 Bibliographic Notes 173
References 174
Symbols and Notation 182
Chapter 2 182
Chapter 3 182
Chapter 4 183
Chapter 5 183
Chapter 6 184
Chapter 7 184
Chapter 8 185
Index 188

Produkt-Details

• Erscheint lt. Verlag: 8.9.2006
• Zusatzinfo: IX, 181 p.
• Verlagsort: Berlin
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Themenwelt: Mathematik / Informatik ► Informatik ► Web / Internet
• Themenwelt: Mathematik / Informatik ► Mathematik
• Themenwelt: Technik
• Schlagworte: Algorithm analysis and problem complexity • Asynchronous cellular automata • Automata • Automata Theory • communicating systems • Distributed Systems • Finite Automata • Finite-State Machines • formal methods • Graphs • Logic • Mazurkiewicz traces • message sequence charts • Modeling • Software engineering
• ISBN-13: 9783540329237 / 9783540329237