Reachability Problems
16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings
Published on 12. October 2022
XLIII, 179 pages
978-3-031-19135-0 (ISBN)
Description
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.
More details
Series
Edition
1st ed. 2022
Language
English
Place of publication
Cham
Switzerland
Publishing group
Springer International Publishing
Product notice
Reflowable
Illustrations
XLIII, 179 p. 28 illus., 7 illus. in color.
ISBN-13
978-3-031-19135-0 (9783031191350)
DOI
10.1007/978-3-031-19135-0
Schweitzer Classification
Other editions
Additional editions
Anthony W. Lin | Georg Zetzsche | Igor Potapov
Reachability Problems
16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings
Book
10/2022
Springer
€58.84
Shipment within 15-20 days
Persons
Content
- Intro
- 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&HD
- 4 HD&ND
- References
- Unambiguity and Fewness for Nonuniform Families of Polynomial-Size Nondeterministic Finite Automata
- 1 Background and an Overview
- 1.1 Historical Background: Unambiguity and Fewness in Complexity Theory
- 1.2 Historical Background: Nonuniform Families of Finite Automata
- 1.3 New Challenges in This Work
- 2 Basic Notions and Notation
- 2.1 Numbers, Promise Problems, and Kolmogorov Complexity
- 2.2 Families of Finite Automata
- 2.3 Unambiguous and Few Computation Paths
- 3 Complexity Classes Defined by One-Way Head Moves
- 3.1 Definitions of New Complexity Classes
- 3.2 Class Separations
- 4 Complexity Classes Defined by Two-Way Head Moves
- 4.1 Case of Logarithmic and Polynomial Ceilings
- 4.2 Case of No Ceiling Restriction
- 5 A Discussion and Open Problems
- References
- The Stochastic Arrival Problem
- 1 Introduction
- 2 Preliminaries
- 2.1 Preliminary Results
- 3 PSPACE-hardness with Three or More Node Types
- 4 The {R,S}-Arrival Problems
- References
- On Higher-Order Reachability Games Vs May Reachability
- 1 Introduction
- 2 HFL(Z) and Reachability Problems
- 2.1 HFL(Z)
- 2.2 Relationship with Reachability Problems
- 2.3 Main Theorem
- 3 From Order-n Reachability Games to Order-(n+1) May-Reachability
- 4 From Order-(n+1) May-Reachability to Order-n Reachability Games
- 5 Applications
- 6 Related Work
- 7 Conclusion
- References
- Coefficient Synthesis for Threshold Automata
- 1 Introduction
- 2 Preliminaries
- 2.1 Threshold Automata
- 3 Undecidability of Coefficient Synthesis
- 3.1 Presburger Arithmetic with Divisibility
- 3.2 The Reduction
- 3.3 Wrapping Up
- 4 Conclusion
- References
- Subsequences in Bounded Ranges: Matching and Analysis Problems
- 1 Introduction
- 2 Basic Definitions
- 3 Matching Problems
- 4 Analysis Problems
- 5 Application: Subsequence Matching in Circular Words
- 6 Conclusions
- References
- Canonization of Reconfigurable PT Nets in Maude
- 1 Introduction
- 2 Background: PT Nets and Maude
- 2.1 Place-Transition (PT) Nets with Inhibitor Arcs
- 2.2 Rewriting Logic and the Maude System
- 3 The Running Example: A Self-healing Production Line
- 4 Encoding Rewritable PT Systems in Maude
- 4.1 Reachability Properties of Rewritable PT Systems
- 5 Canonization of Rewritable PT
- 5.1 Graph Isomorphism and Canonization: An Overview
- 5.2 Base Notations/Definitions for PT Canonization (in Maude)
- 5.3 Equivalences and Rewrite Rules: Making Rules Symmetric
- 5.4 Canonization and Reachability
- 6 PT Canonization and Verification: Does It Scale?
- 7 Conclusion, Open Issues and Ongoing Work
- References
- Author Index
