Paper Details

Reducing Model Checking from Multi-Valued CTL* to CTL*
B. Konikowska and W. Penczek

A multi-valued version of CTL* (mv-CTL*), where both the propositions and the accessibility relation are multi-valued taking values in a finite quasi-Boolean algebra, is considered. A general translation from mv-CTL* to CTL* model checking is defined. An application of the translation is shown for the most commonly used quasi-Boolean algebras.