
Reachability Problems
Description
Alles über E-Books | Antworten auf Fragen rund um E-Books, Kopierschutz und Dateiformate finden Sie in unserem Info- & Hilfebereich.
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
Other editions
Additional editions

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
System requirements
File format: PDF
Copy protection: Watermark-DRM (Digital Rights Management)
System requirements:
- Computer (Windows; MacOS X; Linux): Use the free software Adobe Reader, Adobe Digital Editions, or any other PDF viewer of your choice (see eBook Help).
- Tablet/Smartphone (Android; iOS): Install the free app Adobe Digital Editions or another reading app for eBooks, e.g., PocketBook (see eBook Help).
- E-reader: Bookeen, Kobo, Pocketbook, Sony, Tolino and many more (only limited: Kindle).
The file format PDF always displays a book page identically on any hardware. This makes PDF suitable for complex layouts such as those used in textbooks and reference books (images, tables, columns, footnotes). Unfortunately, on the small screens of e-readers or smartphones, PDFs are rather annoying, requiring too much scrolling.
This eBook uses Watermark-DRM, a „soft” copy protection. This means that there are no technical restrictions to prevent illegal distribution. However, there is a personalised watermark embedded in the eBook that can be used to identify the purchaser of the eBook in the event of misuse and to provide evidence for legal purposes.
For more information, see our eBook Help page.