Tableau-based Bisimulation Invariance Testing

Tin Perkov

Titles

Abstract

A tableau procedure that tests bisimulation invariance of a given first-order formula, and therefore tests if that formula is equivalent to the standard translation of some modal formula, is presented. The test is sound and complete: a given formula is bisimulation invariant if and only if there is a closed tableau for that formula. The test generally does not terminate, but it does if a given formula is bisimulation invariant, i.e., the test is positive.

References

[1] J. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Cambridge University Press, 2001.

[2] G. Boolos, Trees and Finite Satisﬁability: Proof of a Conjecture of Burgess, Notre Dame Journal of Formal Logic 25 (1984), pp. 193–197.

[3] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic, Springer-Verlag, 1984.

[4] R. Jeﬀrey, J. P. Burgess, Formal Logic: Its Scope and Limits, Hackett, 2006.

[5] R. M. Smullyan, First-Order Logic, Springer-Verlag, 1968.

[6] J. van Benthem, Exploring Logical Dynamics, Studies in Logic, Language and Information, CSLI Publications & FoLLI, Stanford, 1996.

Information

Information: Reports on Mathematical Logic, 2013, Number 48, pp. 101 - 115

DOI: https://doi.org/10.4467/20842589RM.13.005.1257

Article type: Original article

Titles:

Polish:

Tableau-based Bisimulation Invariance Testing

English:

Tableau-based Bisimulation Invariance Testing

Authors

Tin Perkov

Polytechnic of Zagreb Avenija V. Holjevca 15 10000 Zagreb, Croatia

Published at: 26.11.2013

Article status: Open

Licence: None

Percentage share of authors:

Tin Perkov (Author) - 100%

Article corrections:

-

Publication languages:

English

View count: 2026

Number of downloads: 1041

<p> Tableau-based Bisimulation Invariance Testing</p>

Pobierz pełny tekst

Titles

Abstract

References

Information

Authors