On Designated Values in Multi-valued CTL^* Model Checking
Beata Konikowka, Wojciech Penczek · Fundamenta Informaticae · 2003
A multi-valued version of CTL^a (mv-CTL^a), 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^a to CTL^a model checking problem for designated values. Bisimulation induced by mv-CTL^a is characterized.