Completeness of Fair ASM Refinement

This page documents the KIV specifications of the completeness proof for fair ASM refinement as described in G. Schellhorn: Completeness of Fair ASM Refinement, submitted to FACS. The specifications and proofs extend the ones of the completeness proof of ASM Refinement. They add a supplementary predicate 'fair' and define refinement based on behaviors (= fair runs). Again, they are organized in two layers, the first using algebraic transitions systems (no failures), the second ASMs (which adds syntactic ASM rules and failures). The two following sections describe the specifications of each layer.

To get an overview over the structure of the specifications of the first layer you can have a look at the development graph. We describe the important specifications bottom-up

The structure of the specifications of the second layer is also visualized by a development graph. The proof is not done by instantiating the one of transitions systems, but separately. Therefore the structure of the specifications is nearly identical to the first layer, although the formulas and proofs needed are somewhat more complex, due to the presence of failing (diverging) ASM rules.

Used basic libraries:

Here you can find all our publications.

Back to the overview of all KIV projects .
For general informations on KIV and a download site for the whole system refer to this page.

[Impressum] [E-Mail]