Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall

摘要

We show that CTL with knowledge modalities but without common knowledge has an undecidable satisfiability problem in the synchronous perfect recall semantics. We also present an adaptation of the classical model-checking algorithm for CTL that handles knowledge operators.