Reachability Problems: 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17–21, 2022, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 15th International Conference on Reachability Problems, RP 2022, held in Kaiserslautern, Germany, in October 2022. The 8 full papers presented were carefully reviewed and selected from 14 submissions. In addition, 3 invited papers were included in this volume. The RP proceedings cover topics such as reachability for infinite state systems; rewriting systems; reachability analysis in counter/timed/cellular/communicating automata; Petri nets; computational aspects of semigroups, groups, and rings; reachability in dynamical and hybrid systems; frontiers between decidable and undecidable reachability problems; complexity and decidability aspects; predictability in iterative maps; and new computational paradigms. Preface Organization Abstracts of Invited Talks The Past and Future of Embedded Finite Model Theory Post’s Correspondence Problem: From Computer Science to Algebra Recent Advances on the Reachability Problem for VASSes by Examples Decidability Results for Context-Bounded Analysis of Systems SAT-Based Invariant Inference and Its Relation to Concept Learning Presentation-Only Submissions The Pseudo-Reachability Problem for Affine Dynamical Systems Pairwise Reachability Oracles and Preservers Under Failures On the Identity Problem for Unitriangular Matrices of Dimension Four On the Undecidability of Loop Analysis Skolem Meets Schanuel Subsequences with Gap Constraints: Complexity Bounds for Matching and Analysis Problems A Dynamic Programming Algorithm for a Maximum s-Clique Set on Trees Higher-Order Nonemptiness Step by Step A Universal Skolem Set of Positive Lower Density On the Computation of the Algebraic Closure of Finitely Generated Groups of Matrices Matching Patterns with Variables Under Edit Distance The Variance-Penalized Stochastic Shortest Path Problem Parameterized Safety Verification of Round-Based Shared-Memory Systems Program Specialization as a Tool for Solving Word Equations Distributed Controller Synthesis for Deadlock Avoidance The Membership Problem for Hypergeometric Sequences with Rational Parameters On the Expressive Power of String Constraints Weak Bisimulation Finiteness of Pushdown Systems with Deterministic Epsilon-Transitions Is 2-EXPTIME-Complete What Can Oracles Teach us About the Ultimate Fate of Life? Universal Complexity Bounds Based on Value Iteration and Application to Entropy Games Regular Path Queries in MillenniumDB On the Skolem Problem for Reversible Sequences Contents Invited Papers SAT-Based Invariant Inference and Its Relation to Concept Learning 1 Introduction 2 Preliminaries 3 Invariant Inference with Queries 3.1 Inference with Queries 3.2 The Inductiveness-Query Model 3.3 The Hoare-Query Model 3.4 Hoare-Queries vs. Inductiveness-Queries 3.5 PDR and Interpolation-Based Inference Cannot Be Implemented with Inductiveness Queries 4 Invariant Learning and Concept Learning with Queries 4.1 Complexity Comparison 4.2 Invariant Learning Cannot Be Reduced to Concept Learning 4.3 Counterexamples in Invariant Learning Are Inherently Ambiguous 5 From Exact Learning to Invariant Inference via the Fence Condition 5.1 The Boundary of Inductive Invariants 5.2 Inference from One-Sided Fence and Exact Learning with Restricted Queries 5.3 Inference from Two-Sided Fence and Exact Learning 6 Conclusion References Post's Correspondence Problem: From Computer Science to Algebra 1 Introduction 2 `Free' PCP 3 `Beyond Free' PCP 4 The Verbal PCP 5 Conclusions References The Past and Future of Embedded Finite Model Theory 1 Introduction 2 Basic Definitions and Some Highlights of Prior Work 3 Higher Order Boundedness 4 Persistent Unboundedness 5 Conclusions and Open Issues References Regular Papers Linearization, Model Reduction and Reachability in Nonlinear odes 1 Introduction 2 Preliminaries 3 Linearization and Dimension Reduction 4 Behaviour of the Global Error 5 Application to Reachability Analysis 6 Experiments 7 Conclusion References History-Deterministic Timed Automata Are Not Determinizable 1 Introduction 2 Notations 3 D