Author name cluster

Michael Mendler

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

TCS Journal 2011 Journal Article

Constructive semantics for instantaneous reactions

Joaquín Aguado
Michael Mendler

This paper presents some results towards a game-theoretic account of the constructive semantics of step responses for synchronous languages, providing a coherent semantic framework encompassing both non-deterministic Statecharts (as per Pnueli & Shalev) and deterministic esterel. In particular, it is shown that esterel arises from a finiteness condition on strategies whereas Statecharts permits infinite games. Beyond giving a novel and unifying account of these concrete languages the paper sketches a general theory for obtaining different notions of constructive responses in terms of winning conditions for finite and infinite games and their characterisation as maximal post-fixed points of functions in directed complete lattices of intensional truth-values.

Details DOI

I&C Journal 2011 Journal Article

Cut-free Gentzen calculus for multimodal CK

Michael Mendler
Stephan Scheele

This paper extends previous work on the modal logic CK as a reference system, both proof-theoretically and model-theoretically, for a correspondence theory of constructive modal logics. First, the fundamental nature of CK is discussed and compared with the intuitionistic modal logic IK which is traditionally taken to be the base line. Then, it is shown, that CK admits of a cut-free Gentzen sequent calculus G - CK which has (i) a local interpretation in constructive Kripke models and (ii) does not require explicit world labels. Finally, the paper demonstrates how non-classical modal logics such as IK, C S 4, CL, or Masiniʼs deontic system of 2-sequents arise as theories of CK, presented both as special rules and as frame classes.

Details DOI

I&C Journal 2010 Journal Article

Is observational congruence on μ -expressions axiomatisable in equational Horn logic?

Michael Mendler
Gerald Lüttgen

It is well known that bisimulation on μ -expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Ésik necessarily involve implicational rules. However, both systems rely on features beyond pure equational Horn logic: either rules that are impure by involving non-equational side-conditions, or rules that are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic. This paper presents a positive and a negative result regarding the axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner’s impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner’s unique fixed point rule and Bloom/Ésik’s GA rule are incomplete without the congruence rule, and neither system has a complete extension in rank-1 equational axioms. It remains open whether there are higher-rank equational axioms or other Horn rules which would render Milner’s or Bloom/Ésik’s axiomatisations complete.

Details DOI

CSL Conference 2001 Conference Paper

Categorical and Kripke Semantics for Constructive S4 Modal Logic

Natasha Alechina
Michael Mendler
Valeria de Paiva
Eike Ritter

Abstract We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the appropriate categorical models for these logics.

Details

I&C Journal 1997 Journal Article

Propositional Lax Logic

Matt Fairtlough
Michael Mendler

We investigate a peculiar intuitionistic modal logic, called Propositional Lax Logic (PLL), which has 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. As a modal logic it is special since it features a single modal operator ○ that has a flavour both of possibility and of necessity. In the paper we provide the motivation for PLL and present several technical results. We investigate some of its proof-theoretic properties, presenting a cut-elimination theorem for a standard Gentzen-style sequent presentation of the logic. We go on to define a new class of fallible two-frame Kripke models for PLL. These models are unusual since they feature worlds with inconsistent information; furthermore, the only frame condition imposed is that the ○-frame be a subrelation of the ⊃-frame. We give a natural translation of these models into Goldblatt's J -space models of PLL. Our completeness theorem for these models yields a Gödel-style embedding of PLL into a classical bimodal theory of type (S4, S4) and underpins a simple proof of the finite model property. We proceed to prove soundness and completeness of several theories for specialized classes of models. We conclude with a brief exploration of two concrete and rather natural types of model from hardware verification for which the modality ○ models correctness up to timing constraints. We obtain decidability of ○-free fragment of the logic of the first type of model, which coincides with the stable form of Maksimova's intermediate logicLΠ.

Details DOI

CSL Conference 1995 Conference Paper

An Intuitionistic Modal Logic with Applications to the Formal Verification of Hardware

Matt Fairtlough
Michael Mendler

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.

Details