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