Reachability Problems : 17th International Conference, RP 2023, Nice, France, October 11–13, 2023, Proceedings

Preface
Organization
Abstracts of Invited Talks
Low Complexity Colorings of the Two-Dimensional Grid
How Complex Shapes Can RNA Fold Into?
Sleptsov Net Computing Resolves Modern Supercomputing Problems
Presentation-Only Submissions
Sleptsov Nets Are Turing-Complete
On Computing Optimal Temporal Branchings
Positivity Problems for Reversible Linear Recurrence Sequences
Discontinuous IVPs with Unique Solutions
Geometry of Reachability Sets of Vector Addition Systems
Semënov Arithmetic, Affine VASS, and String Constraints
Multiplicity Problems on Algebraic Series and Context-Free Grammars
Linear Loop Synthesis for Polynomial Invariants
Higher-Dimensional Automata Theory
Universality and Forall-Exactness of Cost Register Automata with Few Registers
History-Determinism vs. Simulation
Energy Büchi Problems
Reenterable Colored Petri Net Model of Ebola Virus Dynamics
Contents
Invited Papers
Randomness Quality and Trade-Offs for CA Random String Generators
1 Introduction
2 Definition and Notation
2.1 Cellular Automata
2.2 Boolean Functions
3 Theories of Randomness
3.1 Martin-Löf Randomness
3.2 Pseudo-randomness
3.3 FIPS-140-2 and 140-3 Tests
3.4 Marsaglia's Tests
3.5 Knuth's Tests
4 Pseudo-random Strings Generation
4.1 Radius One CA Rules
4.2 Radius Two CA Rules
References
Regular Papers
Complexity of Reachability Problems in Neural Networks
1 Introduction
2 Preliminaries and Network Reachability Problems
2.1 Basics on Constraint Satisfaction Problems CSP
3 Complexity Results for Reachability
4 Network Equivalence and Verification of Interval Property
5 Conclusion and Further Questions
References
Weakly Synchronous Systems with Three Machines Are Turing Powerful
1 Introduction
2 MSCs and Communicating Automata
3 Treewidth of Weakly Synchronous p2p MSCs
4 Reachability for Weakly Synchronous p2p Systems with 3 Machines
5 Conclusion
References
On the Identity and Group Problems for Complex Heisenberg Matrices
1 Introduction
2 Roadmap
3 Preliminaries
4 Properties of Omega-Matrices
5 The Identity Problem for Subsemigroups of H(n,Q(i))
6 Future Research
References
Reachability Analysis of a Class of Hybrid Gene Regulatory Networks
1 Introduction
2 Preliminary Definitions
3 Reachability Analysis Method
3.1 Different Classes of Hybrid Trajectories
3.2 Reachability Analysis Algorithm
4 Conclusion
References
Quantitative Reachability Stackelberg-Pareto Synthesis Is NEXPTIME-Complete
1 Introduction
2 Preliminaries and Studied Problem
2.1 Graph Games
2.2 Stackelberg-Pareto Synthesis Problem
3 Bounding Pareto-Optimal Payoffs
3.1 Improving a Solution
3.2 Crucial Step
4 Complexity of the SPS Problem
5 Conclusion and Future Work
References
Multi-weighted Reachability Games
1 Introduction
2 Preliminaries
2.1 Two-Player Multi-weighted Reachability Games
2.2 Studied Problems
3 Ensured Values
3.1 Fixpoint Algorithm
3.2 Time Complexity
3.3 Synthesis of Lexico-Optimal and Pareto-Optimal Strategies
4 Constrained Existence
References
On the Complexity of Robust Eventual Inequality Testing for C-Finite Functions
1 Introduction
2 Proof Outline
3 Proof of Theorem 1
References
Adaptive Directions for Bernstein-Based Polynomial Set Evolution
1 Introduction
2 Notation and Basics
2.1 Dynamical Systems
3 Representing Sets
4 Over-Approximating Parallelotope Images
4.1 Directions and Approximation
5 Adaptive Directions
5.1 Avoiding Coarser Approximations
5.2 Fitting All the Parallelotope Faces
6 Examples
7 Conclusions
References
Introducing Divergence for Infinite Probabilistic Models
1 Introduction
2 Divergence of Markov Chains
2.1 Markov Chains: Definitions and Properties
2.2 Divergent Markov Chains
2.3 An Algorithm for Divergent Markov Chains
3 (Un)Decidability Results
3.1 Probabilistic Pushdown Automata
3.2 Probabilistic Petri Nets
4 Illustration of Divergence
4.1 Probabilistic Channel Systems
4.2 Probabilistic Pushdown Automata
5 Conclusion and Perspectives
References
A Framework for the Competitive Analysis of Model Predictive Controllers
1 Introduction
2 Hybrid Automata and Competitive Analysis
2.1 The Cost of Control
2.2 Regret
3 Reachability and Competitive Analysis
4 CEGAR-Based Competitive Analysis
4.1 Initial Abstraction and Analysis
4.2 Reachability Status
4.3 Counterexample Analysis and Refinement
4.4 Human in the Loop
5 Implementation and Evaluation
5.1 Competitive Analysis Toolchain
5.2 Initial Abstraction and Training
5.3 Reachability Status
5.4 Counterexample Analysis and Retraining
5.5 Experiments
6 Conclusion
References
Matching Patterns with Variables Under Simon's Congruence
1 Introduction
2 Preliminaries
3 MatchUniv
4 MatchSimon
5 WESimon
6 Conclusions
References
HyperMonitor: A Python Prototype for Hyper Predictive Runtime Verification
1 Introduction
2 Related Work
3 Preliminaries
4 An Overview of the HPRV Procedure
4.1 Inductive Process Mining
4.2 Semantic-Driven Model Transformations
4.3 Hyper Projection over Additional Threads
4.4 Verification
4.5 HPRV Implementation
4.6 Case-Studies
5 Conclusions
References
Generalized ARRIVAL Problem for Rotor Walks in Path Multigraphs
1 Introduction
2 Mechanics and Tools for Rotor Routing in Multigraphs
2.1 Multigraphs
2.2 Rotor Structure
2.3 Configurations
2.4 Rotor Routing
2.5 Legal Routing and Arrival
2.6 Equivalence Classes of Rotors
2.7 Equivalence Classes of Particles
2.8 Sandpile Group
3 Main Results for Path Multigraphs
3.1 Case x=y=1
3.2 Case 0 < x < y Coprime
4 Harmonic and Arcmonic Functions in the Path
4.1 Definition of h and g
4.2 Stable Decomposition of Arcmonic Values
References
Author Index