Title Page 1
Preface 5
Table of Contents 6
Modal and Temporal Argumentation Networks 8
Introduction: Concept of Usability 8
Formal Considerations 12
Kripke Models for Argumentation Networks 1 19
Kripke Models for Argumentation Networks 2 29
Conclusions 32
References 32
Knowledge Based Scheduling of Distributed Systems 33
Introduction 33
Preliminaries 34
Knowledge Based Approach for Priority Scheduling 38
The Supporting Process Policy 39
Discussion 45
Conclusions 47
References 48
Quantitative Simulation Games 49
Introduction 49
Quantitative Simulation Games 52
Transition Systems and Games 52
Qualitative Simulation Games 53
Quantitative Simulation Games 56
Modification Schemes 56
Simulation Distances 57
Correctness 58
Coverage 59
Robustness 59
Computation of Simulation Distances 61
Applications of Distances 61
Forward Error Correction Systems 61
Environment Restriction for Reactive Systems 64
Conclusion 65
References 66
The Localization Reduction and Counterexample-Guided Abstraction Refinement 68
Introduction 68
Localization Reduction 68
Counterexample-Guided Abstraction Refinement 71
Automatic Abstraction without Counterexamples 75
References 76
A Scalable Segmented Decision Tree Abstract Domain 79
Introduction 79
Semantic Disjunctions in Abstract Interpretation 79
Handling Disjunctions in Abstract Interpretation 80
Binary Decision Trees 81
Variable Packing 82
Array Segmentation 83
Segmented Decision Trees 84
Segmented Decision Tree Abstract Functor 87
Reduction of an Abstract Property by a Segmented Decision Tree 87
Reduction of a Segmented Decision Tree by an Abstract Property, Tests 88
Segments Unification, Tree Merges and Binary Operations 89
Assignments 92
Abstracting Functions (and Array Contents) 95
Examples 96
Conditional Computation 96
Partial Array Initialization 97
Multidimentional Arrays 99
Conclusion 101
References 101
Towards Component Based Design of Hybrid Systems: Safety and Stability 103
Introduction 103
Basic Definitions 105
Behavior 107
Parallel Composition 108
Hierarchical Controller Design 109
Hierarchical Verification of Robust Safety and Stability 132
Conclusion 148
References 149
Mildly Context-Sensitive Languages via Buffer Augmented Pregroup Grammars 151
Introduction 151
Pregroups and Pregroup Grammars 153
Buffer Augmented PGGs 155
Pumping Lemma for (Restricted) BAPGG Languages 159
Complexity of BAPGG Languages 160
Complexity of Restricted BAPGG Languages 165
Hierarchy of Restricted BAPGG Languages 170
An Extension of BAPGGs 171
Concluding Remarks 172
References 172
Inference Rules for Proving the Equivalence of Recursive Procedures 174
Introduction 174
Notions of Equivalence 175
Preliminaries 176
The Programming Language 176
Computations and Subcomputations of LPL Programs 177
A Proof Rule for Partial Procedure Equivalence 177
Definitions 178
Rule (PROC-P-EQ) 179
A Proof Rule for Mutual Termination of Procedures 182
Definitions 182
Rule (M-TERM) 182
Using Rule (M-TERM): A Long Example 183
What the Rules Cannot Prove 185
Summary 186
References 187
A Operational Semantics of LPL 188
A.1 Notation of Sequences 188
A.2 Operational Semantics 188
Some Thoughts on the Semantics of Biocharts 192
Introduction 192
Biological Modeling with Differential Equations 193
Challenges in Biological Modeling 193
Biology vs. Software 194
Semantics Outline 195
The Basics 195
Classes and Objects 196
Messages and Actions 196
Inheritance and Statechart Modification 198
Dynamic Changes to a Statechart 198
Steps 199
Low Level Modules 199
APledge 200
References 200
Unraveling a Card Trick 202
Informal Proof 202
The Formalization 205
Conclusions 207
References 208
An Automata-Theoretic Approach to Infinite-State Systems 209
Introduction 209
Preliminaries 213
Labeled Transition Graphs and Rewrite Systems 214
Temporal Logics 216
Alternating Two-Way Automata 218
Alternating Automata on Labeled Transition Graphs 220
Model-Checking Branching-Time Properties 221
Pushdown Graphs 222
Prefix-Recognizable Graphs 224
Path Automata on Trees 227
Definition 228
Expressiveness 229
Decision Problems 231
Model-Checking Linear-Time Properties 236
Pushdown Graphs 236
Prefix-Recognizable Graphs 237
Relating Regular Labeling with Prefix-Recognizability 240
Model-Checking Graphs with Regular Labeling 240
Prefix-Recognizable to Regular Labeling 242
Realizability and Synthesis 247
Discussion 250
References 252
A Proof of Claim 4.3 257
B Lower Bound on Emptiness of 2NBP 260
C Lower Bound for Linear Time Model-Checking on Prefix-Recognizable Systems 263
On the Krohn-Rhodes Cascaded Decomposition Theorem 267
Introduction 267
Preliminaries 269
Automata 269
Semigroups 269
The Krohn-Rhodes Primary Decomposition Theorem 272
Structures Associated with a Cascade 273
A Decomposition Algorithm 278
Concluding Remarks 283
References 284
Temporal Verification of Reactive Systems: Response 286
Response 287
Response Rule 288
Chain Rule 293
ChainDiagrams 297
Well-Founded Rule 319
Rank Diagrams 334
Response with Past Subformulas 340
Compositional Verification of Response Properties 344
Guarantee Properties 353
Obligation Properties 356
The Arrow of Time through the Lens of Computing 369
And The Race Begins... 370
Personal Remarks 374
References 375
What Is in a Step: New Perspectives on a Classical Question 377
Introduction 377
Pnueli and Shalev\u2019s Interpretation of Statecharts 380
Introduction to Statecharts 380
The Pnueli-Shalev Step Semantics 381
Developments and New Perspectives 384
Configuration Syntax 384
Order-Theoretic Perspective 385
Denotational Perspective 387
Algebraic Perspective 390
Game-Theoretic Perspective 392
Related Work, Esterel and Logic Programming 395
Related Work 395
Relation to Esterel 397
Relation to Logic Programming 399
Reminiscences on Amir Pnueli\u2019s First Contributions to the Semantics of Statecharts (by Willem de Roever) 400
Visit to the Weizmann Institute in the Mid 1980s 401
The 5 Different Semantics 402
References 403
Author Index 407