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.