Model checking epistemic extensions of CTL

June 22, 2009

Catalin Dima (LACL)

We show that CTL with knowledge modalities has an undecidable satisfiability problem, but decidable model-checking. We then show that, over continuous time, model-checking is undecidable, and becomes decidable only if the agents are able to fully observe clock values. We also give some ideas of the utility of CTL with knowledge operators in the verification of security properties.