论文部分内容阅读
采用了基于进程代数的并发TCSP语言,规范了整个计算过程,精确地描述了列车的移动行为,统计了列车在给定时间段、给定观察区域的最大数量。给出了计算的表达式,还用该语言表示了计算过程。通过迹行为的精化,能判断运输能力的容量。这种方法以标准化、形式化的方式表示了整个过程的计算框架,同时也为验证系统关键性质打下了坚实的基础。