Lars Luthmann, Hendrik Göttmann, Isabelle Bacher, and Malte Lochau

Timed automata (TA) are a well-established formalism for specifying discrete-state/continuous-time behavior of time-critical reactive systems. Concerning the fundamental analysis problem of comparing a candidate implementation against a specification, both given as TA, it has been shown that timed trace equivalence is undecidable, whereas timed bisimulation equivalence is decidable. The corresponding proof utilizes region graphs, a finite, but generally very space-consuming characterization of TA semantics. Hence, most practical TA tools utilize zone graphs instead, a symbolic and generally more efficient representation of TA semantics, to automate analysis tasks. However, zone graphs only produce sound results for analysis tasks being reducible to plain reachability problems thus being too imprecise for checking timed bisimilarity. In this paper, we propose bounded zone-history graphs, a novel characterization of TA semantics facilitating an adjustable trade-off between precision and scalability of timed-bisimilarity checking. Our tool TimBrCheck is, to the best of our knowledge, the only currently available tool for effectively checking timed bisimilarity and even supports non-deterministic TA with silent moves. We further present experimental results gained from applying our tool to a collection of community benchmarks, providing insights into trade-offs between precision and efficiency, depending on the bound value.

Download our tool and the case studies here: link (ZIP archive).
The archive contains the tool, the subject systems we used for our evaluation, and interesting TA fragments which we utilized to test our implementation.

Please note that our tool was compiled with Azul OpenJDK 13.0.1 but it may be run with previous versions of Java. However, if you encounter any problems during execution, please update your Java installation to the latest release.

The tool implementation of our approach is evaluated by means of the five case studies av-protocol, collision-avoidance, gear-control, ieee-rcp, train-gate-controller.
There is a folder for each of the five case studies in the ZIP archive, containing the TA of the case study and all corresponding mutants.

Install CPLEX from https://www.ibm.com/de-de/analytics/cplex-optimizer.
Open the folder TimBrCheck.
The tool (tool.jar) is invoked from the command line.
The following is an example call for the check of timed bisimulation on the RCP case study and one of its mutants.

java  -Djava.library.path=PATH/x86-64_osx -cp "tool.jar:*:PATH/cplex.jar" main.Main -b 30 ieee-rcp/ieee-rcp.xml ieee-rcp/ieee-rcp-reset-1.xml

The parameter b specifies the bound for the zone histories (30 in this example).
A short summary of the execution is printed to the console after finishing the check for bisimilarity.