DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

DOI10.1007/978-3-540-69850-0_12zbMath1142.68431OpenAlexW1501731334MaRDI QIDQ3512441

E. Allen Emerson, Edmund M. Clarke

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

program specificationconcurrent programstemporal logictableau-based decision procedurefinite modelpropositional branching time logicsynchronisation skeleton

Mathematics Subject Classification ID

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

Related Items (7)

On first-order runtime enforcement of branching-time properties ⋮ Operational causality -- necessarily sufficient and sufficiently necessary ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ Unnamed Item ⋮ A tableau calculus for first-order branching time logic ⋮ An efficient approach for abstraction-refinement in model checking ⋮ Exogenous Probabilistic Computation Tree Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• A lattice-theoretical fixpoint theorem and its applications
• The Total Correctness of Parallel Programs
• Depth-First Search and Linear Graph Algorithms

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