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

temporal logicspecification languagetimed transition systems

Mathematics Subject Classification ID

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

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

(32)

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

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)