Reachability Problems : 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17–21, 2022, Proceedings / edited by Anthony W. Lin, Georg Zetzsche, Igor Potapov.

Format:

Book

Contributor:

Lin, Anthony W., editor.

Zetzsche, Georg, editor.

Potapov, Igor, editor.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 13608

Language:

English

Subjects (All):

Machine theory.

Computer science.

Software engineering.

Logic programming.

Algorithms.

Computer science--Mathematics.

Formal Languages and Automata Theory.

Computer Science Logic and Foundations of Programming.

Software Engineering.

Logic in AI.

Design and Analysis of Algorithms.

Mathematics of Computing.

Local Subjects:

Formal Languages and Automata Theory.

Computer Science Logic and Foundations of Programming.

Software Engineering.

Logic in AI.

Design and Analysis of Algorithms.

Mathematics of Computing.

Physical Description:

1 online resource (215 pages)

Edition:

1st ed. 2022.

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2022.

Summary:

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.

Contents:

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

2 `Free' PCP

3 `Beyond Free' PCP

4 The Verbal PCP

5 Conclusions

2 Basic Definitions and Some Highlights of Prior Work

3 Higher Order Boundedness

4 Persistent Unboundedness

5 Conclusions and Open Issues

Regular Papers

Linearization, Model Reduction and Reachability in Nonlinear odes

3 Linearization and Dimension Reduction

4 Behaviour of the Global Error

5 Application to Reachability Analysis

6 Experiments

7 Conclusion

History-Deterministic Timed Automata Are Not Determinizable

2 Notations

3 D&lt

HD

4 HD&lt

ND

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

The Stochastic Arrival Problem

2.1 Preliminary Results

3 PSPACE-hardness with Three or More Node Types

4 The {R,S}-Arrival Problems

On Higher-Order Reachability Games Vs May Reachability

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

Coefficient Synthesis for Threshold Automata

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

Subsequences in Bounded Ranges: Matching and Analysis Problems

2 Basic Definitions

3 Matching Problems

4 Analysis Problems

5 Application: Subsequence Matching in Circular Words

6 Conclusions

Canonization of Reconfigurable PT Nets in Maude

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

Author Index.

Notes:

Includes bibliographical references and index.

Other Format:

Print version: Lin, Anthony W. Reachability Problems

ISBN:

9783031191350

3031191358