Domain Reduction Abstraction

Abstract

We suggest "domain reduction abstraction" for model checking systems with numeric guarding conditions and data transition constraints. The technique abstracts the domain of data variables using "data equivalence" and "trajectory reduction" in order to reduce the (possibly infinite) state space. Earlier work introduced the technique for systems with no data constraints or deterministic data constraints. Here, we extend the work to "non-deterministic constrained data transition systems". We provide a formal definition andproof of the soundness of the technique, and illustrate the abstraction technique with a small example.