Bisimulation and p-morphism for branching-time logics with indistinguishability relations

TL;DR

This paper introduces bisimulation and p-morphism concepts for branching-time logics with indistinguishability relations, providing preservation results that enhance the understanding of their semantic properties.

Contribution

It defines new notions of bisimulation and p-morphism tailored for branching-time logics with indistinguishability, along with related preservation theorems.

Findings

Established bisimulation and p-morphism definitions for the logic.

Proved preservation results for these notions.

Enhanced semantic understanding of branching-time logics with indistinguishability.

Abstract

In Zanardo, 1998, the Peircean semantics for branching-time logics is enriched with a notion of indistinguishability at a moment t between histories passing through t. Trees with indistinguishability relations provide a semantics for a temporal language with tense and modal operators. In this paper a notion of p-morphism and a notion of bisimulation, wrt this language and semantics, are given and a number of preservation results are proven.