left

Liveness

right
AProVE Help SystemTechniquesLiveness

Liveness Problems

We only give a short introduction to the notions of liveness problems in the context of top rewrite systems. For a more detailed introduction we refer to [GZ '03].

Top Rewrite Systems

For a top symbol top a term t is called a top term if and only if t = top(t1, ..., tn) and all t1, ..., tn do not contain top.

A term rewrite system over the signature Σ ∪ {top} is a top rewrite system if all rules are either of the form

Liveness Property

The transformation techniques in AProVE can handle eventuality liveness problems where we start from top terms and wish to determine if we eventually reach a state (term) from the set G of good states (terms).

The set of good states G here is defined as the set of all states (terms) which do not contain any instances of a given term as a subterm.

For two examples of such liveness properties see Subsection 5.3 of [GZ '03].