Reachability in Trace-Pushdown Systems

TL;DR

This paper extends classical pushdown system analysis to trace-pushdown systems with Mazurkiewicz traces, proving the reachability relation is lc-rational and decidability results for configuration reachability.

Contribution

It introduces lc-rational relations for trace-pushdown systems and proves their properties, generalizing classical pushdown system results and enabling decidability of reachability.

Findings

Reachability relation in trace-pushdown systems is lc-rational.

Forward reachability preserves rationality; backward reachability preserves recognizability.

Decidability of reachability between recognizable and rational configuration sets.

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).