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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
D. Lehmann, A. Pnueli and J. Stavi, Impartiality, justice and fairness: the ethics of concurrent termination, LNCS 115, 264–277 (1981).
J. Quielle and J. Sifakis, Fairness and related properties in transition systems, Acta Informatica 19, 195–220 (1983).
M. Hennessy, Axiomatising finite delay operators, Acta Informatica 21, 61–88 (1984).
N. Francez, Fairness, Springer-Verlag (1986).
C. Courcoubetis, M. Vardi and W.Wolper, Reasoning about fair concurrent programs, POPL (1986).
R. Milner, A Calculus of Communicating Systems, LNCS 92 (1980).
D. Walker, Introduction to a Calculus of Communicating Systems, University of Edinburgh report ECS-LFCS-87-22 (1987).
R. Milner, Communication and Concurrency, Prentice-Hall (1989).
D. Walker, Bisimulations and Divergence, Proc. LICS 186–192 (1989).
C. Stirling, Modal logics for communicating systems, TCS 49, 311–347 (1987).
M. Hennessy and C. Stirling, The power of the future perfect in program logics, Information and Control 67, 23–52 (1985).
E. Clarke and O. Grümberg, Research on automatic verification of finite-state concurrent systems, Ann. Rev. Comput. Sci. 2, 269–290 (1987).
R. Cleaveland, J. Parrow and B. Steffen, The Concurrency Workbench, this volume.
K. Larsen, A context-dependent bisimulation between process TCS (1988).
C. Stirling and D. Walker, Local model checking in the modal mu-calculus, in LNCS 351, 369–383 (1989).
R. Cleaveland, Tableau based model checking in the propositional mu-calculus, submitted for publication.
K. Larsen, Proof systems for Hennessy-Milner logic with recursion, in Proc. CAAP 88.
A. Emerson and C. Lei, Efficient model checking in fragments of the propositional mu-calculus, Proc. LICS, 267–278 (1986).
H. Barringer, R. Kuiper, and A. Pnueli, Now you may compose temporal logic specifications, 16th STOC (1984).
E. Emerson and E. Clarke, Characterising correctness properties of parallel programs as fix-points, LNCS 85 (1981).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stirling, C., Walker, D. (1990). CCS, liveness, and local model checking in the linear time mu-calculus. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_14
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive