Temporal proof methodologies for timed transition systems

DOI10.1006/INCO.1994.1060MaRDI QIDQ1333273zbMATH OpenOpenAlexFDO

Authors Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Publication date 12 October 1994

Published in Information and Computation (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://hdl.handle.net/1813/6096

zbMATH Keywords

specification languagetemporal logictimed transition systems

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Logic in artificial intelligence (68T27)

Recommendations

• Verification of clocked and hybrid systems
• Specification and compositional verification of real-time systems
• Deductive verification of real-time systems using STeP
• Factorizing proofs in timed CSP

Cited in

(36)

• Using mappings to prove timing properties
• Event-clock automata: a determinizable class of timed automata
• An embedding of timed transition systems in \(HOL\)
• Two-sorted metric temporal logics
• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Verification of reactive systems using temporal logic with clocks
• Verification of clocked and hybrid systems
• Deductive verification of real-time systems using STeP
• Verification, refinement and scheduling of real-time programs
• Proof assistance for real-time systems using an interactive theorem prover
• Unifying behavioral equivalences of timed transition systems
• Slime mould games based on rough set theory
• Categorical foundations for randomly timed automata
• Compositional verification of real-time systems with explicit clock temporal logic
• Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic
• A proof-based method for modelling timed systems
• Branching-Time Property Preservation Between Real-Time Systems
• Timed Temporal Logics for Abstracting Transient States
• scientific article; zbMATH DE number 52748 (Why is no real title available?)
• An equivalence theorem for the operational and temporal semantics of real-time, concurrent programs
• TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
• Dynamic networks of heterogeneous timed machines
• scientific article; zbMATH DE number 7566069 (Why is no real title available?)
• Verification in continuous time by discrete reasoning
• The Unmet Challenge of Timed Systems
• What good are digital clocks?
• Towards integrated verification of timed transition models
• Factorizing proofs in timed CSP
• Proving sequential function chart programs using timed automata
• Learning of event-recording automata
• On specifications and proofs of timed circuits
• Modular abstractions for verifying real-time distributed systems
• Semantic domains of timed event structures
• Automated compositional proofs for real-time systems
• Modeling and verification of real-time systems based on equations
• Automatic generation of path conditions for concurrent timed systems

This page was built for publication: Temporal proof methodologies for timed transition systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1333273)