Underapproximating Predicate Transformers
David A. Schmidt (Kansas State University)
Abstract
We study the underapproximation of the predicate transformers used to give semantics to the modalities in dynamic and temporal logic. Because predicate transformers operate on state sets, we define appropriate powerdomains for sound approximation. We study four such domains - two are based on "set inclusion" approximation, and two are based on "quantification" approximation - and we apply the domains to synthesize the most precise, underapproximating pre~ and pre transformers, in the latter case, introducing a focus operation. We also show why the expected abstractions of post and post~ are unsound, and we use the powerdomains to guide us to correct, sound underapproximations.