Predicate abstraction for dense real-time systems

DOI10.1016/S1571-0661(04)80478-XMaRDI QIDQ2842588zbMATH OpenOpenAlexFDO

Authors M. Oliver Möller, Harald Rueß, Maria Sorea

Publication date 15 August 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)80478-x

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Predicate diagrams for the verification of real-time systems
• Predicate diagrams for the verification of real-time systems
• Compositional Abstraction in Real-Time Model Checking
• An abstraction technique for real-time verification
• Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise
• scientific article; zbMATH DE number 1231547
• On timed models and full abstraction
• Verifying abstractions of timed systems
• Modular abstractions for verifying real-time distributed systems

Cites work

• A theory of timed automata
• Analysis of timed systems using time-abstracting bisimulations
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1670793 (Why is no real title available?)
• scientific article; zbMATH DE number 1701753 (Why is no real title available?)
• scientific article; zbMATH DE number 2102725 (Why is no real title available?)
• scientific article; zbMATH DE number 898449 (Why is no real title available?)
• Predicate abstraction for dense real-time systems
• Results on the propositional \(\mu\)-calculus
• Symbolic model checking for real-time systems

Cited in

(10)

• Bounded model checking of max-plus linear systems via predicate abstractions
• Abstractions for hybrid systems
• Predicate diagrams for the verification of real-time systems
• Predicate abstraction for dense real-time systems
• Bounded model checking for timed automata
• Predicate diagrams for the verification of real-time systems
• Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise
• scientific article; zbMATH DE number 2080039 (Why is no real title available?)
• Predicate abstraction of rewrite theories
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

This page was built for publication: Predicate abstraction for dense real-time systems

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