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

DOI10.1007/978-3-642-00602-9_40zbMATH Open1237.68127OpenAlexW1543600830MaRDI QIDQ3624601FDOQ3624601

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

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

zbMATH Keywords

algorithmstimed automataexperimentsmodel-checkingbranching bisimulationTCTL

Mathematics Subject Classification ID

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

Cites Work

• Kronos: A verification tool for real-time systems
• Characterizing finite Kripke structures in propositional temporal logic
• CONCUR 2005 – Concurrency Theory
• Title not available (Why is that?)
• 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

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)