Reachability Problems: 15th International Conference, RP 2021, Liverpool, UK, October 25–27, 2021, Proceedings (Lecture Notes in Computer Science, 13035)

This book constitutes the refereed proceedings of the 15th International Conference on Reachability Problems, RP 2021, held in Liverpool, UK in October 2021. The 6 full papers presented were carefully reviewed and selected from 27 submissions. In addition, 4 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. Chapter ‘Recent Advances on Reachability Problems for Valence Systems’ is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Preface Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference Sound Verification Procedures for Temporal Properties of Infinite-State Systems Continuous One-counter Automata Solitaire of Independence Linear-time Model Checking Branching Processes Depth-first Search in Directed Planar Graphs The Pseudo-Skolem Problem is Decidable The Edit Distance to k-Subsequence Universality Matching Patterns with Variables under Hamming Distance Runtime Monitoring for Markov Decision Processes Organization Abstracts of Invited Talks Quantitative vs. Weighted Automata Theorem Proving Using Clausal Resolution: From Past to Present Population Protocols: Beyond Runtime Analysis Algorithmic Self-Assembly and Molecular Robotics: Theory and Practice Recent Advances on Reachability Problems for Valence Systems Contents Invited Papers Quantitative vs. Weighted Automata 1 Introduction 2 Definitions of Quantitative and Weighted Automata 2.1 Quantitative Automata 2.2 Weighted Automata 3 Related Notions and Entities 3.1 Alternation 3.2 Games 3.3 Logic 3.4 Between Determinism and Nondeterminism 3.5 Approximations 3.6 Formal Verification and Synthesis References Theorem Proving Using Clausal Resolution: From Past to Present 1 Introduction 2 Propositional Temporal Logic 2.1 Normal Form 2.2 Resolution for Propositional Temporal Logic 3 Branching-Time Temporal Logics 4 First Order Temporal Logic 5 Normal Modal Logics 6 Conclusion References Population Protocols: Beyond Runtime Analysis 1 Introduction 2 Some Terminology 3 Verification of Population Protocols 3.1 Decidability and Complexity 3.2 A First Attempt at a Verification Tool 3.3 A New Proof Methodology: Stage Graphs 3.4 Population Protocols Decide Exactly the Presburger Predicates 3.5 Automatic Computation of Stage Graphs 4 Succinct Predicates and State Complexity 4.1 State Complexity: Upper Bounds 4.2 State Complexity: Lower Bounds 5 Conclusions and Future Work References Recent Advances on Reachability Problems for Valence Systems (Invited Talk) 1 Introduction 2 Reachability 3 Complexity 4 First-Order Logic with Reachability 5 Underapproximation I: Bounded Context Switching 6 Underapproximation II: Scope Boundedness References Regular Papers Improvements in Unfolding of Colored Petri Nets 1 Introduction 2 Preliminaries 2.1 Colored Petri Nets 2.2 P/T Nets 2.3 Integer Colored Petri Nets 2.4 Unfolding 3 Color Quotienting 3.1 Computing Stable Partitions 3.2 Stable Partition Algorithm for Integer CPNs 4 Color Approximation 4.1 Computing Color Approximation on Integer CPNs 5 Experiments 6 Conclusion References Reachability of Weakly Nonlinear Systems Using Carleman Linearization 1 Introduction 2 Preliminaries 2.1 Vectors, Norms, and Sets 2.2 Support Function 2.3 Kronecker Product 3 Carleman Linearization 4 Set Propagation 5 Reachability Algorithm 5.1 Error Bound 5.2 Obtaining a Sound Set-Propagation Algorithm 5.3 Reevaluation of the Error Term 6 Evaluation 6.1 Epidemic Model (SEIR) 6.2 Burgers Partial Differential Equation 7 Conclusions References Continued Fraction Approach to Gauss Reduction Theory 1 Background 1.1 Basics of Integer Geometry in the Plane 1.2 Sail and LLS Sequences 1.3 LLS Periods of GL(2,Z) Matrices 1.4 Reduced Matrices and Continuants 1.5 Difference of Sequences 2 Three Cases of GL(2,Z) Matrices 3 Techniques to Find Reduced Matrices PGL(2,Z)-Conjugate to a Given One 4 Technical Aspects of Reduced Matrices Computation 4.1 Continued Fraction Enumeration of Reduced Matrices 4.2 Matrices PGL(2,Z)-Conjugate to a Given One 4.3 Computation of LLS Sequences for Rational Angles 4.4 Periods of the LLS Sequences Corresponding to Matrices References Absent Subsequences in Words 1 Introduction 2 Basic Definitions 3 Combinatorial Properties of SAS and MAS 4 Algorithms 4.1 A Compact Representation of the SAS of a Word 4.2 A Compact Representation of the MAS of a Word References Minimal Number of Calls in Propositional Protocols 1 Introduction 1.1 Background and Motivation 1.2 Related Work 1.3 Plan of the Paper 2 Gossiping Logic 3 Minimal Number of Calls 3.1 Basic Call Structure of a Correct Propositional Protocol 3.2 Different Call Scenarios 3.3 The Main Result 4 Conclusions References Reachability is NP-Complete Even for the Simplest Neural Networks 1 Introduction 2 Preliminaries 3 NNReach is NP-Complete 3.1 Membership in NP 3.2 NP-Hardness 4 NP-Hardness Holds in Very Restricted Cases Already 4.1 Neural Networks of a Simple Structure 4.2 Neural Networks with Simple Parameters 5 Conclusion References Author Index This book constitutes the refereed proceedings of the 7th International Workshop on Reachability Problems, RP 2013, held in Uppsala, Sweden, in September 2013. The 19 revised papers (The 14 revised papers were carefully reviewed and selected from 24 submissions in addition to 5 invited talks) were carefully reviewed and selected from 24 submissions. Topics of interest include reachability for finite 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.