Name
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.entcs.2004.04.043 | Electronic Notes in Theoretical Computer Science |
Keywords | DocType | Volume |
π-calculus,Symbolic Transition Graph,π-μ-logic,Model Checking Algorithm | Journal | 123 |
ISSN | Citations | PageRank |
1571-0661 | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Taolue Chen | 1 | 599 | 53.41 |
| Tingting Han | 2 | 98 | 7.34 |
| Jian Lu | 3 | 155 | 17.81 |