## Verification Diagrams: Logic + Automata

*
Zohar Manna,
Henny Sipma
*
We use automata on infinite words to reduce the verification
of linear temporal logic (\ltl) properties over infinite-state systems to
the proof of first-order verification conditions and an
algorithmic language inclusion check. The automaton serves as a
temporal abstraction of the system, preserving a subset of both
safety and liveness properties. The first-order verification
conditions prove that the abstraction is conservative; the
algorithmic check verifies that the abstraction satisfies the
property. Automata precisely separate the combinatoric from the
logic part of the proof, such that the combinatoric part can be
handled completely by algorithmic methods.

In *Proceedings
of the7th Monterey Workshop: Modelling Software Systems
Structures in a Fastly Moving Scenario*, pp 226-237,
Santa Margherita, 2000.

Postscript,
PDF.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Wed Mar 28 16:10:48 PST 2001