A CTL-based logic for program abstractions

Abstract

We define an action-based extension of the branching-time temporal logic CTL which allows path quantifiers to be restricted by formal languages. The main purpose of this logic is its use in abstract interpretation. A reduction from a concrete system to an abstract one may contain spurious traces which can render the verification of the abstract system useless with respect to the concrete one. We pick up the suggestion to verify a modified property on the abstract system instead of the one that the concrete system is supposed to have. The logic introduced here enables a systematic modification of such properties. We present some ways of such a modification which aim at implicitly excluding spurious traces in the verification of abstracted systems. © 2010 Springer-Verlag.