Model checking for multivalued logic of knowledge and time
Beata Konikowska, Wojciech Penczek · 2006
We present a multivalued μK-calculus, an expressive logic to specify knowledge and time in multi-agent systems. We show that the general method of translation [22] from multivalued to two-valued De Morgan algebras can be extended to mv μK-calculus model checking. This way can we reduce the model checking problem for mv μK-calculus to several instances of the model checking problem for two-valued μK-calculus. As a result, properties involving mv μK-calculus or its subsets, like mv CTLK or mv CTL*K, can be verified using any of the available model checking algorithms. Three simple examples are shown to exemplify possible applications of multivalued logics of knowledge and time.