Timed Recursive CTL

We study the complexity of the model-checking problem of, TRecCTL. This logic is obtained as the merger of two extensions of CTL, Timed CTL and Temporal Logic with Recursion. The former extends CTL by operators to talk about timed aspects of systems defined by timed automata. The latter adds a recursion operator to CTL, greatly increasing the expressive power of the resulting logic. We obtain that the model-checking problem for TRecCTL is 2EXPTIME complete. Moreover, the model-checking problem for the so-called tail-recursive fragment of TRecCTL, obtained by limiting the way recursion is used, is EXPSPACE complete. Notably, the former problem is already 2EXPTIME hard in its expression complexity, and the latter is already EXPSPACE complete in its data complexity. Moreover, the hardness result already holds for timed automata with one clock only. For Timed CTL, the amount of clocks present is important. Contributed talk given by Florian Bruse Lunch Friday 14h00 - 14h48, Contributed Talks Model Theory & Logic | HS 3 | chair: Ramanathan Thinniyam Srinivasan Applications and Other Topics | HS 4 | chair: Supratik Chakraborty Model Theory & Logic | HS 3 | chair: Ramanathan Thinniyam Srinivasan Applications and Other Topics | HS 4 | chair: Supratik Chakraborty

Authors

• Florian Bruse

Keywords

No keywords are indexed for this paper.