The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse

要約

Milner のプロセス セマンティクス (1984) の正規表現モジュロ二相似性に関する公理化と表現可能性の問題は、デッドロック 0 と空のステップ ~1 を持つ式の完全なクラスでは困難であることが判明しました。
0 が使用可能な場合に 1 が追加されることで発生する現象について報告します。これにより、この困難の重大な理由が明らかになります。
つまり、1-free 正規表現の解釈はバイシミュレーション崩壊の下で閉じられますが、これは任意の正規表現の解釈には当てはまりません。
1-free 正規表現のプロセス グラフの解釈は、ループの存在と除去のプロパティ LEE を満たします。これは、バイシミュレーションの崩壊の下で保持されます。
LEE のこれらの機能は、1 フリー正規表現のモジュロ双類似性に対する等式証明システムが完全であること、およびプロセス グラフが 1 フリー正規表現の解釈と双類似であるかどうかが多項式時間で決定可能であることを示すために適用されました。
正規表現の解釈は一般的にプロパティ LEE を満たさないが、LEE は 1-transitions を持つグラフとしての洗練された解釈によって回復できることを示す (これはオートマトンのサイレントステップに似ている)。
これは、LEE が一般的な公理化と表現可能性の問題にも適していることを示唆しています。
しかし、対処する必要がある新しい現象が発生します。プロセス グラフのプロパティ「1 遷移と LEE を使用してプロセス グラフに洗練できる」という性質は、バイシミュレーションの崩壊下では保持されません。
LEE を満たす 2 つの 1 遷移を持つ 10 頂点グラフを提供します。このグラフでは、洗練されたプロパティを維持しながら、双相頂点のペアを互いに折りたたむことはできません。
これは、正規表現のプロセス解釈のイメージがバイシミュレーション崩壊の下で閉じられていないことを意味します。

要約(オリジナル)

Axiomatization and expressibility problems for Milner’s process semantics (1984) of regular expressions modulo bisimilarity have turned out to be difficult for the full class of expressions with deadlock 0 and empty step~1. We report on a phenomenon that arises from the added presence of 1 when 0 is available, and that brings a crucial reason for this difficulty into focus. To wit, while interpretations of 1-free regular expressions are closed under bisimulation collapse, this is not the case for the interpretations of arbitrary regular expressions. Process graph interpretations of 1-free regular expressions satisfy the loop existence and elimination property LEE, which is preserved under bisimulation collapse. These features of LEE were applied for showing that an equational proof system for 1-free regular expressions modulo bisimilarity is complete, and that it is decidable in polynomial time whether a process graph is bisimilar to the interpretation of a 1-free regular expression. While interpretations of regular expressions do not satisfy the property LEE in general, we show that LEE can be recovered by refined interpretations as graphs with 1-transitions refined interpretations with 1-transitions (which are similar to silent steps for automata). This suggests that LEE can be expedient also for the general axiomatization and expressibility problems. But a new phenomenon emerges that needs to be addressed: the property of a process graph `to can be refined into a process graph with 1-transitions and with LEE’ is not preserved under bisimulation collapse. We provide a 10-vertex graph with two 1-transitions that satisfies LEE, and in which a pair of bisimilar vertices cannot be collapsed on to each other while preserving the refinement property. This implies that the image of the process interpretation of regular expressions is not closed under bisimulation collapse.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google