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

Issue title: Concurrency Specification and Programming (CS&P 2003)

Article type: Research Article

Authors: Konikowka, Beata | Penczek, Wojciech

Affiliations: Institute of Computer Science, PAS, 01-237 Warsaw, ul. Ordona 21, Poland

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.

Journal: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 211-224, 2004