Timed Bisimulation

[hkr-droid]

Hello,

There are several types of equivalence relations we can define on timed automata, including timed/untimed, weak/strong trace equivalence, as well as timed/untimed, weak/strong bisimulation. Uppaal can model check TCTL formulas as well as generate counterexample traces, however, it doesn't seem to consider when two timed automata can be considered "equal" according to the above properties. I can also only find one tool currently that does check these properties, CAAL [1] which works over TCCS expressions (converted internally to certain sorts of dependency graphs), which can be tried out in-browser here: http://caal.cs.aau.dk/.

It's possible I'm missing something obvious, but is there any reason, broadly, why Uppaal doesn't provide facilities for equivalence checking? Or is there anyway to set up a timed bisimulation checking using Uppaal as it is?

If it isn't currently possible, I am happy to write up my own code for checking e.g. timed bisimulation. To that end, I would appreciate any extra context for this. For instance, in the literature, I can find two different presentations of decidable algorithms for checking timed bisimulation in [2] and [3]. The first is based on a region construction over the product of two automata, while the second optimizes the first by swapping regions for zones.

Are these two the canonical ways of constructing such an algorithm, or are there other approaches (game-theoretic?) that are more current? Any help would be appreciated!

[1] http://caal.cs.aau.dk/docs/CAAL2_EPG.pdf
[2] https://dl.acm.org/doi/10.5555/647761.735349
[3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.52.2107

[mikucionisaau]

Hi,
I think Uppaal ECDAR is the closest project to these research questions (it has simulation/refinment checks). Perhaps Ulrik Nyman is the right person to ask, but I don't know his github handle.
Cheers,
Marius

[ulriknyman]

Hi @hkr-droid.
We are indeed working on creating the open source tool Ecdar (https://github.com/Ecdar). We do not have a stable release yet. We are not exactly checking bisimulation but rather refinement. But if you have mutual refinement, then this probably comes close to what you want.
The theory TIOA (Timed Input/Output Automata) that we are basing this on is best presented in the paper: https://vbn.aau.dk/ws/portalfiles/portal/58768871/HSCC2010cameraready.pdf
We are currently also working on an updated and extended version of this as a journal paper (hopefully submitted before summer).

The history of the tool can be found here: http://ulrik.blog.aau.dk/ecdar/ecdar-history/
All papers on Ecdar, can be found here: http://ulrik.blog.aau.dk/ecdar/

Please don't hesitate to ask more questions, if this formalism could be relevant for you.
Best regards Ulrik

[hkr-droid]

Hello @ulriknyman ,

Thank you for the quick response. I downloaded Uppaal Ecdar (https://uppaal.org/downloads/) and went through the examples given in the camera ready paper. I think refinement looks like a promising direction. My use case involves optimizing certain types of networks which I model as TA; in that sense, refinement might actually be closer to what I want.

I can see from the Ecdar github that there are a few different versions available: Ecdar-GUI, j-Ecdar, and Reveaal. I know you said there isn't a current stable release, but would you recommend any of these in particular for refinement checking?

Looking forward to investigating further!

Best,

Harlan