On Designated Values in Multi-valued CTL^* Model Checking

Abstract

A multi-valued version of CTL^* (mv-CTL^*), where both the propositions and the accessibility relation are multi-valued, taking values in a complete lattice with a complement, is considered. Contrary to all the existing model checking results for multi-valued modal logics, our lattices are not required to be finite. A set of restrictions is provided under which there is a direct translation from mv-CTL^* to CTL^* model checking problem for designated values. Bisimulation induced by mv-CTL^* is characterized.