Branch-Well-Structured Transition Systems and Extensions

TL;DR

A new notion of monotony is defined, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem.

Abstract

We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from another. Furthermore, the monotony condition is relaxed in the same way. While this retains the decidability of non-termination and boundedness, it appears that the coverability problem is undecidable. To this end, we define a new notion of monotony, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem.

Figures (8)

• Figure 1: The FIFO machine $\mathcal{M}_1$ (left), and the corresponding (incomplete) infinite reachability tree (right) with initial state $(q_0, \varepsilon)$. We see that the induced transition system is branch-wqo.
• Figure 2: The FIFO machine $\mathcal{M}_2$ (left) and the incomplete reachability tree from $(q_2, \varepsilon)$ (right).
• Figure 3: The Reduced Reachability Tree of $\mathcal{M}_1$ from $(q_0, \varepsilon)$. Note that $(q_0, a)$ is dead because it is subsumed by state $(q_0, \varepsilon)$. As a matter of fact, we have $(q_0, \varepsilon) \xrightarrow{*} (q_0, a)$ and $(q_0, \varepsilon) \leq_{p} (q_0, a)$. State $(q_1, b)$ is also dead but it is not subsumed.
• Figure 4: The FIFO machine $\mathcal{M}_3$
• Figure 5: The FIFO machine $\mathcal{M}_4$ (right) and the automata $\mathcal{A}_s$ and $\mathcal{A}_r$ (left) that recognize $\mathcal{L}_!$ and $\mathit{Pref}(\mathcal{L}_?)$ respectively intersect to give $\bar{\mathcal{M}}_{4,\mathcal{L}}$(below) which is branch-monotone.

Theorems & Definitions (70)

• Definition 2.1
• Proposition 2.2: erdos_partition_1956schmitz_algorithmic_2012
• Proposition 2.3: erdos_partition_1956
• Definition 2.4: finkel_reduction_1990
• Definition 2.5
• Theorem 2.6: finkel_well-structured_2001abdulla_algorithmic_2000
• Definition 2.7: blondin_well_2017
• Theorem 2.8: blondin_well_2017
• Proposition 2.9: blondin_well_2017
• Proposition 2.10: blondin_well_2017