Pairs of Languages Closed under Shuffle Projection

TL;DR

This paper investigates the properties of language pairs under shuffle projection, introduces automata-based formulations, and proves decidability results for regular languages, advancing understanding of language closure properties in formal language theory.

Contribution

It presents a new automata-based approach to characterize and decide closure of language pairs under shuffle projection, including conditions for decidability for regular languages.

Findings

Decidability of closure under shuffle projection for regular languages.

Introduction of multi-counter automata for shuffle projection analysis.

Conditions under which transductions are rational and decidable.

Abstract

Shuffle projection is motivated by the verification of safety properties of special parameterized systems. Basic definitions and properties, especially related to alphabetic homomorphisms, are presented. The relation between iterated shuffle products and shuffle projections is shown. A special class of multi-counter automata is introduced, to formulate shuffle projection in terms of computations of these automata represented by transductions. This reformulation of shuffle projection leads to construction principles for pairs of languages closed under shuffle projection. Additionally, it is shown that under certain conditions these transductions are rational, which implies decidability of closure against shuffle projection. Decidability of these conditions is proven for regular languages. Finally, without additional conditions, decidability of the question, whether a pair of regular languages is closed under shuffle projection, is shown. In an appendix the relation between shuffle projection and the shuffle product of two languages is discussed. Additionally, a kind of shuffle product for computations in S-automata is defined.