Taming the Infinities of Concurrency: Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday (Lecture Notes in Computer Science, 14660)

Javier Esparza received his primary degree in Theoretical Physics and in 1990 his PhD in Computer Science from the University of Zaragoza. After positions at the University of Hildesheim, the University of Edinburgh, and the Technical University of Munich, he then held professorships at the University of Edinburgh and the University of Stuttgart, and finally returned to TU Munich where he currently holds the Chair of Foundations of Software Reliability and Theoretical Computer Science. Javier is a leading researcher in concurrency theory, distributed and probabilistic systems, Petri nets, analysis of infinite-state models, and more generally formal methods for the verification of computer systems. He has coauthored over 200 publications, many of them highly influential. He coauthored the monographs Free Choice Petri Nets, and Unfoldings: A Partial Order Approach to Model Checking, and more recently the textbook Automata Theory: An Algorithmic Approach. The latter is an exampleof Javier’s many activities as a teacher, he has supervised more than 20 PhD students, taught at more than 20 summer schools, and won many awards for his university teaching. He is regularly invited to deliver plenary talks at prestigious computer science conferences and participate in senior program committees, he has contributed as a senior member of technical working groups, society councils, and journal editorial boards, and in 2021 he became a founding Editor-in-Chief of the open-access TheoretiCS journal. This Festschrift celebrates Javier’s contributions on the occasion of his 60th birthday, the contributions reflect the breadth and depth of his successes in Petri nets, concurrency in general, distributed and probabilistic systems, games, formal languages, logic, program analysis, verification, and synthesis. Preface Organization Contents Fairness and Liveness Under Weak Consistency 1 Introduction 2 Concurrency, Shared Memory, and Verification 2.1 Memory Models: Intuition 2.2 Memory Fairness: Intuition 3 Sequential Consistency (SC) 3.1 Model 3.2 Safety Properties 3.3 Fairness and Liveness 4 Total Store Order (TSO) 5 Fairness and Liveness Under TSO 5.1 Transition Fairness 5.2 Memory-Boundedness Transition (MBT) Fairness 5.3 Probabilistic Memory Fairness 5.4 Equivalence of Fairness Notions 6 Verification of Markov Chains 6.1 Necessity of Decisiveness 6.2 Attractors 6.3 Sufficiency of Finite Attractors 6.4 Getting Desired Finite Attractors 7 Conclusions and Future Work References Restricted Flow Games 1 Introduction 2 Preliminaries 2.1 Automata 2.2 Flow Games 2.3 Restricted Flow Games 3 Calculating the Outcome in Restricted Flow Games 3.1 Solving the Maximal and Minimal Outcome Problems 3.2 Solving the Positive Maximal and Minimal Outcome Problems 4 Calculating the Value in Restricted Flow Games 4.1 Solving the Maximum and Minimum Restricted Flow Problems 4.2 Solving the Positive Maximum and Minimum Restricted Flow Problems 5 Discussion 5.1 Memoryful Strategies 5.2 No Tolerance to Loss and Waste References SynthLearn: A Tool for Guided Reactive Synthesis 1 Introduction 2 Preliminaries 3 SynthLearn Algorithm 3.1 Testing P-Realizability of Safety Specifications Efficiently 3.2 Generalization Phase 3.3 Completion Phase 4 Case Studies 4.1 Variations on Mutual Exclusion Arbiters 4.2 Arbiter for a Three-Way Intersection 5 Conclusion References On Regular Expression Proof Complexity of Salomaa's Axiom System F1 1 Introduction 2 Preliminaries 3 Regular Expression Proof Complexity Within Salomaa's Axiom System F1 3.1 Equational Characterizations for Regular Expressions 3.2 From Equational Characterizations to the Equality of Regular Expressions 4 Proof Complexity of Regular Expressions in General References Hidden Markov Models with Unobservable Transitions 1 Introduction 2 Preliminaries 3 Probability Space and Random Variables 4 Finding the Best Explanation for an Observation 5 Parameter Learning 5.1 Conditional Expectation of the Number of Transition Traversals 5.2 Using the EM Algorithm 6 Contractivity 7 Runtime Results 8 Conclusion References Coverability in Well-Formed Free-Choice Petri Nets 1 Motivation 2 Some Context 3 T-Coverability 4 S-Coverability 5 Concluding Remarks References On Verifying Concurrent Programs Under Weak Consistency Models: Decidability and Complexity 1 Introduction 2 Program Semantics 2.1 Sequential Consistency 2.2 Total Store Order 3 Solving the State Reachability Problem 3.1 Reachability in Programs with a Fixed Number of Processes 3.2 The Parametric Reachability Problem 4 Overcoming Undecidability and High Complexity 4.1 Verifying Program Robustness 4.2 Context-Bounded Verification for Weak Memory Models 5 Conclusion References A Summary and Personal Perspective on Recent Advances in Privacy Risk Assessment in Digital Pathology Through Formal Methods 1 Introduction 1.1 How Is WSI Acquired 1.2 The Attacker Model 1.3 The Attack Model Implementation 1.4 Experimental Results 2 Conclusion References A Uniform Framework for Language Inclusion Problems 1 Introduction 2 Preliminaries 3 Algorithm 4 Quasiorder Instantiation 4.1 A State-Based Quasiorder 4.2 Other Quasiorders 5 Algorithmic Aspects 5.1 A State-Based Variant 5.2 A Data-Structure for the Case of Straight Line Programs 6 Other Language Inclusion Problems 6.1 REG REG 6.2 REG Petri Net Traces 6.3 Languages of Infinite Words 6.4 Pointers to Other Cases References On the Home-Space Problem for Petri Nets 1 Introduction 2 A General Approach to the Home-Space Problem 3 Semilinear Inductive Cores for Semilinear Sets 4 Home-Space Witnesses References Newton's Method – There and Back Again 1 Introduction 2 Motivation 3 Newton's Method: Iterated Linearization 4 Approximation by Unfolding 5 Convergence via Combinatorics on Trees 6 Conclusion References Template-Based Verification of Array-Manipulating Programs 1 Introduction 2 Template-Based Verification of Programs 2.1 Internal Program Representation 2.2 Template-Based Predicate Inference 2.3 Abstract Domains in 2LS 3 Abstract Domain for Arrays 3.1 Array Domain Template 3.2 Computing Array Segment Borders 3.3 Array Domain Invariant Inference 3.4 Running Example 4 Experimental Evaluation 5 Related Work 5.1 Methods Based on Array Segmentation 5.2 Methods Based on Analysis of Array-Manipulating Loops 5.3 Predicate Abstraction and Non-automatic Methods 6 Conclusions and Future Work References Memoryless Strategies in Stochastic Reachability Games 1 Introduction 2 Preliminaries 3 Martingales for Safety 4 Optimal Safety 5 -Optimal Reachability 6 Optimal Reachability 7 Conclusion and Related Work References Region Quadtrees Verified 1 Introduction 2 Isabelle Notation 3 Region Quadtrees 3.1 Functions 42 1000 63 1000 33 1000 58 1000 59 1000 44 1000 get and 42 1000 63 1000 33 1000 58 1000 59 1000 44 1000 put 3.2 Boolean Operations 3.3 Extracting Subimages 3.4 From and to Matrix 4 Matrix Quadtrees 4.1 Addition and Multiplication of Matrices 4.2 Addition and Multiplication of Quadtrees 5 Related Formalization Work 6 Conclusion References Computing pre* for General Context Free Grammars 1 Introduction 2 Preliminaries 3 Computing pre* for General Grammars 4 Unambiguous Grammars 5 Applications to Parsing 6 Some More Applications 7 Conclusion References 2-Pointer Logic 1 Introduction 2 Quantitative Equalities 3 Adding Dis-Equalities 4 Assignments 5 Related Work 6 Conclusion References Author Index Javier Esparza received his primary degree in Theoretical Physics and in 1990 his PhD in Computer Science from the University of Zaragoza. After positions at the University of Hildesheim, the University of Edinburgh, and the Technical University of Munich, he then held professorships at the University of Edinburgh and the University of Stuttgart, and finally returned to TU Munich where he currently holds the Chair of Foundations of Software Reliability and Theoretical Computer Science. Javier is a leading researcher in concurrency theory, distributed and probabilistic systems, Petri nets, analysis of infinite-state models, and more generally formal methods for the verification of computer systems. He has coauthored over 200 publications, many of them highly influential. He coauthored the monographs Free Choice Petri Nets, and A Partial Order Approach to Model Checking, and more recently the textbook Automata An Algorithmic Approach. The latter is an example of Javiers many activities as a teacher, he has supervised more than 20 PhD students, taught at more than 20 summer schools, and won many awards for his university teaching. He is regularly invited to deliver plenary talks at prestigious computer science conferences and participate in senior program committees, he has contributed as a senior member of technical working groups, society councils, and journal editorial boards, and in 2021 he became a founding Editor-in-Chief of the open-access TheoretiCS journal. This Festschrift celebrates Javiers contributions on the occasion of his 60th birthday, the contributions reflect the breadth and depth of his successes in Petri nets, concurrency in general, distributed and probabilistic systems, games, formal languages, logic, program analysis, verification, and synthesis.