Timed testing for dense timed model

In this paper, we try to decide a problem of recognising timed testing equivalences for timed event structures with dense internal actions. For this purpose, we construct a formula that characterizes a timed event structure up to the timed must-preorder. So, to understand if two timed event structures are in testing relations, it is enough to check if the formula is satisfied.