In: Arbeitspapiere der GMD, No. 1007. July 1996.
Abstract: We present a brief description of the SH-Verification tool. This tool comprises computing abstractions of finite-state behaviour representations as well as automata and temporal logic based verification approaches. To be suitable for the verification of so-called co-operating systems, a modified type of satisfaction relation (approximate satisfaction) is considered. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to fulfill a certain property called simplicity on the concrete (i.e. not abstracted) behaviour.