Positive and negative results on the
decidability of the model-checking problem for an epistemic extension
of Timed CTL

We present TCTLK, a continuous-time variant of the Computational Tree Logic with knowledge operators, generalizing both TCTL, the continuous-time variant of CTL, and CTLK, the epistemic generalization of CTL. Formulas are interpreted over timed automata, with a synchronous and perfect recall semantics, and the observability relation requires one to specify what clocks are visible for an agent.

We show that, in general, the model-checking problem for TCTLK is undecidable, even if formulas do not use any clocks – and hence CTLK has an undecidable model-checking problem when interpreted over timed automata. On the other hand, we show that, when each agent can see all clock values, model-checking becomes decidable.

*To appear in "Proceedings of the 16th
International Symposium on Temporal Representation and Reasoning
(TIME 2009)", Bressanone-Brixen, Italy, 23-25 July 2009,
Springer Verlag, Lecture Notes in Computer Science.*

gzipped postscript file.

*See also the Technical
Report, LACL, 2009.*