Reachability Problems

Name: Reachability Problems | 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings
Brand: Springer
Price: 58.84 EUR
Availability: OnlineOnly

16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings

Anthony W. Lin Georg Zetzsche Igor Potapov(Herausgeber*in)

Springer (Verlag)

Erschienen am 12. Oktober 2022

XLIII, 179 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-031-19135-0 (ISBN)

58,84 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken