Underapproximating predicate transformers

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. © Springer-Verlag Berlin Heidelberg 2006.