Model checking timed recursive CTL

Simple item page
dc.date.accessioned2024-08-07T08:16:20Z
dc.date.available2024-08-07T08:16:20Z
dc.date.issued2024-04-09
dc.description.sponsorshipGefördert im Rahmen des Projekts DEAL
dc.identifierdoi:10.17170/kobra-2024080710640
dc.identifier.urihttp://hdl.handle.net/123456789/15958
dc.language.isoeng
dc.relation.doidoi:10.1016/j.ic.2024.105168
dc.rightsNamensnennung-Nicht-kommerziell 4.0 International*
dc.rights.urihttp://creativecommons.org/licenses/by-nc/4.0/*
dc.subjectTimed automataeng
dc.subjectModel checkingeng
dc.subject.ddc004
dc.subject.swdZeitbehafteter Automatger
dc.subject.swdModel Checkingeng
dc.titleModel checking timed recursive CTLeng
dc.typeAufsatz
dc.type.versionpublishedVersion
dcterms.abstractWe 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.accessRightsopen access
dcterms.creatorBruse, Florian
dcterms.creatorLange, Martin
dcterms.extent18 Seiten
dcterms.source.articlenumber105168
dcterms.source.identifiereissn:1090-2651
dcterms.source.issueIssue June
dcterms.source.journalInformation and Computationeng
dcterms.source.volumeVolume 298
kup.iskupfalse

Files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
1_s2.0_S0890540124000336_main.pdf
Size:
535.5 KB
Format:
Adobe Portable Document Format
Description:
Download

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
3.03 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Artikel