Joining Transition Systems of Records: Some Congruency and Language-Theoretic Results

TL;DR

This paper explores the properties of labeled transition systems of records, focusing on congruence relations under the join operation, and introduces language-theoretic definitions, revealing limitations in B"uchi automata of records.

Contribution

It generalizes B"uchi automata of records to labeled transition systems, analyzes their equivalence relations, and establishes language-theoretic characterizations of the join operation.

Findings

Finite-traces, infinite-traces, and NFA-based equivalences are congruences under join.

B"uchi acceptance-based equivalence is not a congruence.

No language-based, structure-independent join definition exists for B"uchi automata of records.

Abstract

B\"uchi automaton of records (BAR) has been proposed as a basic operational semantics for Reo coordination language. It is an extension of B\"uchi automaton by using a set of records as its alphabet or transition labels. Records are used to express the synchrony between the externally visible actions of coordinated components modeled by BARs. The main composition operator on the set of BARs is called as join which is the semantics of its counterpart in Reo. In this paper, we define the notion of labeled transition systems of records as a generalization of the notion of BAR, abstracting away from acceptance or rejection of strings. Then, we consider four equivalence relations (semantics) over the set of labeled transition systems of records and investigate their congruency with respect to the join composition operator. In fact, we prove that the finite-traces-based, infinite-traces-based, and nondeterministic finite automata (NFA)-based equivalence relations all are congruence relations over the set of all labeled transition systems of records with respect to the join operation. However, the equivalence relation using B\"uchi acceptance condition is not so. In addition, using these results, we introduce the language-theoretic definitions of the join operation considering both finite and infinite strings notions. Also, we show that there is no language-based and structure-independent definition of the join operation on B\"uchi automata of records.