## Yes, Matilda! Abstraction can Replace Deduction, even for
Computational Models which are BAD (Buchi Automata with Data)

**Amir Pnueli**

Weizmann Institute of Science. Joint work (in progress) with
Y. Kesten and M. Vardi

**Abstract.**

In the KIT workshop on Hybrid Systems (Grenoble Oct., 1998), we
introduced the method of Verification by Finitary Abstraction (VFA). By
this method, in order to verify that an infinite-state system S
satisfies the temporal property f, one abstracts S into a finite-state
system S^A and abstracts f into a finite-state (propositional temporal
formula f^A, verifies S^A |= f^A by model checking, and then infers
that the original property f holds over the original system S. In the
talk, we presented a recipe for ensuring that the method is sound
(safe) for all LTL properties f. We also conjectured with high
probability that the method is also complete, namely, whenever S |= f,
there exists an abstraction mapping \alpha such that
S^{\a} |= f^{\a}. We formulated this conjecture by asking "Can
abstraction replace deduction?"

Since then, we have confirmed this conjecture and have shown that the
VFA method is indeed complete. A paper with these results have been
submitted to LICS99.

Moshe Vardi raised the question whether it is possible to
reformulate the VFA method and obtain similar completeness results
within the automata-theoretic framework. The topic of this talk is a
positive answer to his question.

To start with, we had to find out what is the automata-theoretic
version of a deductive system (assumed to be applicable to
infinite-state systems), which we have to replace. This led to the
computational model BAD (Buchi Automata with Data), which is a Buchi
(finite-state) automaton, equipped with additional state variables
that can range over infinite domains, and transition relations
(appearing as edge labels) referring and modifying these state
variables. Then we proposed a single deductive rule which is sound and
(relatively) complete for establishing the emptiness of a (potentially
infinite-state) BAD automaton, a problem to which all verification
problems can be reduced.

Having constructed the deductive method we wished to replace, we
immediately proceed to formulate the appropriate notion of abstraction
which is a particular type of a homomorphism, and show that it is
sound for Verification by Finitary Abstraction. Next, we utilize the
availability of the single complete deductive rule in order to
establish the completeness of the VFA method for the BAD models of
computation.