Symbolic branching bisimulation-checking of dense-time systems in an environment
Journal
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Journal Volume
5469
Pages
485-489
Date Issued
2009
Author(s)
Abstract
We present timed branching bisimulation in an environment which allows us to design a new bisimulation-checking algorithm with enhanced performance by reducing state spaces with shared environment state information between the model and the specification automatas. We also propose non-Zeno bisimulation in an environment that fully characterizes TCTL formulas. We then report our implementation and experiments with the ideas.
We present timed branching bisimulation in an environment which allows us to design a new bisimulation-checking algorithm with enhanced performance by reducing state spaces with shared environment state information between the model and the specification automatas. We also propose non-Zeno bisimulation in an environment that fully characterizes TCTL formulas. We then report our implementation and experiments with the ideas.
Type
conference paper