| A predicate spatial logic for mobile processes |
| |
| 引用本文： | LIN Huimin Laboratory for Computer Science,Institute of Software. Chinese Academy of Sciences,Beijing 100080,China. A predicate spatial logic for mobile processes[J]. 中国科学F辑(英文版), 2004, 47(3): 394-408. DOI: 10.1360/02yf0385 |
| |
| 作者姓名： | LIN Huimin Laboratory for Computer Science Institute of Software. Chinese Academy of Sciences Beijing 100080 China |
| |
| 作者单位： | LIN Huimin Laboratory for Computer Science，Institute of Software. Chinese Academy of Sciences，Beijing 100080，China |
| |
| 摘 要： | A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.
|
| 关 键 词： | modal logic predicate μ-calculus model checking mobile processes asynchronous π-calculus |
A predicate spatial logic for mobile processes |
| |
| Lin Huimin. A predicate spatial logic for mobile processes[J]. Science in China(Information Sciences), 2004, 47(3): 394-408. DOI: 10.1360/02yf0385 |
| |
| Authors: | Lin Huimin |
| |
| Affiliation: | Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080,China |
| |
| Abstract: | A modal logic for describing temporal as well as spatial properties of mobile processes, expressed in the asynchronous π-calculus, is presented. The logic has recursive constructs built upon predicate-variables. The semantics of the logic is established and shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm is developed to automatically check if a mobile process has properties described as formulas in the logic. The correctness of the algorithm is proved. |
| |
| Keywords: | modal logic predicate μ -calculus model checking mobile processes asynchronous π -calculus |
| 本文献已被 CNKI 万方数据 SpringerLink 等数据库收录！ |
