dCTL: a branching time temporal logic for fault-tolerant system verification

DOI10.1007/978-3-642-24690-6_9zbMATH Open1350.68181OpenAlexW26992193MaRDI QIDQ3095236FDOQ3095236

Authors: Pablo F. Castro, Cecilia Kilmurray, Araceli Acosta, Nazareno Aguirre 

Publication date: 28 October 2011

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24690-6_9

Recommendations

• Model checking propositional deontic temporal logic via a \(\mu \)-calculus characterization
• Synthesizing masking fault-tolerant systems from deontic specifications
• A Temporal Logic of Robustness
• Formally verifying fault tolerant system designs
• Reasoning about System-Degradation and Fault-Recovery with Deontic Logic

zbMATH Keywords

model checkingfault toleranceformal methodstemporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• Deontic action logic, atomic Boolean algebras and fault-tolerance
• A Temporal Logic of Robustness
• Logical specification and analysis of fault tolerant systems through partial model checking

Cited In (5)

• Expressiveness and succinctness of a logic of robustness
• Model checking propositional deontic temporal logic via a \(\mu \)-calculus characterization
• Simulation relations for fault-tolerance
• Reasoning about System-Degradation and Fault-Recovery with Deontic Logic
• Synthesizing masking fault-tolerant systems from deontic specifications

This page was built for publication: dCTL: a branching time temporal logic for fault-tolerant system verification

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