Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Unboundedness via Amalgamation

Ashwani Anand, Sylvain Schmitz, Lia Schütze, Georg Zetzsche

TL;DR

Inspired by recent algorithmic techniques on VAS, an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs is proposed, which subsumes a large class of infinite-state systems, including VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete.

Abstract

Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS' scope entirely, such as pushdown systems (PDS). Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete. Moreover, this abstract setting enables simple and general algorithmic solutions to unboundedness problems, which have received much attention in recent years. We present algorithms for the (i) simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii) computing priority downward closures, (iii) deciding whether a language is bounded, meaning included in $w_1^*\cdots w_k^*$ for some words $w_1,\ldots,w_k$, and (iv) effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems.

Verifying Unboundedness via Amalgamation

TL;DR

Inspired by recent algorithmic techniques on VAS, an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs is proposed, which subsumes a large class of infinite-state systems, including VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete.

Abstract

Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS' scope entirely, such as pushdown systems (PDS). Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete. Moreover, this abstract setting enables simple and general algorithmic solutions to unboundedness problems, which have received much attention in recent years. We present algorithms for the (i) simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii) computing priority downward closures, (iii) deciding whether a language is bounded, meaning included in for some words , and (iv) effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems.
Paper Structure (59 sections, 25 theorems, 30 equations, 6 figures, 1 table)

This paper contains 59 sections, 25 theorems, 30 equations, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Contributions
  3. Consequences
  4. Well-Quasi-Orders
  5. Amalgamation Systems
  6. Concatenative Amalgamation Systems
  7. Admissible Embeddings and Gaps.
  8. Conditions.
  9. Gap Languages.
  10. Effectiveness
  11. Example: Regular Languages
  12. Example: Vector Addition Systems
  13. Configurations and Semantics.
  14. Runs and Admissible Embeddings.
  15. Concatenative Amalgamation.
  16. ...and 44 more sections

Key Result

lemma 1

Let $L\subseteq\Sigma^*$ be a subsemigroup. Then exactly one of the following holds: (i) $L$ is bounded or (ii) $L$ contains two prefix-incomparable words.

Figures (6)

  • Figure 1: A finite automaton for \ref{['ex:nfa']}.
  • Figure 2: A VASS for \ref{['ex:vass']}.
  • Figure 3: Derivation tree embeddings for \ref{['ex:cfg']}.
  • Figure 4: The hierarchy of classes obtained by the operations $\cdot + \mathbb{N}$ and $\mathsf{Alg}(\cdot)$.
  • Figure 5: Gaps in the canonical decomposition of trees.
  • ...and 1 more figures

Theorems & Definitions (61)

  • proof : Proof of "$(\ref{['emptiness-decidable']})\Rightarrow(\ref{['sup-decidable']})$"
  • proof : Proof of "$(\ref{['sup-decidable']})\Rightarrow(\ref{['emptiness-decidable']})$"
  • lemma 1
  • proof
  • proof : Proof of "$(\ref{['emptiness-decidable']})\Rightarrow(\ref{['boundedness-decidable']})$"
  • proof : Proof of "$(\ref{['boundedness-decidable']})\Rightarrow(\ref{['emptiness-decidable']})$"
  • lemma 2: folklore
  • lemma 3: Leroux2019
  • proof
  • proof : Proof of "$(\ref{['emptiness-decidable']})\Rightarrow(\ref{['unary-effectively-regular']})$"
  • ...and 51 more