Model checking timed recursive CTL

dc.date.accessioned	2024-08-07T08:16:20Z
dc.date.available	2024-08-07T08:16:20Z
dc.date.issued	2024-04-09
dc.identifier	doi:10.17170/kobra-2024080710640
dc.identifier.uri	http://hdl.handle.net/123456789/15958
dc.description.sponsorship	Gefördert im Rahmen des Projekts DEAL
dc.language.iso	eng
dc.rights	Namensnennung-Nicht-kommerziell 4.0 International	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc/4.0/	*
dc.subject	Timed automata	eng
dc.subject	Model checking	eng
dc.subject.ddc	004
dc.title	Model checking timed recursive CTL	eng
dc.type	Aufsatz
dcterms.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.	eng
dcterms.accessRights	open access
dcterms.creator	Bruse, Florian
dcterms.creator	Lange, Martin
dcterms.extent	18 Seiten
dc.relation.doi	doi:10.1016/j.ic.2024.105168
dc.subject.swd	Zeitbehafteter Automat	ger
dc.subject.swd	Model Checking	eng
dc.type.version	publishedVersion
dcterms.source.identifier	eissn:1090-2651
dcterms.source.issue	Issue June
dcterms.source.journal	Information and Computation	eng
dcterms.source.volume	Volume 298
kup.iskup	false
dcterms.source.articlenumber	105168

Except where otherwise noted, this item's license is described as Namensnennung-Nicht-kommerziell 4.0 International