Date
2024-04-09Metadata
Show full item record
Aufsatz
Model checking timed recursive CTL
Abstract
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.
Sponsorship
Gefördert im Rahmen des Projekts DEALCitation
@article{doi:10.17170/kobra-2024080710640,
author={Bruse, Florian and Lange, Martin},
title={Model checking timed recursive CTL},
journal={Information and Computation},
year={2024}
}
0500 Oax
0501 Text $btxt$2rdacontent
0502 Computermedien $bc$2rdacarrier
1100 2024$n2024
1500 1/eng
2050 ##0##http://hdl.handle.net/123456789/15958
3000 Bruse, Florian
3010 Lange, Martin
4000 Model checking timed recursive CTL / Bruse, Florian
4030
4060 Online-Ressource
4085 ##0##=u http://nbn-resolving.de/http://hdl.handle.net/123456789/15958=x R
4204 \$dAufsatz
4170
5550 {{Zeitbehafteter Automat}}
5550 {{Model Checking}}
7136 ##0##http://hdl.handle.net/123456789/15958
<resource xsi:schemaLocation="http://datacite.org/schema/kernel-2.2 http://schema.datacite.org/meta/kernel-2.2/metadata.xsd"> 2024-08-07T08:16:20Z 2024-08-07T08:16:20Z 2024-04-09 doi:10.17170/kobra-2024080710640 http://hdl.handle.net/123456789/15958 Gefördert im Rahmen des Projekts DEAL eng Namensnennung-Nicht-kommerziell 4.0 International http://creativecommons.org/licenses/by-nc/4.0/ Timed automata Model checking 004 Model checking timed recursive CTL Aufsatz 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. open access Bruse, Florian Lange, Martin 18 Seiten doi:10.1016/j.ic.2024.105168 Zeitbehafteter Automat Model Checking publishedVersion eissn:1090-2651 Issue June Information and Computation Volume 298 false 105168 </resource>
The following license files are associated with this item:
Except where otherwise noted, this item's license is described as Namensnennung-Nicht-kommerziell 4.0 International