A Generalized UNITY-style Temporal Logic Library
================================================
Author: Mark-Oliver Stehr

The contents of this packet is a formal development in Coq of a
generalized UNITY-style temporal logic library. The full details can be
found in the the thesis [2]. It goes beyond the development reported
in [1] in several points, including the generality of the system model
and in the rules for compositional verification.

[1] Mark-Oliver Stehr: Embedding UNITY into the Calculus of Inductive
Constructions , Fachbereichsbericht FBI-HH-B-214/98, Universität
Hamburg, Fachbereich Informatik, September 1998.

[2] Mark-Oliver Stehr: Programming, Specification, and Interactive
Theorem Proving - Towards a Unified Language based on Equational
Logic, Rewriting Logic, and Type Theory , Doctoral Thesis, Fachbereich
Informatik, Universität Hamburg, 2002.

Contents of the Package
=======================

Arith_suppl.v     supplementary material about natural numbers
Finite_types.v    supplementary material about finite types
EqdepT.v          dependent equality (adapted for Type)

init.v            common initialization file

WfT.v             Well-founded induction (adapted for Type)
WfT_nat.v         Well-founded relations for natural numbers (adapted for Type)

state_pred.v      state predicate and basic logical operators
safety.v          safety assertions and related theorems
liveness.v        liveness asserttions and related theorems
composition.v     compositionality theorems

abstract.v        abstract frame for labeled transition systems

var_state_ops.v   operations on variable state space
var_state_pred.v  predicates about (in)dependence of variables
var_elim.v        elimination theorem
var_abstract.v    abstract frame labeled transition systems with variables

cmt.v             instantitation of the library for a solution to
                  the common meeting time problem together with 
                  a correctness proof

WfTinf.v          well-founded induction (informative version)
WfTinf_nat.v      well-founded relations for natural numbers (informative version)

inf_liveness.v    informative version of liveness assertions and
                  new compositionality theorems

cmt3.v            extands previous example extended by a third party,
                  as an illustration of compositional verification of
                  liveness properties

The modules for dependent equality and well-founded relations are part
of the Coq library, but some modifications were necessary, which is why
they are included in this package.

Prerequisites
=============

The development has been tested with Coq Version 6.3.1-3 which can be
obtained from ftp.inria.fr/INRIA/coq/V6.3.1. Due to subtle changes in
the interpretation of proof scripts and in the syntax syntax it would
need to be adapted to work with later versions of Coq.

Loading the Development
=======================

After a fresh start of the Coq proof assistent there are the following
four options to load and reverify the library and the examples in this
pagackge.

Possibility 1
-------------

To load the UNITY-style logic for labelled transition systems:

   Load abstract.

This includes all basic definitions and theorems for safety, liveness,
and elementray compositionality theorems.

Possibility 2
-------------

To load the UNITY-style logic for labelled transition systems
with a dependently typed state space with variables:

   Load var_abstract.

This includes all of the above plus theorems specific to the structure
of the state space.

To further load the informative version of liveness assertions
together with extended compositionality results on top of the previous
development:

   Load inf_liveness .

Possibility 3
-------------

To initiate the verification of the classical common meeting time example:

   Load cmt .

In this case a concrete version of var_abstract is included.

Possibility 4
-------------

To initiate the verification of the common meeting time example
composed with a third party:

   Load cmt3 .

In this case a concrete version of var_abstract and a version of
inf_liveness for extended compositional reasoning is included.

Remark: The warning "failed to extract" is unproblematic, since
we are not concerned with program extraction.