Abstract：Timed automata are the primary method for formal modeling and checking of real-time systems.They can also check whether various components of the system are correctly interacting and communicating.Both the system models and the properties to be verified are represented by timed automata.The language inclusion checking of timed automata can check whether the system model satisfies given properties with time.At present,there is no perfect language inclusion checking method to be applied to the actual system.Because the method needs system models and properties to be verified have the same set of events.However,in practical problems,system models often contain a large number of events,while properties generally only need to pay attention to a few events.Therefore,we improve the existing timed automata language inclusion checking algorithm so that it only needs to consider the concerned events.And then,we summarize the common property patterns described by timed automata.In addition,the method is applied to a water level control system with effective conclusion.
王婷,苏琪,陈铁明. 结合关注事件的时间自动机语言包含模型检测[J]. 小型微型计算机系统, 2019, 40(12): 2578-2584.
WANG Ting,SU Qi,CHEN Tie-ming. Language Inclusion Checking of Timed Automata with Concerned Events. Journal of Chinese Computer Systems, 2019, 40(12): 2578-2584.
2019, Vol. 40 
