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.
CITATION STYLE
Aagaard, M. D., Melham, T. F., & O’Leary, J. W. (1999). Xs are for trajectory evaluation, booleans are for theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1703, pp. 202–218). Springer Verlag. https://doi.org/10.1007/3-540-48153-2_16
Mendeley helps you to discover research relevant for your work.