Train Resources Conflict Detection of NGTC Based on Probabilistic Timed Automata

The conflict resolution of the multi-train competition Object Controller (OC) resources play an important role in the typical Next Generation Train Control system (NGTC). Due to the nondeterministic communication stochastic behaviour between train and OC, the traditional conflict resolution methods such as graph theory and integer programming can not solve the resources conflict. In this paper, inspired by [1], we newly introduce a formal modeling method, namely probabilistic timed automata (PTA) to solve the conflict of train to OC communication in NGTC considering the communication stochastic behaviour. Firstly, the communication protocol of resource application between train and OC is defined according to the characteristics of train resource application in NGTC system. Secondly, based on PTA, the communication protocol model of resource application is established. Finally, a detail qualitative and quantitative formal analysis of the probabilistic characteristics has been made, such as the probability reachability, the number of conflicts and expected cost of message transmission, based on probabilistic model checking technology. The analysis results show that the defined protocol can be used to apply for resource message successfully without considering the message sending termination caused by the number of conflicts and the upper limit of time.