Abstract

Tradition in the area of formal specification teaches that pure propositional logic is adequate for the stationary state of finite bit-level systems, but that in order to capture dynamic behaviour over time an enrichment by some form of extra temporal operators (predicate logic, temporal logic, modal logic) is necessary.

This talk will demonstrate that the opposite strategy is feasible too, namely that there are fragments of propositional logic in which it is possible to specify nontrivial classes of finite state behaviours. This is relevant for applications in Computer Science where the right trade-off between syntax and semantics is essential.

In the talk we will consider intuitionistic logic as a natural such fragment, which, though propositional in syntax, offers second-order expressiveness. We will look at two different ways of exploiting this semantic richness to accommodate timing behaviour. The first one generates a fully-abstract semantics for Statecharts, essentially solving the full-abstraction problem for this widely used engineering design language. The second fragment is related to Maximovas intermediate logic LPi (Logic of the Rhombuses), in which properties of finite bidirectional automata may be expressed.