Treffer: Model Checking Timed Recursive CTL
Title:
Model Checking Timed Recursive CTL
Authors:
Contributors:
Florian Bruse and Martin Lange
Publisher Information:
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Publication Year:
2021
Collection:
DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics )
Subject Terms:
Document Type:
Fachzeitschrift
article in journal/newspaper<br />conference object
File Description:
application/pdf
Language:
English
Relation:
Is Part Of LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.12
DOI:
10.4230/LIPIcs.TIME.2021.12
Availability:
Accession Number:
edsbas.122D4F44
Database:
BASE
Weitere Informationen
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.