Compositional Abstraction in Real-Time Model Checking

DOI10.1007/978-3-540-85778-5_17MaRDI QIDQ3543301zbMATH OpenOpenAlexFDO

Authors Jasper Berendsen, F. Vaandrager

Publication date 2 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85778-5_17

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1696495
• Model-checking for real-time systems
• Verifying abstractions of timed systems
• Abstraction and abstraction refinement
• Compositional abstraction for stochastic systems

Cites work

• A process algebra with distributed priorities
• A theory of normed simulations
• Compositional Abstraction in Real-Time Model Checking
• CONCUR 2005 – Concurrency Theory
• Formal Methods for the Design of Real-Time Systems
• Forward and backward simulations. I. Untimed Systems
• Foundations of a Compositional Interchange Format for Hybrid Systems
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 1696495 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1863171 (Why is no real title available?)
• Process algebra with guards: Combining hoare logic with process algebra
• The existence of refinement mappings
• The Spotlight Principle
• The Theory of Timed I/O Automata
• Turning SOS rules into equations

Cited in

(10)

• Event algebra for transition systems composition application to timed automata
• scientific article; zbMATH DE number 1696495 (Why is no real title available?)
• Predicate abstraction for dense real-time systems
• Methodologies for specification of real-time systems using timed I/O automata
• On Expressiveness and Complexity in Real-Time Model Checking
• Compositional Abstraction in Real-Time Model Checking
• Compositional abstraction for stochastic systems
• On implementable timed automata
• Spotlight abstraction in model checking real-time task schedulability
• The axiomatization of override and update

Describes a project that uses

Uses Software

• Uppaal

This page was built for publication: Compositional Abstraction in Real-Time Model Checking

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