Scholarlink

<p>This paper addresses the problem of the relationship between the correctness of the event diagram of distributed computing, from the standpoint of communication between the local processes of this computing, and the existence of a logical clock for that diagram. The problem is analyzed using the Coq Proof Assistant without assuming the fairness of the principle of excluded middle. That is, the obtained results are correct from the point of view of constructive logic, which is essential for computer science. The authors have formally proved that the existence of a logical clock for distributed computing ensures the irreflexivity of the causal relation related to that computing. They have also formulated the conjecture about the fairness of the converse statement.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Realizability of Event Diagrams and Existence of Logical Clocks

  • 期刊论文

  • 发表日期：

    2025年1月1日

查看全文
  • G. Zholtkevych,
  • A. Zozulia

摘要

This paper addresses the problem of the relationship between the correctness of the event diagram of distributed computing, from the standpoint of communication between the local processes of this computing, and the existence of a logical clock for that diagram. The problem is analyzed using the Coq Proof Assistant without assuming the fairness of the principle of excluded middle. That is, the obtained results are correct from the point of view of constructive logic, which is essential for computer science. The authors have formally proved that the existence of a logical clock for distributed computing ensures the irreflexivity of the causal relation related to that computing. They have also formulated the conjecture about the fairness of the converse statement.