🇬🇧

Model checking timed recursive CTL

Bruse, Florian
Lange, Martin

We introduce Timed Recursive CTL, a merger of two extensions of the well-known branching-time logic CTL: Timed CTL is interpreted over real-time systems like timed automata; Recursive CTL introduces a powerful recursion operator which takes the expressiveness of this logic CTL well beyond that of regular properties. The result is an expressive logic for real-time properties. We show that its model checking problem is decidable over timed automata, namely 2-EXPTIME-complete.

Sponsor
Gefördert im Rahmen des Projekts DEAL
Citation
In: Information and Computation Volume 298 / Issue June (2024-04-09) , S. ; eissn:1090-2651
Collections
@article{doi:10.17170/kobra-2024080710640,
  author    ={Bruse, Florian and Lange, Martin},
  title    ={Model checking timed recursive CTL},
  keywords ={004 and Zeitbehafteter Automat and Model Checking},
  copyright  ={http://creativecommons.org/licenses/by-nc/4.0/},
  language ={en},
  journal  ={Information and Computation},
  year   ={2024-04-09}
}