Timed CTL model checking in Real-Time Maude

DOI10.1007/978-3-642-34005-5_10MaRDI QIDQ3164837zbMATH OpenOpenAlexFDO

Authors Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky

Publication date 16 October 2012

Published in Rewriting Logic and Its Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-34005-5_10

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model-checking in dense real-time
• Model Checking Real-Time Systems
• Symbolic model checking for real-time systems
• scientific article; zbMATH DE number 1439078
• Model-checking timed temporal logics

Cited in

(11)

• Twenty years of rewriting logic
• Verifying hierarchical Ptolemy II discrete-event models using real-time maude
• Abstraction and completeness for real-time Maude
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• An algebraic specification for CTL with time constraints
• Extending CTL with Actions and Real Time
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Model Checking Timed Systems with Urgencies
• Strategies, Model Checking and Branching-Time Properties in Maude
• Semantics and pragmatics of real-time maude
• Model checking MASL specification of distributed real-time systems

Describes a project that uses

Uses Software

• Romeo
• Kronos
• Uppaal
• Maude
• Ptolemy
• MOMENT2
• TSMV
• AADL

This page was built for publication: Timed CTL model checking in Real-Time Maude

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3164837)