Skip to main content

About this book

This book constitutes the refereed proceedings of the 14th International Conference on Reachability Problems, RP 2020, held in Paris, France in October 2020.

The 8 full papers presented were carefully reviewed and selected from 25 submissions. In addition, 2 invited papers were included in this volume. The papers 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.

Table of Contents


Invited Papers


On Decision Problems for Substitutions in Symbolic Dynamics

In this survey, we discuss decidability issues for symbolic dynamical systems generated by substitutions. Symbolic dynamical systems are discrete dynamical systems made of infinite sequences of symbols, with the shift acting on them. Substitutions are simple rules that replace letters by string of letters and allow the generation of infinite words. We focus here on symbolic dynamical systems that are generated by infinite compositions of substitutions, allowing to go beyond the case of the iteration of a single substitution. This is the so-called S-adic framework. Motivated by decidability and ergodic questions, we focus on questions dealing with the convergence of products of nonnegative matrices and associated Lyapunov exponents.
Valérie Berthé

Games with Full, Longitudinal, and Transverse Observability

Design and control of multi-agent systems correspond to the synthesis of winning strategies in games that model the interaction between the agents. In games with full observability, the strategies of players depend on the full history of the play. In games with partial observability, strategies depend only on observable components of the history. We survey two approaches to partial observability in two-player turn-based games with behavioral winning conditions. The first is the traditional longitudinal observability, where in all vertices, the players observe the assignment only to an observable subset of the atomic propositions. The second is the recently studied transverse observability, where players observe the assignment to all the atomic propositions, but only in vertices they own.
Orna Kupferman

Regular Papers


Reachability Set Generation Using Hybrid Relation Compatible Saturation

Generating the state space of any finite discrete-state system using symbolic algorithms like saturation requires the use of decision diagrams or compatible structures for encoding its reachability set and transition relations. For systems that can be formally expressed using ordinary Petri Nets (PN), implicit relations, a static alternative to decision diagram-based representation of transition relations, can significantly improve the performance of saturation. However, in practice, some systems require more general models, such as self-modifying Petri nets, which cannot currently utilize implicit relations and thus use decision diagrams that are repeatedly rebuilt to accommodate the changing bounds of the system variables, potentially leading to overhead in saturation algorithm. This work introduces a hybrid representation for transition relations, that combines decision diagrams and implicit relations, to reduce the rebuilding overheads of the saturation algorithm for a general class of models. Experiments on several benchmark models across different tools demonstrate the efficiency of this representation.
Shruti Biswal, Andrew S. Miner

Case Study: Reachability and Scalability in a Unified Combat-Command-and-Control Model

Reachability analysis computes an envelope encompassing the reachable states of a hybrid automaton within a given time horizon. It is known to be a computationally intensive task. In this case study paper, we consider the application of reachability analysis on a mathematical model unifying two key warfighting functions: Combat, and Command-and-Control (C2). Reachability here has a meaning of whether, given a range of initial combat forces and a C2 network and various uncertainties, one side can survive combat with intact forces while the adversary is diminished to zero. These are questions which arise in military Operations Research (OR). This paper is the first to utilize the notions of a hybrid automaton and reachability analysis in the area of OR. We explore the applicability and scalability of Taylor-model based reachability techniques in this domain. Our experiments demonstrate the potential of reachability analysis in the context of OR.
Sergiy Bogomolov, Marcelo Forets, Kostiantyn Potomkin

Qualitative Multi-objective Reachability for Ordered Branching MDPs

We study qualitative multi-objective reachability problems for Ordered Branching Markov Decision Processes (OBMDPs), or equivalently context-free MDPs, building on prior results for single-target reachability on Branching Markov Decision Processes (BMDPs).
We provide two separate algorithms for “almost-sure” and “limit-sure” multi-target reachability for OBMDPs. Specifically, given an OBMDP, \(\mathcal {A}\), given a starting non-terminal, and given a set of target non-terminals K of size \(k = |K|\), our first algorithm decides whether the supremum probability, of generating a tree that contains every target non-terminal in set K, is 1. Our second algorithm decides whether there is a strategy for the player to almost-surely (with probability 1) generate a tree that contains every target non-terminal in set K. The two separate algorithms are needed: we give examples showing that indeed “almost-sure” \(\not =\) “limit-sure” for multi-target reachability in OBMDPs. Both algorithms run in time \(2^{O(k)} \cdot |\mathcal {A}|^{O(1)}\), where \(|\mathcal {A}|\) is the bit encoding length of \(\mathcal {A}\). Hence they run in P-time when k is fixed, and are fixed-parameter tractable with respect to k. Moreover, we show that the qualitative almost-sure (and limit-sure) multi-target reachability decision problem is in general NP-hard, when k is not fixed.
Kousha Etessami, Emanuel Martinov

Quantum-over-Classical Advantage in Solving Multiplayer Games

We study the applicability of quantum algorithms in computational game theory and generalize some results related to Subtraction games, which are sometimes referred to as one-heap Nim games.
In quantum game theory, a subset of Subtraction games became the first explicitly defined class of zero-sum combinatorial games with provable separation between quantum and classical complexity of solving them. For a narrower subset of Subtraction games, an exact quantum sublinear algorithm is known that surpasses all deterministic algorithms for finding solutions with probability 1.
Typically, both Nim and Subtraction games are defined for only two players. We extend some known results to games for three or more players, while maintaining the same classical and quantum complexities: \(\varTheta \left( n^2\right) \) and \(\tilde{O}\left( n^{1.5}\right) \) respectively.
Dmitry Kravchenko, Kamil Khadiev, Danil Serov, Ruslan Kapralov

Efficient Restrictions of Immediate Observation Petri Nets

In a previous paper we introduced immediate observation Petri nets [9], a subclass of Petri nets with application domains in distributed protocols and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties [9, 14], but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, and it is polynomial for the second restriction with applications in chemical settings.
Michael Raskin, Chana Weil-Kennedy

Binary Expression of Ancestors in the Collatz Graph

The Collatz graph is a directed graph with natural number nodes and where there is an edge from node x to node \(T(x)=T_0(x)=x/2\) if x is even, or to node \(T(x)=T_1(x)=\frac{3x+1}{2}\) if x is odd. Studying the Collatz graph in binary reveals complex message passing behaviors based on carry propagation which seem to capture the essential dynamics and complexity of the Collatz process. We study the set \(\mathcal {E}\text {Pred}_k(x)\) that contains the binary expression of any ancestor y that reaches x with a limited budget of k applications of \(T_1\). The set \(\mathcal {E}\text {Pred}_k(x)\) is known to be regular, Shallit and Wilson [EATCS 1992]. In this paper, we find that the structure of the Collatz graph naturally leads to the construction of a regular expression, \(\texttt {reg}_{k}(x)\), which defines \(\mathcal {E}\text {Pred}_k(x)\). Our construction, is exponential in k which improves upon the doubly exponentially construction of Shallit and Wilson. Furthermore, our result generalises Colussi’s work on the \(x = 1\) case [TCS 2011] to any natural number x, and gives mathematical and algorithmic (Code available here: https://​github.​com/​tcosmo/​coreli.) tools for further exploration of the Collatz graph in binary.
Tristan Stérin

The Collatz Process Embeds a Base Conversion Algorithm

The Collatz process is defined on natural numbers by iterating the map \(T(x) = T_0(x) = x/2\) when \(x\in \mathbb {N}\) is even and \(T(x)=T_1(x) =(3x+1)/2\) when x is odd. In an effort to understand its dynamics, and since Generalised Collatz Maps are known to simulate Turing Machines [Conway, 1972], it seems natural to ask what kinds of algorithmic behaviours it embeds. We define a quasi-cellular automaton that exactly simulates the Collatz process on the square grid: on input \(x\in \mathbb {N}\), written horizontally in base 2, successive rows give the Collatz sequence of x in base 2. We show that vertical columns simultaneously iterate the map in base 3. This leads to our main result: the Collatz process embeds an algorithm that converts any natural number from base 3 to base 2. We also find that the evolution of our automaton computes the parity of the number of 1s in any ternary input. It follows that predicting about half of the bits of the iterates \(T^i(x)\), for \(i = O(\log x)\), is in the complexity class NC\(^1\) but outside AC\(^0\). These results show that the Collatz process is capable of some simple, but non-trivial, computation in bases 2 and 3, suggesting an algorithmic approach to thinking about prediction and existence of cycles in the Collatz process.
Tristan Stérin, Damien Woods

The Complexity of the Label-Splitting-Problem for Flip-Flop-Nets

Let \(\tau \) be a type of nets. Synthesis consists in deciding whether a given labelled transition system (TS) A can be implemented by a net N of type \(\tau \). In case of a negative decision, it may be possible to convert A into an implementable TS \(A'\) by relabeling edges that previously had the same label differently: Label-splitting is the problem to decide for a TS A and a natural number \(\kappa \) whether there is an implementable TS B with at most \(\kappa \) labels, which is derived from A by splitting labels. In this paper, we show that label-splitting is NP-complete if \(\tau \) corresponds to the type of flip-flop nets or some flip-flop net derivatives.
Ronny Tredup


Additional information