Compositional reasoning using intervals and time reversal

DOI10.1007/s10472-013-9356-8zbMath1378.03017MaRDI QIDQ2251129

Ben Moszkowski

Publication date: 11 July 2014

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-013-9356-8

zbMATH Keywords

symmetry; time reversal; mutual exclusion; interval temporal logic; compositional reasoning; formal~verification; Peterson's~algorithm

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

03B44: Temporal logic

Related Items

Reversibility of Executable Interval Temporal Logic Specifications, An application of temporal projection to interleaving concurrency

Uses Software

• SPIN
• KIV

Cites Work

• A cylinder computation model for many-core parallel computing
• A complete proof system for propositional projection temporal logic
• Proving linearizability with temporal logic
• Myths about the mutual exclusion problem
• Process logic: Expressiveness, decidability, completeness
• A calculus of durations
• Composition of assumption-commitment specifications in a UNITY style
• Duration calculus: Logical foundations
• Duration calculus. A formal approach to real-time systems.
• Interconnections between classes of sequentially compositional temporal formulas
• Framed temporal logic programming
• Temporal logic and state systems
• A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time
• An Introduction to Practical Formal Methods Using Temporal Logic
• Axiomatic semantics of projection temporal logic programs
• Regular Linear Temporal Logic
• A Brief Overview of PVS
• Interactive verification of concurrent systems using symbolic execution
• Temporal Logic Verification of Lock-Freedom
• A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
• PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic
• Regular Linear Temporal Logic with Past
• Tentative steps toward a development method for interfering programs
• Equations between Regular Terms and an Application to Process Logic
• Propositional temporal logics: decidability and completeness
• A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
• Reactive Systems
• Using Temporal Logic to Analyse Temporal Logic: A Hierarchical Approach Based on Intervals
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
• An axiomatic basis for computer programming
• Real-Time Systems
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item