2015年
Formal Verification of the Ricart-Agrawala Mutual Exclusion Algorithm in N-Labeled Calculus
2015 INTERNATIONAL CONFERENCE ON CONTROL, AUTOMATION AND ARTIFICIAL INTELLIGENCE (CAAI 2015)
- 開始ページ
- 167
- 終了ページ
- 171
- 記述言語
- 英語
- 掲載種別
- 研究論文(国際会議プロシーディングス)
- 出版者・発行元
- DESTECH PUBLICATIONS, INC
Mutual exclusion algorithms are essential for contemporary programs having parallel processes, and they offer typical examples of verification of such time-concerned cooperating programs. Especially, the Ricart-Agrawala mutual exclusion algorithm for distributed systems is one of the outstanding and well-known algorithm not only practical but also theoretical. N-labeled calculus is investigated lately for verification and analysis of time-concerned cooperating program systems, especially those in the artificial intelligence area. It has high formality since they are based on the Peano arithmetic, one of the natural number theories. In this paper, the Ricart-Agrawala mutual exclusion algorithm is formally represented and verified in the calculus.
- リンク情報
- ID情報
-
- Web of Science ID : WOS:000375397000033