Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reachability in Trace-Pushdown Systems

Chris Köcher, Dietrich Kuske

TL;DR

This work extends Caucal's reachability results to trace pushdown systems where the pushdown stores Mazurkiewicz traces. It introduces lc_rational trace relations, a left closed refinement of rational relations, and develops a robust theory showing that the reachability relation of trace_pDS is lc_rational under natural transition structure conditions. Using forward and backward preservation properties of lc_rational relations, the authors show that backwards reachability preserves recognizability and forwards reachability preserves rationality, yielding polynomial-time decidability for questions about reaching a recognizable trace set from a rational trace set. The results generalize classical pushdown reachability to the trace setting and complement Zetzsche’s monoid-based decidability results by focusing on transition structures, achieving Caucal-like preservation in this richer setting.

Abstract

We consider the reachability relation of pushdown systems whose pushdown holds a Mazurkiewicz trace instead of just a word as in classical systems. Under two natural conditions on the transition structure of such systems, we prove that the reachability relation is lc-rational, a new notion that restricts the class of rational trace relations. We also develop the theory of these lc-rational relations to the point where they allow to infer that forwards-reachability of a trace-pushdown system preserves the rationality and backwards-reachability the recognizability of sets of configurations. As a consequence, we obtain that it is decidable whether one recognizable set of configurations can be reached from some rational set of configurations. All our constructions are polynomial (assuming the dependence alphabet to be fixed). These findings generalize results by Caucal on classical pushdown systems (namely the rationality of the reachability relation of such systems) and complement results by Zetzsche (namely the decidability for arbitrary transition structures under severe restrictions on the dependence alphabet).

Reachability in Trace-Pushdown Systems

TL;DR

This work extends Caucal's reachability results to trace pushdown systems where the pushdown stores Mazurkiewicz traces. It introduces lc_rational trace relations, a left closed refinement of rational relations, and develops a robust theory showing that the reachability relation of trace_pDS is lc_rational under natural transition structure conditions. Using forward and backward preservation properties of lc_rational relations, the authors show that backwards reachability preserves recognizability and forwards reachability preserves rationality, yielding polynomial-time decidability for questions about reaching a recognizable trace set from a rational trace set. The results generalize classical pushdown reachability to the trace setting and complement Zetzsche’s monoid-based decidability results by focusing on transition structures, achieving Caucal-like preservation in this richer setting.

Abstract

We consider the reachability relation of pushdown systems whose pushdown holds a Mazurkiewicz trace instead of just a word as in classical systems. Under two natural conditions on the transition structure of such systems, we prove that the reachability relation is lc-rational, a new notion that restricts the class of rational trace relations. We also develop the theory of these lc-rational relations to the point where they allow to infer that forwards-reachability of a trace-pushdown system preserves the rationality and backwards-reachability the recognizability of sets of configurations. As a consequence, we obtain that it is decidable whether one recognizable set of configurations can be reached from some rational set of configurations. All our constructions are polynomial (assuming the dependence alphabet to be fixed). These findings generalize results by Caucal on classical pushdown systems (namely the rationality of the reachability relation of such systems) and complement results by Zetzsche (namely the decidability for arbitrary transition structures under severe restrictions on the dependence alphabet).

Paper Structure

This paper contains 22 sections, 30 theorems, 89 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Trace Theory
  4. Automata and Word Languages
  5. Transducer and Word Relations
  6. Rational and Recognizable Trace Languages
  7. Rational Trace Relations
  8. Left and Right Application
  9. Convention
  10. Trace-Pushdown Systems and Problem Statement
  11. LC-Rational Trace Relations
  12. LC-Rational Word Relations
  13. LC-Rational Trace Relations
  14. Products of lc-rational trace relations
  15. Preservation of language properties
  16. ...and 7 more sections

Key Result

Theorem 2.1

Let $\mathcal{D}=(A,D)$ be a dependence alphabet and $B_1,\dots,B_n\subseteq A$ sets of letters with $D=\bigcup_{1\le i\le n}B_i\times B_i$. For any words $u,v\in A^*$, $u\sim v$ if, and only if, $\pi_{B_i}(u)=\pi_{B_i}(v)$ for all $1\le i\le n$.

Figures (6)

  • Figure 1: Visualization of the diamond property \ref{['def:diamond1-DFA']} of an NFA. It states that whenever we find the black transitions with $a\parallel b$, we also find a state $q'$ with the red transitions.
  • Figure 2: Visualization of the diamond property \ref{["def:diamond1'"]} of a tPDS. It states that whenever we find the black transitions with $av\parallel bw$, we also find a state $q'$ with the red transitions.
  • Figure 3: Configuration graph of the tPDS from Example \ref{['ex:tPDS']}.
  • Figure 4: The trace-pushdown system from Example \ref{['ex:twophases-counterexample']}.
  • Figure 5: The trace-pushdown system $\mathfrak{P}=\mathfrak{P}^{(0)}$, $\mathfrak{P}^{(1)}$, and $\mathfrak{P}^{(2)}=\mathfrak{P}^{(\infty)}$ (from left to right). New transitions are marked in bold and red.
  • ...and 1 more figures

Theorems & Definitions (62)

  • Theorem 2.1: cf. Die90
  • Theorem 3.1: Zetzsche Zet21
  • definition 1
  • Lemma 3.2
  • proof
  • Theorem 4.1
  • proof
  • definition 2
  • Proposition 4.2
  • proof
  • ...and 52 more