Partially commuting pushdowns and rational trace relations

Sep 5 14:00 ₂₀₂₃

We consider the reachability problem for pushdown systems where the pushdown does not store a word, but a Mazurkiewicz trace. Since this model generalizes multi-pushdown systems, the reachability problem can only be solved for a restricted class that we call cooperating multi-pushdown systems (cPDS). In the talk, I will show how the saturation algorithm by Finkel et al. (1997) can be modified. For such saturated cPDS, the reachability relation can be shown to be a finite union of finite compositions of prefix-recognizable trace relations (for words, these relations were studied, e.g., by Caucal, 1992).

The second part of the talk presents results on rational relations on the trace monoid. An easy observation shows that these relations do not preserve recognizability nor rationality of languages, it follows that they do not compose. To safe these much appreciated properties of rational relations on the free monoid, I introduce a restricted class, called rc-rational relations. As an example, the above mentioned prefix-recognizable trace relations are rc-rational.

Thus, putting the two parts together, we obtain that the reachability relation of a cPDS is rc-rational. Consequently, a cPDS preserves the rationality of a set of configurations under forwards- and the recognizability under backwards-reachability.

(The results on cPDS were obtained together with Chris Köcher.)