Timed automata provide a modeling formalism for time-critical properties of reactive systems with discrete-state/continuous-time behaviors. To handle the infinite state space of timed automata, recent verification tools use zone graphs, a symbolic semantic model that guarantees sound results, at least for properties reducible to reachability problems. If we instead want to compare the behavior of two timed automata, checking for timed trace equivalence is undecidable. Fortunately, timed bisimulation equivalence is decidable, but currently available checks do not provide useful explanations of the results. To overcome this limitation, we use a recently proposed extension of zone graphs by so-called virtual clocks. The extension not only facilitates effective tool support for timed bisimilarity checking but also enables the derivation of useful explanations from the results. If timed bisimilarity holds, all witnesses derivable from the composed symbolic representation of both models are indeed valid for both models. If timed bisimilarity does not hold, we describe how to obtain counterexamples, making explicit the behavioral differences. These witnesses/counterexamples may serve as test cases in later stages of system refinement.

翻译：时间自动机为具有离散状态/连续时间行为的反应式系统的时间关键属性提供了建模形式。为了处理时间自动机的无限状态空间，近年来的验证工具使用区域图（一种保证结果可靠性的符号语义模型，至少对于可归约为可达性问题的属性而言）。若需比较两个时间自动机的行为，检查时间迹等价性是不可判定的。幸运的是，时间互模拟等价性是可判定的，但现有检查方法无法提供结果的合理解释。为克服此局限，我们采用近期提出的区域图扩展——所谓虚拟时钟。该扩展不仅为时间互模拟等价性检查提供了有效工具支持，还能从结果中推导出有用的解释。若时间互模拟成立，从两个模型组合符号表示中导出的所有验证均对两个模型有效。若时间互模拟不成立，我们描述了如何获取反例以显式说明行为差异。这些验证/反例可在系统精化的后续阶段作为测试用例。