Strong Priority and Determinacy in Timed CCS

要約

優先順位を備えたプロセス代数の標準理論に基づいて、同期プログラミングの本質を捉えるように設計された「建設的リダクション」と呼ばれる新しいスケジューリング メカニズムを特定します。
この評価戦略の特徴的な特性は、共有メモリを使用したマルチキャスト同時通信の構築による決定性を達成することです。
クロックと優先順位によって拡張された CCS の技術設定では、大規模なクラスの「コヒーレント」プロセスに対して、建設的な削減のための合流特性が証明されました。
「ピボット可能性」と呼ばれるいくつかの制限の下では、プレフィックス、合計、並列合成、制限、および隠蔽の演算子によって一貫性が維持されることを示します。
これによりメモリと共有が可能になるため、優先順位のない CCS に関するミルナーの古典的合流理論に比べて、厳密に大きなクラスのプロセスをカバーすることができます。

要約(オリジナル)

Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called ‘constructive reduction’ which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of ‘coherent’ processes a confluence property for constructive reductions. We show that under some restrictions, called ‘pivotability’, coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner’s classical confluence theory for CCS without priorities.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google