Abstract. This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prove a theorem that translates correctness results from trajectory evaluation over a four-valued lattice into a shallow embedding of temporal operators over Boolean streams. This translation connects the specialized world of trajectory evaluation to a general-purpose logic and provides the semantic basis for connecting additional decision procedures and model checkers.
Mark Aagaard, Thomas F. Melham, John W. O'Leary