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.
|Deposited By:||INVALID USER|
|Deposited On:||08 Sep 2009|
|Last Modified:||18 Nov 2009 16:14|
Repository Staff Only: item control page