Model Checking Games for a Fair Branching-Time Temporal Epistemic Logic

Model checking games are instances of Hintikka’s game semantics for logic used for purposes of debugging systems verification models. Previous work in the area has developed these games for branching time logic. The paper develops an extension to a logic that adds epistemic operators, and interprets the branching time operators with respect to fairness constraints. The implementation of the extended games in the epistemic model checker MCK is described.

• Type: Conference
• Year: 2009
• Where: AUSAI
• Authors: Xiaowei Huang, Ron van der Meyden
• Keywords: Artificial Intelligence, AUSAI 2009, Branching Time, Branching Time Operators, Model Checking Games