Tableau-based Bisimulation Invariance Testing
Tableau-based Bisimulation Invariance Testing

Summary/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.

• Details
• Contents