Mu-Calculus with explicit points and approximations

Dam, Mads and Gurov, Dilian (2002) Mu-Calculus with explicit points and approximations. Journal of Logic and Computation, 12 (2). pp. 255-269.

Full text not available from this repository.


We present a Gentzen-style sequent calculus for program verification which accomodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture,and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.

Item Type:Article
ID Code:2896
Deposited On:08 Sep 2009
Last Modified:18 Nov 2009 16:14

Repository Staff Only: item control page