DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

DOI10.1007/978-3-540-69850-0_12MaRDI QIDQ3512441zbMATH OpenOpenAlexFDO

Authors Edmund Clarke, E. Allen Emerson

Publication date 15 July 2008

Published in 25 Years of Model Checking (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69850-0_12

zbMATH Keywords

temporal logicprogram specificationconcurrent programstableau-based decision procedurefinite modelpropositional branching time logicsynchronisation skeleton

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 3870578
• scientific article; zbMATH DE number 4060695
• Synthesis of communicating process skeletons from temporal-spatial logic specifications
• scientific article; zbMATH DE number 47403
• Theoretical Computer Science

Cites work

• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 3729438 (Why is no real title available?)
• scientific article; zbMATH DE number 3767031 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3325547 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Depth-First Search and Linear Graph Algorithms
• The Total Correctness of Parallel Programs
• The temporal logic of branching time

Cited in

(14)

• An efficient approach for abstraction-refinement in model checking
• A tableau calculus for first-order branching time logic
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• On runtime enforcement via suppressions
• Explaining Hyperproperty Violations
• Complete abstractions and subclassical modal logics
• Operational causality -- necessarily sufficient and sufficiently necessary
• A complete fragment of LTL(EB)
• Implement of synchronization of concurrent objects
• On first-order runtime enforcement of branching-time properties
• scientific article; zbMATH DE number 2213335 (Why is no real title available?)
• scientific article; zbMATH DE number 1864594 (Why is no real title available?)
• Exogenous probabilistic computation tree logic
• Synthesizing synchronous systems by static scheduling in space-time

This page was built for publication: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

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