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

DOI10.1007/978-3-642-24690-6_9MaRDI QIDQ3095236zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

model checkingfault toleranceformal methodstemporal logic

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Temporal Logic of Robustness
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deontic action logic, atomic Boolean algebras and fault-tolerance
• Logical specification and analysis of fault tolerant systems through partial model checking
• “Sometimes” and “not never” revisited

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)