Modal, temporal, and hybrid expressivity

Go to home page

Finite H-dimension does not imply expressive completeness

Ian Hodkinson
J. Philosophical Logic 23 (1994) 535-573.
A conjecture of Gabbay (1981) states that any class of flows of time having the property known as finite H-dimension admits a finite set of expressively complete one-dimensional temporal connectives. Here we show that the class of `circular' structures refutes the generalisation of this conjecture to Kripke frames. We then construct from this class, by a general method, a new class of irreflexive transitive flows of time that refutes the original conjecture.

Our paper includes full descriptions of a method for establishing finite H-dimension for a class of structures and of the technique for extending finite H-dimension to other classes, and an introduction surveying the area of expressive completeness.

The k-variable property is stronger than H-dimension k

I. Hodkinson and A Simon
J. Philosophical Logic 26 (1997) 81--101.
We study the notion of H-dimension and the formally stronger k-variable property, as considered by Gabbay and Immerman & Kozen. We exhibit a class of flows of time that has H-dimension 3, and admits a finite expressively complete set of one-dimensional connectives, but does not have the k-variable property for any finite k.

Expressive completeness of Until and Since over dedekind complete linear time

I. M. Hodkinson
In: Modal logic and process algebra, ed. A. Ponse, M. de Rijke, Y. Venema, CSLI Lecture Notes 53, 1995, ISBN 1-881526-95-X, pp. 171-185.
We prove the theorem of Kamp that the temporal connectives Until and Since are expressively complete over the class of all dedekind complete flows of time. We use an argument of Gabbay, Pnueli, Shelah, and Stavi, but presented in terms of games.

Temporal expressive completeness in the presence of gaps

D. M. Gabbay, I. M. Hodkinson, M. A. Reynolds
In: Logic Colloquium 90, ed. J. Oikkonen, J. Väänänen, Springer Lecture Notes in Logic 2, 1993, ISBN 3-540-57094-2, pp. 89-121.
It is known that the temporal connectives Until and Since are expressively complete for Dedekind Complete flows of time but that the Stavi connectives are needed to achieve expressive completeness for general linear time which may have 'gaps' in it. We present a full proof of this result.
We introduce some new unary connectives which, along with Until and Since are expressively complete for general linear time. We axiomatize the new connectives over general linear time, define a notion of complexity on gaps and show that Until and Since are themselves expressively complete for flows of time with only isolated gaps. We also introduce new unary connectives which are less expressive than the Stavi connectives but are, nevertheless, expressively complete for flows of time whose gaps are of only certain restricted types. In this connection we briefly discuss scattered flows of time.

Notes on games in temporal logic

Ian Hodkinson
Lecture notes for LUATCS meting, Johannesburg, Dec 1999.  13 pages.
We prove a positive and a negative expressive completeness result, both due to J.A.W. (Hans) Kamp. We use games to simplify the proofs.
  1. Propositional temporal logic with Until and Since is expressively complete over Dedekind-complete linear time.  The proof simplifies the one in Modal Logic and Process Algebra above, by using ideas of Wilke.
  2. Predicate (first-order) temporal logic with Until and Since is not expressively complete over the real order.  However, a positive result is proved for `simple' formulas -- taken from the paper with Wolter and Zakharyaschev here.

Separation - past, present, and future

Ian Hodkinson and Mark Reynolds
Chapter in We will show them! (Essays in honour of Dov Gabbay on his 60th birthday), volume 2
S. Artemov, H. Barringer, A. d'Avila Garcez, L. Lamb, J. Woods, eds.
College Publications, 2005, ISBN 1-904987-12-5.  Pages 117-142.
We discuss the original application of separation in temporal logic, some more recent activity on it, and some open problems about it.

The paper contains an incorrect reference, which should read: Jonker, C.M., Treur, J., and Wijngaards, W.C.A., A Temporal Modelling Environment for Internally Grounded Beliefs, Desires and Intentions, Cognitive Systems Research Journal, vol. 4(3), 2003, pp. 191-210.

A bisimulation characterization theorem for hybrid logic with the current-state binder

Ian Hodkinson and Hicham Tahiri
Review of Symbolic Logic 3 (2010) 247-261.
doi:10.1017/S1755020309990426, published online by Cambridge University Press 26 Feb 2010.  Copyright Cambridge University Press
We prove that every first-order formula that is invariant under quasi-injective bisimulations is equivalent to a formula of hybrid logic with the downarrow operator.  Our proof uses a variation of the usual unravelling technique.  We also briefly survey related results, and show in a standard way that it is undecidable whether a first-order formula is invariant under quasi-injective bisimulations.

Bounded fragment and hybrid logic with polyadic modalities

Ian Hodkinson
Review of Symbolic Logic 3 (2010) 279-286
doi:10.1017/S1755020309990402, published online by Cambridge University Press 22 Mar 2010.  Copyright Cambridge University Press
We show that the bounded fragment of first order logic and the hybrid language with 'downarrow' and 'at' operators are equally expressive even with polyadic modalities, but that their 'positive' fragments are equally expressive only for unary modalities.