The true bisimulations for 'since' and 'until'

Holger Sturm



The aim of this paper is to establish a new notion of equivalence between temporal models, so-called S-similarity, as the appropriate notion of bisimilarity for temporal logic with Since and Until. The main technical results of the paper provide semantical characterizations of the first-order formulas that are equivalent to a temporal formula: Theorem 3.7 concerns the equivalence of temporal and first-order formulas with respect to pointed temporal models, whereas Theorem 4.4 takes the level of temporal models into account.

Full Text:



van Benthem, J.F.A.K., and J. Bergstra: “Logic of transition systems”, Journal of Logic, Language and Information 3 (1995), 247–283.

Chang, C.C., and H.J. Keisler: Model Theory. North-Holland, Amsterdam 1990.

Kurtonina, N., and M. de Rijke: “Bisimulations for temporal logic”, Journal of Logic, Language and Information 6 (1997), 403–425.

de Rijke, M., and H. Sturm: “Global definability in basic modal logic”, in H. Wansing, Essays on Non-classical Logic, World Scientific, London/Singapore 2001, 111–133.

Sturm, H.: Modale Fragmente von Lωω und Lω1ω, PhD thesis, University of Munich, CIS, Munich 1997.

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism