A calculus of durations
From MaRDI portal
Publication:1183485
DOI10.1016/0020-0190(91)90122-XzbMath0743.68097MaRDI QIDQ1183485
Chaochen Zhou, C. A. R. Hoare, Anders P. Ravn
Publication date: 28 June 1992
Published in: Information Processing Letters (Search for Journal in Brave)
Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)
Related Items (only showing first 100 items - show all)
Verification of cooperating traffic agents ⋮ No Need Knowing Numerous Neighbours ⋮ Safe and Optimal Adaptive Cruise Control ⋮ A duration calculus with neighborhood modalities ⋮ Extending Hoare logic to real-time ⋮ Model-checking discrete duration calculus ⋮ A duration calculus with infinite intervals ⋮ Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude ⋮ An Abstract Model for Proving Safety of Autonomous Urban Traffic ⋮ Checking Integral Real-Time Automata for Extended Linear Duration Invariants ⋮ Undecidability of the Logic of Overlap Relation over Discrete Linear Orderings ⋮ Verification of schedulability for real-time programs ⋮ A theory of Orwellian specifications with NewThink ⋮ Recent advances in program verification through computer algebra ⋮ Axiomatisation and decidability of multi-dimensional Duration Calculus ⋮ An application of temporal projection to interleaving concurrency ⋮ Duration calculus: Logical foundations ⋮ Compositional verification of real-time systems with explicit clock temporal logic ⋮ Exploring an Interface Model for CKA ⋮ Completeness of the accumulation calculus ⋮ Non-elementary lower bound for Propositional Duration Calculus ⋮ Specification and optimal reactive synthesis of run-time enforcement shields ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ A generic logical-temporal performance analysis method for complex systems ⋮ Induction in the timed interval calculus ⋮ Automata over continuous time ⋮ HRELTL: a temporal logic for hybrid systems ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Mathematical analysis of stage-based programmable logic controller ⋮ Towards a UTP Semantics for Modelica ⋮ Completeness of temporal logics over infinite intervals. ⋮ A wide-spectrum language for object-based development of real-time systems ⋮ Verification of duration systems using an approximation approach ⋮ Specification and verification of multimedia synchronization in duration calculus ⋮ Algebraic neighbourhood logic ⋮ A novel algorithm for intrusion detection based on RASL model checking ⋮ Checking temporal duration properties of timed automata. ⋮ An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic ⋮ Interval logics and their decision procedures. II: A real-time interval logic ⋮ The algorithmic analysis of hybrid systems ⋮ Finite divergence ⋮ Metric temporal logic with durations ⋮ Sequential calculus ⋮ Hybrid automata with finite bisimulations ⋮ Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography ⋮ Verification and enforcement of access control policies ⋮ Incremental methods for checking real-time consistency ⋮ Assessing component impairing at mission level ⋮ Guest editors' preface to special issue on interval temporal logics ⋮ The dark side of interval temporal logic: marking the undecidability border ⋮ Compositional reasoning using intervals and time reversal ⋮ A practical approach to model checking duration calculus using Presburger arithmetic ⋮ Hybrid Metric Propositional Neighborhood Logics with Interval Length Binders ⋮ A decision procedure for propositional projection temporal logic with infinite models ⋮ A process algebraic framework for specification and validation of real-time systems ⋮ Reachability results for timed automata with unbounded data structures ⋮ On the completeness and decidability of duration calculus with iteration ⋮ A timeband framework for modelling real-time systems ⋮ Process algebra for hybrid systems ⋮ Rate monotonic scheduling re-analysed ⋮ An abstract model for proving safety of autonomous urban traffic ⋮ Connection between logical and algebraic approaches to concurrent systems ⋮ A general tableau method for propositional interval temporal logics: theory and implementation ⋮ BDI-modelling of complex intracellular dynamics ⋮ Complexity of propositional projection temporal logic with star ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ A Modular Static Analysis Approach to Affine Loop Invariants Detection ⋮ Timing in music and modal temporal logic ⋮ Real-time refinement in Manna and Pnueli's temporal logic ⋮ A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time ⋮ PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic ⋮ A Relatively Complete Axiomatisation of Projection onto State in the Duration Calculus ⋮ Logical Interpolation and Projection onto State in the Duration Calculus ⋮ Robust safety of timed automata ⋮ Safe Runtime Verification of Real-Time Properties ⋮ Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata ⋮ A formal framework for modeling and validating simulink diagrams ⋮ Design for delay verifiability ⋮ Decidability of mean value calculus ⋮ Star free expressions over the reals ⋮ Prefix and Projection onto State in Duration Calculus ⋮ Interval Duration Logic ⋮ Proving Safety of Traffic Manoeuvres on Country Roads ⋮ Slicing techniques for verification re-use ⋮ Refinement of time ⋮ Deductive verification of real-time systems using STeP ⋮ PLC-automata: A new class of implementable real-time automata ⋮ Verification, refinement and scheduling of real-time programs ⋮ Decidable integration graphs. ⋮ Expressive completeness of duration calculus. ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Positive loop-closed automata: A decidable class of hybrid systems ⋮ Decidability of a Hybrid Duration Calculus ⋮ Efficient verification of a class of time Petri nets using linear programming ⋮ Automatic Verification of Combined Specifications: An Overview ⋮ On Verification of Linear Occurrence Properties of Real-Time Systems ⋮ Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools ⋮ Models for reactivity
Cites Work
This page was built for publication: A calculus of durations
