Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations

DOI10.1145/2532440MaRDI QIDQ5169969zbMATH OpenOpenAlexFDO

Authors Cindy Eisner, Dana Fisman, John W. Havlicek

Publication date 17 July 2014

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2532440

zbMATH Keywords

topologytemporal logicregular expressionssafetylivenessSVAPSL

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A lattice-theoretic characterization of safety and liveness
• The coarsest precongruences respecting safety and liveness properties
• Safety and liveness from a methodological point of view
• scientific article; zbMATH DE number 1759635
• Safety, domain independence and generalized quantification
• A topological characterization of weakness
• Computer Science Logic
• Safety, domination, and differential support
• Quantitative safety and liveness

Cites work

• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 3479763 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1956573 (Why is no real title available?)
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• A lattice-theoretic characterization of safety and liveness
• A topological characterization of weakness
• Computer Science Logic
• Defining liveness
• Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness
• Looping vs. repeating in dynamic logic
• Reasoning about infinite computations
• Reasoning with temporal logic on truncated paths.
• Recognizing safety and liveness
• Safety, liveness and fairness in temporal logic
• Some Complexity Results for SystemVerilog Assertions
• Temporal logic can be more expressive
• The temporal semantics of concurrent programs

Cited in

(2)

• A topological characterization of weakness
• Functional specification of hardware via temporal logic

This page was built for publication: Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations

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