Proving correctness with respect to nondeterministic safety specifications (Q1182117)

We use nondeterministic automata of a particular type as specifications and consider the problem of proving that a specification \(L\) implements a safety specification \(H\). A safety specification is any specification with finite nondeterminism. We present a complete proof method for this problem. This method originally appeared in \textit{A. P. Sistla} [A complete proof system for proving correctness on nondeterministic safety specifications, Technical Correspondence TC-0060-8-89-378, JTE Laboratories Incorporated (1989)]. In our approach, we use history variables and multi-valued mappings from the states of \(L\) to the states of \(H\). Multi-valued mappings are essential to our proof method and are used in our method to satisfy the following property: If \(s\) and \(s'\) are reachable states in \(L\) such that \(L\) permits a transition from \(s\) to \(s'\) after engaging in an action ''\(a\)'', then for every state \(t'\) in \(H\) which is the image of \(s'\), there exists a state \(t\) in the image of \(s\) such that \(H\) permits a transition from \(t\) to \(t'\) after engaging in the action ''\(a\)''. Roughly speaking, the above property is similar to the property satisfied by a possibilities mapping in the reverse direction.