Compositional reasoning using intervals and time reversal
From MaRDI portal
Publication:2251129
DOI10.1007/s10472-013-9356-8zbMath1378.03017MaRDI QIDQ2251129
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
symmetry; time reversal; mutual exclusion; interval temporal logic; compositional reasoning; formal~verification; Peterson's~algorithm
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
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