摘要

Although signal automata are more suitable for the modeling of some classes of real-time systems than timed automata, they can not be applied to the practical real-time model verification practical verification of realtime systems due to the lack of verification algorithm. In order to solve this problem, this paper considers the verification of signal automata as that of the timed automata, and reveals the similarity of language recognition as well as the bisimulation relationship between the two types of automata. Moreover, a linear bisimulation algorithm is proposed and is further combined with the existing verification algorithm of timed automata. Thus, a verification algorithm of signal automata is obtained and the verification of signal automata is successfully solved.

全文