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.
Preview
Unable to display preview. Download preview PDF.
References
N. Benton, G. Bierman, and V. de Paiva. Computational types from a logical perspective I. Draft Technical Report, Computer Laboratory University of Cambridge, U.K., August 1993.
B. Chellas. Modal Logic. Cambridge University Press, 1980.
H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249–265, 1952.
H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957.
M. Dummett. Elements of Intuitionism. Clarendon Press, Oxford, 1977.
W. B. Ewald. Intuitionistic tense and modal logic. Journal of Symbolic Logic, 51, 1986.
M. Fairtlough and M. Mendier. An intuitionistic modal logic with applications to the formal verification of hardware. Technical Report ID-TR:1994-13, Department of Computer Science, Technical University of Denmark, 1994.
G. Fischer-Servi. Semantics for a class of intuitionistic modal calculi. In M. L. Dalla Chiara, editor, Italian Studies in the Philosophy of Science, pages 59–72. Reidel, 1980.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.
L. L. Maksimova. On maximal intermediate logics with the disjunction property. Studia Logica, 45:69–45, 1986.
M. Mendler. Constrained proofs: A logic for dealing with behavioural constraints in formal hardware verification. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, pages 1–28. Springer, 1990.
M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993.
E. Moggi. Computational lambda-calculus and monads. In Proceedings LICS'89, pages 14–23, June 1989.
G. Plotkin and C. Stirling. A framework for intuitionistic modal logics. In Theoretical aspects of reasoning about knowledge, pages 399–406, Monterey, 1986.
A. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, Department of Computer Science, 1994.
A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, volume II. North-Holland, 1988.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fairtlough, M., Mendler, M. (1995). An intuitionistic modal logic with applications to the formal verification of hardware. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022268
Download citation
DOI: https://doi.org/10.1007/BFb0022268
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60017-6
Online ISBN: 978-3-540-49404-1
eBook Packages: Springer Book Archive