DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

DOI10.1007/978-3-540-69850-0_12zbMATH Open1142.68431OpenAlexW1501731334MaRDI QIDQ3512441FDOQ3512441

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

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

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)

Cites Work

• Depth-First Search and Linear Graph Algorithms
• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The temporal logic of branching time
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Total Correctness of Parallel Programs

Cited In (14)

• An efficient approach for abstraction-refinement in model checking
• A tableau calculus for first-order branching time logic
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)