Name
Abstract | ||
|---|---|---|
In this paper we show that observation equivalence on CCS processes preserves temporal properties (drawn from a very general temporal logic encompassing standard linear and branching time logics). Moreover, relative to a progress requirement, we show that CCS processes are live. But it is also very important to be able to verify that a process has or lacks a temporal property. In Section 3 we briefly discuss the idea of local model checking, checking that a particular finitary process has a property. Finally in Section 4 we exhibit a correct model checker for a sublogic, the linear time mu-calculus, of the general temporal logic. |
Year | DOI | Venue |
|---|---|---|
1989 | 10.1007/3-540-52148-8_14 | computer aided verification |
Keywords | Field | DocType |
local model checking,linear time mu-calculus,model checking,linear time,temporal logic | Transition system,Computation tree logic,Discrete mathematics,Model checking,Computer science,Algorithm,Theoretical computer science,Linear temporal logic,Finitary,Equivalence (measure theory),Temporal logic,Liveness | Conference |
Volume | ISSN | ISBN |
407 | 0302-9743 | 0-387-52148-8 |
Citations | PageRank | References |
13 | 1.35 | 12 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Colin Stirling | 1 | 934 | 102.50 |
| David W. Walker | 2 | 1158 | 129.14 |