%0 Journal Article
%T A Model Checking of Real-Time Systems in Linear Temporal Logic with Clocks<br>基于线性时序逻辑的实时系统模型检查
%A LI Guang-yuan
%A TANG Zhi-song
%A <br>李广元
%A 唐稚松
%J 软件学报
%D 2002
%I 
%X Model checking is an algorithmic technique for checking if a concurrent system satisfies a given property expressed in an appropriate temporal logic. LTLC(linear temporal logic with clocks) is a continuous-time temporal logic proposed for the specification of real-time systems. It is a real-time extension of the temporal logic LTL. In this paper, the model checking problem for LTLC is discrssed and a reduction from LTLC model checking to LTL model checking is presented. This reduction will enable us to use the existingLTL model checking tools for LTLC model chcking.Owing to the to the fact LTLC canexpress both the proerties and implementations of real-time sys,the LTLC modelchecking procedures can be used for both the prperty verication and the refinement verification for real-time systems with finite locations.
%K real-time system
%K timed automaton
%K linear temporal logic
%K model checking
%K property verification<br>实时系统
%K 时间自动机
%K 线性时序逻辑
%K 模型检查
%K 性质验证
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=57B343A01743207E&yid=C3ACC247184A22C1&vid=FC0714F8D2EB605D&iid=0B39A22176CE99FB&sid=23104246A5FCFCEF&eid=974CBB04624305A1&journal_id=1000-9825&journal_name=软件学报&referenced_num=4&reference_num=12