A Journey From Process Algebra Via Timed Automata to Model Learning : Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday

Preface Organization Contents Non-finite Axiomatisability Results via Reductions: CSP Parallel Composition and CCS Restriction 1 Introduction 2 Preliminaries 3 The Proof Strategy: Reduction Mappings 4 Axiomatisability Results for CSP Parallel Composition 4.1 The Languages BCCSPAp, BCCSPActp, BCCSPp and BCCSPp 4.2 The Negative Result for BCCSPAp 4.3 The Case of BCCSPp and the Negative Result for BCCSPp 4.4 The Case of BCCSPActp 5 The Case of Restriction 5.1 The Negative Result 5.2 The Reduction 6 Concluding Remarks References Operational Causality – Necessarily Sufficient and Sufficiently Necessary 1 Introduction 2 Preliminaries 3 Necessary and Sufficient Causes 3.1 Necessary Causes 3.2 Sufficient Causes 4 Finding Good Causes 4.1 Degrees of Sufficiency and Necessity 4.2 Weight-Minimal Necessary Causes 5 Conclusion References Axiomatizing Consciousness with Applications 1 Towards Consciousness 2 Consciousness as Discrete, Probabilistic-Computable Actor 3 Compound Consciousness 4 Self 5 Mindfulness: Mechanism and Application to ER 6 Suffering 6.1 Suffering as Pain 6.2 Suffering as Change 6.3 Suffering from Lack 7 Release: "3223379 Suffering and "3222378 Freedom 8 Freedom Paradox 9 Layers of Consciousness 10 Conclusion References Symmetric Transrationals: The Data Type and the Algorithmic Degree of its Equational Theory 1 Introduction 2 Basic Theory of Abstract Data Types 2.1 Expansions, Extensions, and Enlargements 3 The Symmetric Transfields 3.1 Algebra of Peripheral Numbers and their Equational Specification 3.2 Making a Symmetric Transfield 3.3 Making a Bounded Symmetric Transfield 4 Rationals and Transrationals 4.1 Transrationals and Bounded Transrationals 4.2 Minimality of the Bounded Transrationals 5 One-One Degree of Equations in Symmetric Transrationals 5.1 The Diophantine Problem for the Rationals 5.2 Equational Theories 6 Concluding Remarks 6.1 Background on the Rationals and Their Enlargements 6.2 Practical Computer Arithmetics 6.3 Hybrid Systems References A Survey of Model Learning Techniques for Recurrent Neural Networks 1 Introduction 2 Recurrent Neural Networks as Language Acceptors 3 Model Learning for Recurrent Neural Networks 3.1 Answering Equivalence Queries Probably Approximately Correct 3.2 Equivalence Queries Inspired by Statistical Model Checking 3.3 An Abstraction Refinement Approach to Equivalence Queries 4 Explainability Beyond Regular Languages 5 Conclusion References Back-and-Forth in Space: On Logics and Bisimilarity in Closure Spaces 1 Introduction 2 Preliminaries 3 Bisimilarity for Closure Models 3.1 CM-bisimilarity 3.2 Logical Characterisation of CM-bisimilarity 4 CMC-bisimilarity for QdCMs 4.1 CMC-bisimilarity for QdCMs 4.2 Logical Characterisation of CMC-bisimilarity 5 CoPa-Bisimilarity for QdCM 5.1 CoPa-bisimilarity 5.2 Logical Characterisation of CoPa-bisimilarity 6 Conclusions References Better Automata Through Process Algebra 1 Introduction 2 Languages, Regular Expressions and Automata 2.1 Alphabets and Languages 2.2 Regular Expressions 2.3 Finite Automata 3 Kleene's Theorem 4 NFAs via Structural Operational Semantics 4.1 An Operational Semantics for Regular Expressions 4.2 Building Automata Using Acceptance and Transitions 4.3 Computing NFAs from Regular Expressions 5 Discussion 6 Conclusions and Directions for Future Work A SOS Rules for Acceptance and Transitions References Family-Based Fingerprint Analysis: A Position Paper 1 Introduction 2 Software Fingerprinting 2.1 Model Learning 2.2 A Methodology and Taxonomy for Formal Fingerprint Analysis 3 Family-Based Fingerprint Analysis 3.1 Family-Based Modeling and Analysis 3.2 A Framework for Family-Based Fingerprint Analysis 3.3 Practical and Theoretical Implications 4 Final Remarks References What's in School? – Topic Maps for Secondary School Computer Science 1 Introduction 2 Computer Science Learning and Teaching Standards 3 Topic Maps 4 Model Checking Unit 5 Discussion and Conclusion References Tree-Based Adaptive Model Learning 1 Introduction 2 Preliminaries 2.1 Learning with a Classification Tree 3 Learning Evolving Systems Incrementally 3.1 Correctness and Termination 4 Experiments 5 Conclusion A Omitted Incremental Subroutines B Additional Experiment Graphs B.1 Mutation Benchmark B.2 Feature-Add Benchmark References From Languages to Behaviors and Back 1 Introduction 2 Preliminaries for Behavioral Systems 2.1 A Semantic Point of View 2.2 A Technical Point of View 3 Systems of Procedural Transition Systems 3.1 A Semantic Point of View 3.2 A Technical Point of View 4 Learning Systems of Procedural Transition Systems 4.1 A Semantic Point of View 4.2 A Technical Point of View 5 On Behaviors and Reductions to Well-Matched Languages 6 Evaluation 6.1 Benchmark Setup 6.2 Results 7 Related Work 8 Outlook and Future Work References The Quest for an Adequate Semantic Basis of Dense-Time Metric Temporal Logic 1 Introduction 2 Signal Duration Calculus 3 Formulae Differentiating Signal Classes 4 Conclusion References Equivalence Checking 40 Years After: A Review of Bisimulation Tools 1 Introduction 2 Retrospective of the 1980s 2.1 Bisimulation Tools Based on Term Rewriting 2.2 Algorithms for Bisimulations on Finite-State Systems 2.3 Early Bisimulation Tools 3 Retrospective of the 1990s 3.1 New Algorithms for Bisimulations 3.2 Algorithms for On-the-Fly Verification 3.3 Algorithms for Symbolic Verification 3.4 Algorithms for Compositional Verification 3.5 Enhanced Bisimulation Tools 3.6 New Bisimulation Tools 3.7 Bisimulation Tools for Timed and Hybrid Systems 3.8 Bisimulation Tools for Probabilistic and Stochastic Systems 3.9 Bisimulation Tools for Mobile Systems 4 Retrospective of the 2000s 4.1 New Algorithm for Strong Bisimulation 4.2 New Bisimulation Tools 4.3 Bisimulation Tools Using On-the-Fly Verification 4.4 Bisimulation Tools Based on Compositional Verification 4.5 Bisimulation Tools Based on Parallel/Distributed Computing 4.6 Bisimulation Tools Based on Symbolic Verification 4.7 Bisimulation Tools for Timed Systems 4.8 Bisimulation Tools for Probabilistic and Stochastic Systems 5 Retrospective of the 2010s 5.1 New Bisimulation Tools 5.2 Bisimulation Tools for Probabilistic and Stochastic Systems 5.3 Bisimulation Tools for Mobile Systems 5.4 Bisimulation Tools Based on Parallel/Distributed Computing 5.5 Bisimulation Tools Based on Compositional Verification 5.6 Recent Results for Strong and Branching Bisimulations 6 Conclusion References Apartness and Distinguishing Formulas in Hennessy-Milner Logic 1 Introduction 2 Bisimulation and Apartness for LTSs 2.1 Hennessy-Milner Logic for Bisimulation 3 Weak Bisimulation and Apartness for LTSs 3.1 Hennessy-Milner Logic for Weak Bisimulation 4 Branching Bisimulation and Apartness for LTSs 4.1 Hennessy-Milner Logic for Branching Bisimulation 4.2 Examples 4.3 Related and Further Work References Playing Wordle with Uppaal Stratego 1 Introduction 2 Wordle 3 Uppaal Stratego 4 Wordle in Uppaal Stratego 5 Evaluation 6 Conclusion References Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation 1 Introduction 2 ATerm Library 3 State Space Generation 4 Model Checking via Boolean Equation Systems 5 Conclusion References Active Automata Learning as Black-Box Search and Lazy Partition Refinement 1 Introduction 2 Regular Languages and Automata 3 MAT Learning 4 The L Algorithm 5 Demonstration 6 Evaluation 7 Conclusion References A Reconstruction of Ewens' Sampling Formula via Lists of Coins 1 Introduction 2 The Challenge 3 Going Probabilistic 4 Adding a Mutation Rate Parameter 5 The Lengths of Coin Sequences 6 Multisets Instead of Lists References .26em plus .1em minus .1emRooted Divergence-Preserving Branching Bisimilarity is a Congruence: A Simpler Proof 1 Introduction 2 Finite-State CCS and Branching Bisimulation 3 Congruence for Finite-State Processes 4 Comparison with the Congruence Proof for a Traditional Definition 5 Extending the Proof to Full CCS? References Learning Language Intersections 1 Introduction 2 Strategies 2.1 The Word-by-Word Strategy 2.2 The Independent Strategy 2.3 The Machine-by-Machine Strategy 3 Prototype Implementation 3.1 The Membership Oracle Signature 3.2 An Adequate Equivalence Oracle 4 Empirical Evaluation 4.1 Setup 4.2 Summary 4.3 Detailed Results 5 Conclusion and Outlook References Runtime Verification of Compound Components with ComMA 1 Introduction 2 Interface Modeling and Monitoring 2.1 ComMA Interface Modeling 2.2 Interface Monitoring 3 Component Models 3.1 Components with Functional Constraints 3.2 Using the Identity of Communication Partners 4 Compound Components 5 Component Monitoring 5.1 Traces with Messages Between Component Instances 5.2 Algorithm for Monitoring a Trace 5.3 Checking Functional Constraints 6 Related Work 7 Conclusions References A Basic Compositional Model for Spiking Neural Networks 1 Introduction 2 The Spiking Neural Network Model 2.1 Network Structure 2.2 Executions and Probabilistic Executions 2.3 External Behavior of a Network 2.4 Examples 3 Composition of Spiking Neural Networks 3.1 Composition of Two Networks 3.2 Examples 3.3 Compositionality Definitions 4 Theorems for Acyclic Composition 4.1 Compositionality 4.2 Examples 5 Theorems for General Composition 5.1 Composition Results for Executions and Traces 5.2 Composition Results for One-Step Extensions 5.3 Compositionality 5.4 Examples 6 Hiding for Spiking Neural Networks 6.1 Hiding Definition 6.2 Examples 7 Problems for Spiking Neural Networks 7.1 Problems and Solving Problems 7.2 Composition of Problems 7.3 Hiding of Problems 7.4 Examples 8 Conclusions References State Identification and Verification with Satisfaction 1 Introduction 2 State Identification and Verification 2.1 Testing Problems 2.2 Separating and Distinguishing Sequences 2.3 Identification in a Subset of States 3 Reduction to SAT Solving 3.1 State Verification via UIO Sequences 3.2 State Identification via Adaptive Distinguishing Sequences 4 Preliminary Experimental Results 4.1 Implementation 4.2 Benchmarks 4.3 UIO Experiments 4.4 ADS Experiments 5 Conclusions and Future Work References A Note on the Message Complexity of Cidon's Distributed Depth-First Search Algorithm 1 Introduction 2 Cidon's DDFS Algorithm 3 On the Message Complexity of Cidon's Algorithm 4 Conclusion References Minesweeper is Difficult Indeed! 1 Introduction 2 Related Work 3 Notations 4 Minesweeper Consistency and Inference 5 Simulating Circuits in Minesweeper 6 Templates for Circuit Synthesis 6.1 Removing and Gates from Boolean Circuits 6.2 Design Principles for Templates 6.3 Templates for Gate Layers 6.4 Wire Templates 6.5 Templates for the Literal Layer 6.6 Templates for Connecting Layers 7 NP-completeness of Minesweeper Consistency 8 Conclusions References Goodbye ioco 1 Introduction 2 Preliminaries 3 Examples 4 Test Observations 5 Refinement 6 Canonical Implementations 7 Relating Relations 8 Concluding Remarks References Process Algebras and Flocks of Birds 1 Introduction 2 A Simplified Model of a Flocking Behaviour 3 Analysis of Cohesion 4 Revising the Model 5 Conclusion References The Integration of Testing and Program Verification *9pt 1 Introduction 2 Strengths and Weaknesses of Testing and Verification 3 Our Vision 4 Challenges 4.1 Challenges for Integration 4.2 Challenges for Testing 4.3 Challenges for Deductive Verification 5 Conclusion References Discovering Directly-Follows Complete Petri Nets from Event Data 1 Introduction 2 Preliminaries 3 Directly-Follows Completeness 4 Subclasses of Accepting Petri Nets Relevant for Process Mining 5 The 1.0 and 1.1 Algorithms 6 The 2.0 Algorithm 7 Discussion 8 Conclusion References Fair Must Testing for I/O Automata 1 Introduction 2 I/O Automata 3 Testing Preorders 4 Testing Preorders for I/O Automata 5 May Testing 6 Must Testing Based on Progress 7 Must Testing Based on Fairness 8 Action-Based Must Testing 9 Fair Must Testing Agrees with the Fair Traces Preorder 10 Reward Testing 11 Conclusion References Passive Automata Learning: DFAs and NFAs 1 Introduction 2 Finding a Smallest DFA 3 Finding a Smallest NFA 4 Results References Author Index This Festschrift, dedicated to Frits W. Vaandrager on the occasion of his 60th birthday, contains papers written by many of his closest collaborators. Frits has been a Professor of Informatics for Technical Applications at Radboud University Nijmegen since 1995, where his research focuses on formal methods, concurrency theory, verification, model checking, and automata learning. The volume contains contributions of colleagues, Ph.D. students, and researchers with whom Frits has collaborated and inspired, reflecting a wide spectrum of scientific interests, and demonstrating successful work at the highest levels of both theory and practice.