Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9655948 | Electronic Notes in Theoretical Computer Science | 2005 | 15 Pages |
Abstract
The Ï-calculus is one of the most important mobile process calculi and has been well studied in the literatures. Temporal logic is thought as a good compromise between description convenience and abstraction and can support useful computational applications, such as model-checking. In this paper, we use symbolic transition graph inherited from Ï-calculus to model concurrent systems. A wide class of processes, that is, the finite-control processes can be represented as finite symbolic transition graph. A new version Ï-μ-Logic is introduced as an appropriate temporal logic for the Ï-calculus. Since we make a distinction between proposition and predicate, the possible interactions between recursion and first-order quantification can be solved. A concise semantics interpretation for our modal logic is given. Based on the above work, we provide a model checking algorithm for the logic, which follows the well-known Winskel's tag set method to deal with fixpoint operator. As for the problem of name instantiating, our algorithm follows the 'on-the-fly' style, and systematically employs schematic names. The correctness of the algorithm is shown.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Taolue Chen, Tingting Han, Jian Lu,