V. Rusu. Verifying that Invariants are Context-Inductive. In 
Theorem Proving in Higher-Order Logics (TPHOLs'01), emerging trends paper.
University of Edinburgh, Informatics Research Report EDI-INF-RR-0046,
pp. 337-351.



Abstract:
We study the deductive verification of infinite-state systems modeled by 
extended automata. Typically, this process requires proving many invariants,
and automatically discharging these proof obligations would save the user a
significant amount of effort. To accomplish this we present techniques for
automatically verifying that invariants are inductive in a given context, and
identify a class of systems and a logic for expressing  invariants and contexts
for which the problem is decidable.