%0 Journal Article
%T Intuitionistic Linear-Time μ-Calculus<br>直觉线性μ-演算
%A KAZMI Syed Asad Raza
%A KAZMI Syed Asad Raza
%A ZHANG Wen-Hui
%A <br>KAZMI
%A Syed
%A Asad
%A Raza
%A 张文辉
%J 软件学报
%D 2008
%I 
%X 线性mu-演算(μTL)是线性时序逻辑(LTL)的不动点扩展.LTL是一个便于规范和论证反应式系统的方法.μTL作为比LTL表达能力更强的逻辑,用LTL表示的性质度可由μTL表示.类似于LTL的直觉线性时序逻辑(ILTL),提出一种基于直觉解释的μTL,称为直觉μTL(IμTL).确立了IμTL和ILTL的关系,比较了它们之间的表达能力.讨论了使用IμTL与安全性质和活性描述的关系以及描述"假设-保证"规范的问题.
%K propositional linear temporal logic<br>命题线性时序逻辑
%K 直觉线性μ-演算
%K intuitionistic
%K linear
%K time
%K μ-calculus
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=024DF690E8285536077C4726381FA620&yid=67289AFF6305E306&vid=2A8D03AD8076A2E3&iid=59906B3B2830C2C5&sid=259C2F715CA6B505&eid=B6A3E865D698AFBC&journal_id=1000-9825&journal_name=软件学报&referenced_num=1&reference_num=27