Reachability Problems
16th International Conference, RP 2022, Kaiserslautern, Germany, October 17–21, 2022, Proceedings
Page
%P
-
Chapter and Conference Paper
Decision Procedures for Sequence Theories
Sequence theories are an extension of theories of strings with an infinite alphabet of letters, together with a corresponding alphabet theory (e.g. linear integer arithmetic). Sequences are natural abstraction...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Learning Union of Integer Hypercubes with Queries
We study the problem of learning a finite union of integer (axis-aligned) hypercubes over the d-dimensional integer lattice, i.e., whose edges are parallel to the coordinate axes. This is a natural generalization...
-
Chapter
Regular Model Checking Revisited
In this contribution we revisit regular model checking, a powerful framework—pioneered by Bengt Jonsson et al.—that has been successfully applied for the verification of infinite-state systems, especially paramet...
-
Chapter and Conference Paper
Parameterized Synthesis with Safety Properties
Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g., in the form of distributed p...
-
Chapter and Conference Paper
Monadic Decomposition in Integer Linear Arithmetic
Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a Boolean combination of monadic predicates in the theory. Recently, V...
-
Chapter and Conference Paper
Probabilistic Bisimulation for Parameterized Systems
Probabilistic bisimulation is a fundamental not...
-
Chapter and Conference Paper
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Word equations are a crucial element in the theoretical foundation of constraint solving over strings. A word equation relates two words over string variables and constants. Its solution amounts to a function ...
-
Chapter and Conference Paper
Complexity Analysis of Tree Share Structure
The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a la...
-
Chapter and Conference Paper
Fair Termination for Parameterized Probabilistic Concurrent Systems
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameteri...
-
Article
A linear-time algorithm for the orbit problem over cyclic groups
The orbit problem is at the heart of symmetry reduction methods for model checking concurrent systems. It asks whether two given configurations in a concurrent system (represented as finite strings over some f...
-
Chapter and Conference Paper
Regular Symmetry Patterns
Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is computationally expensive. We ...
-
Chapter and Conference Paper
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols...
