Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Separability and Non-Determinizability of WSTS

Wojciech Czerwiński, Eren Keskin, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K Narayan Kumar, Prakash Saivasan

TL;DR

This work analyzes languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility, proving that disjoint WSTS languages are regularly separable and that detWSTS languages form a strict subset of WSTS languages. It introduces converging transition systems (CTS) as a deterministic, lattice-based model that preserves expressiveness through finite invariants, and shows how to obtain regular separators from inductive invariants via finite representations. The paper also develops a detailed determinization theory, including a Nerode-order characterization of detWSTS languages and a witness language T demonstrating non-determinization, and extends the results to downward-compatible WSTS using ideal completion techniques. Collectively, these results provide a principled framework for regular separability and invariant-based verification in infinite-state systems, with implications for verification tooling and further theoretical study of determinization and separability.

Abstract

We study the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that every pair of disjoint WSTS languages is regularly separable: there is a regular language containing one of them while being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. Our second result shows that the languages recognized by deterministic WSTS form a strict subclass of the languages recognized by all WSTS: we give a non-deterministic WSTS language that we prove cannot be recognized by a deterministic WSTS. The proof relies on a novel characterization of the languages accepted by deterministic WSTS.

Separability and Non-Determinizability of WSTS

TL;DR

This work analyzes languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility, proving that disjoint WSTS languages are regularly separable and that detWSTS languages form a strict subset of WSTS languages. It introduces converging transition systems (CTS) as a deterministic, lattice-based model that preserves expressiveness through finite invariants, and shows how to obtain regular separators from inductive invariants via finite representations. The paper also develops a detailed determinization theory, including a Nerode-order characterization of detWSTS languages and a witness language T demonstrating non-determinization, and extends the results to downward-compatible WSTS using ideal completion techniques. Collectively, these results provide a principled framework for regular separability and invariant-based verification in infinite-state systems, with implications for verification tooling and further theoretical study of determinization and separability.

Abstract

We study the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that every pair of disjoint WSTS languages is regularly separable: there is a regular language containing one of them while being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. Our second result shows that the languages recognized by deterministic WSTS form a strict subclass of the languages recognized by all WSTS: we give a non-deterministic WSTS language that we prove cannot be recognized by a deterministic WSTS. The proof relies on a novel characterization of the languages accepted by deterministic WSTS.
Paper Structure (21 sections, 50 theorems, 28 equations, 4 figures)

This paper contains 21 sections, 50 theorems, 28 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Well-Structured Transition Systems
  3. Regular Separability
  4. Proof Principle
  5. Proving the Proof Principle
  6. Discussion
  7. A Deterministic Model for WSTS
  8. Finitely Represented Invariants in CTS
  9. A Closer Look at WSTS Determinization
  10. Determinizability
  11. Non-Determinizability
  12. Characterization of the detWSTS Languages
  13. Witness Language
  14. A Specialized Invariant Construction for detWSTS
  15. Ideal Completion
  16. ...and 6 more sections

Key Result

Lemma 2.1

Let $\mathit{U}$ be an ULTS. Then $\mathit{U}^{\mathit{det}}$ is a deterministic ULTS with $\mathit{L}(\mathit{U}^{\mathit{det}})=\mathit{L}(\mathit{U})$.

Figures (4)

  • Figure 1: Transition relation of $\mathcal{A}$.
  • Figure 2: Rado order with the column and row of $(3,5)$ marked (left), with the elements larger than $(3,5)$ marked (middle), and with the downward closure of column $3$ marked (right).
  • Figure 3: The effect of $a$ and $\bar{a}$-labeled transitions on column $3$ (left) and the effect of $\mathit{zero}$-labeled transitions on columns $0$ and $3$ (right).
  • Figure 4: Relations between language classes.

Theorems & Definitions (66)

  • Lemma 2.1
  • Lemma 2.2: JANCAR1999
  • Lemma 2.3
  • Lemma 2.4
  • Lemma 2.5
  • Theorem 3.1
  • Definition 3.2
  • Theorem 3.3
  • Lemma 3.4
  • Proposition 3.5
  • ...and 56 more