Tableau-based Bisimulation Invariance Testing

Perkov, Tin

Journal

Reports on Mathematical Logic

2013 | 48 |

Article title

Tableau-based Bisimulation Invariance Testing

Authors

Tin Perkov

Content

Full texts:

Download

Title variants

Languages of publication

PL

Abstracts

PL

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.

Keywords

PL

Publisher

[unknown2]

Journal

Reports on Mathematical Logic

Year

2013

Volume

48

Physical description

Dates

published

2013

online

07 - 07 - 2015

Contributors

author

Tin Perkov

References

Document Type

Publication order reference

Identifiers

YADDA identifier

bwmeta1.element.ojs-issn-2084-2589-year-2013-volume-48-article-2910