Characteristic Formulae for CCS with Divergence

Bernhard Steffen

Abstract: Characteristic formulae have been introduced by Graf and Sifakis to relate equational reasoning about processes to reasoning in a modal logic, and therefore to allow proofs about processes to be carried out in a logical framework. Based upon an intuitionistic understanding of the modal mu-calculus, this paper extends the results of Graf and Sifakis in two respects. First, it covers not only finite processes, but finite state processes. Second, it handles not only bisimulation-like equivalences but also preorders, which are sensitive to liveness properties.


Previous | Index | Next