Timed testing for models with internal actions

In the paper, we construct a formula that characterizes a timed event structure with discrete internal actions up to the timed must-preorder.