Verifying Modal Formulas over I/O-Automata by means of Type Theory

Abstract

We introduce the notion of an I/O-automaton over a signature Σ. Beside we introduce a modal logic to reason about such an I/O-automaton. The semantics of the logic is defined in terms of a given Σ-algebra. We illustrate how the question whether or not an execution in a given I/O-automaton is a model for formula ø can be reduced to an inhabitation problem in the Calculus of Inductive Constructions. Furthermore we present a proof for soundness and completeness.