An intuitionistic modal logic with applications to the formal verification of hardware

Abstract

We investigate a novel intuitionistic modal logic, called Propositional Lax Logic, with promising applications to the formal verification of computer hardware. The logic has emerged from an attempt to express correctness ‘up to’ behavioural constraints — a central notion in hardware verification — as a logical modality. The resulting logic is unorthodox in several respects. As a modal logic it is special since it features a single modal operator O that has a flavour both of possibility and of necessity. As for hardware verification it is special since it is an intuitionistic rather than classical logic which so far has been the basis of the great majority of approaches. Finally, its models are unusual since they feature worlds with inconsistent information and furthermore the only frame condition is that the O-frame be a subrelation of the ⊃-frame. We provide the motivation for Propositional Lax Logic and present several technical results. We investigate some of its proof-theoretic properties, and present a cut-elimination theorem for a standard Gentzen-style sequent presentation of the logic. We further show soundness and completeness for several classes of fallible two-frame Kripke models. In this framework we present a concrete and rather natural class of models from hardware verification such that the modality O models correctness up to timing constraints.