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)
03B45: Modal logic (including the logic of norms)
68Q60: Specification and verification (program logics, model checking, etc.)
68N99: Theory of software
Related Items
Verification of Linear Duration Invariants by Model Checking CTL Properties, Towards a denotational semantics of timed RSL using duration calculus, An intuitive formal proof for deadline driven scheduler, A real-time interval logic and its decision procedure, A first order logic for specification of timed algorithms: Basic properties and a decidable class, On the completeness and decidability of duration calculus with iteration, 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, Axiomatisation and decidability of multi-dimensional Duration Calculus, Algebraic neighbourhood logic, Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography, Robust safety of timed automata, Non-elementary lower bound for Propositional Duration Calculus, Design for delay verifiability, Decidability of mean value calculus, Models for reactivity, Extending Hoare logic to real-time, Model-checking discrete duration calculus, Duration calculus: Logical foundations, Completeness of the accumulation calculus, Induction in the timed interval calculus, Automata over continuous time, Completeness of temporal logics over infinite intervals., Verification of duration systems using an approximation approach, Specification and verification of multimedia synchronization in duration calculus, Checking temporal duration properties of timed automata., Star free expressions over the reals, 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, Efficient verification of a class of time Petri nets using linear programming, Process algebra for hybrid systems, Real-time refinement in Manna and Pnueli's temporal logic, 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, Verification of schedulability for real-time programs, A theory of Orwellian specifications with NewThink, Compositional verification of real-time systems with explicit clock temporal logic, A wide-spectrum language for object-based development of real-time systems, A decision procedure for propositional projection temporal logic with infinite models, A general tableau method for propositional interval temporal logics: theory and implementation, Slicing techniques for verification re-use, Verification of cooperating traffic agents, Complexity of propositional projection temporal logic with star, Timing in music and modal temporal logic
Cites Work
