Reachability Problems: 15th International Conference, RP 2021, Liverpool, UK, October 25–27, 2021, Proceedings

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