Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment

DOI10.1007/978-3-642-00602-9_40MaRDI QIDQ3624601zbMATH OpenOpenAlexFDO

Authors Farn Wang

Publication date 30 April 2009

Published in Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00602-9_40

zbMATH Keywords

algorithmstimed automataexperimentsmodel-checkingbranching bisimulationTCTL

Mathematics Subject Classification ID

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

Recommendations

• Symbolic Simulation-Checking of Dense-Time Automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Symbolic verification and analysis of discrete timed systems
• Efficient scaling-invariant checking of timed bisimulation
• Branching time and abstraction in bisimulation semantics
• Symbolic model checking for real-time systems
• Bisimulation minimization and symbolic model checking
• An efficient fully symbolic bisimulation algorithm for non-deterministic systems
• scientific article; zbMATH DE number 1324667

Cites work

• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• CONCUR 2005 – Concurrency Theory
• Characterizing finite Kripke structures in propositional temporal logic
• Kronos: A verification tool for real-time systems
• Symbolic Simulation-Checking of Dense-Time Automata

Cited in

(3)

• Equivalence checking 40 years after: a review of bisimulation tools
• Symbolic Simulation-Checking of Dense-Time Automata
• Efficient scaling-invariant checking of timed bisimulation

Describes a project that uses

Uses Software

• Kronos

This page was built for publication: Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment

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