时间符号迁移图及其互模拟判定

引入时间符号迁移图的概念，作为既涉及通讯又具有实时性的并发系统的模型，该文给出了这种迁移图时间互模拟的算法，并证明了该算法的正确性。

Timed Bisimulation over Timed Symbolic Transition Graph

A new modeling language, Timed Symbolic Transition Graph(TSTG), is introduced which can characterize both real time and value passing systems. An algorithm checking the timed bisimulation between TSTGs is presented.Traditionally, Labeled Transition System(LTS) is used to characterize the behavior of systems with states connected by directed edges labeled by some actions. Since LTSs do not contain variables, they are not suitable for explicit manipulation of data transfer between systems. In this paper, we use TSTG to model value passing processes where processes can communicate with each other by exchanging messages(data) via channels. Another capability of TSTG is that it can model real time processes. To model the behavior of real time processes, it uses some clock variables with values ranging over non negative real numbers, where all the clocks will increment at the same speed in order to model time elapse. As value passing systems and real time systems are studied separately generally, TSTG is the first modeling language which can model such mixed systems under the unified framework.Bisimulation checking is a very important method in automatic verification of software and hardware systems, where timed bisimulation is a kind of equivalence relation between real time systems. In this work, we present an algorithm for the timed bisimulation checking between TSTGs together with its correctness proof.