中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
Intuitionistic Linear-time µ-Calculus
作者: Syed Asad Raza Kazmi
答辩日期: 2008-01-25
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 直觉主义线性µ ; 演算
其他题名: Intuitionistic Linear-time µ-Calculus
摘要: 时序逻辑是一种便于描述并发和反应式系统性质及用于推理的逻辑。这些系统通常具有无穷(即不终止)的系统与环境的交互行为序列。有时我们需要能够同时表示系统有穷和无穷的行为,并区分这些行为。有多种尝试将线性时序逻辑LTL扩展到有穷领域,比如使用强弱两种下一时刻时序算子,使用不同的语义解释,以及有穷无穷行为的一致解释。论文研究直觉线性μ-演算(IμTL),即μ-演算(μTL)的直觉解释。μTL的语义基础是Boolean代数。对于IμTL,语义基础为基于前缀封闭集合的Heyting代数。为给出基于Heyting的IμTL语义,论文定义了解释函数Iiρ。该定义用于刻画反应式系统的重要性质,如安全性质和活性。由于该刻画能够在直觉语义下表示有穷和无穷行为,论文对直觉语义下的安全性质和活性进行了表达。并且,由于IμTL包含不动点,论文证明了互斥问题的一种不动点表示为直觉论域意义下的安全性质。为比较ILTL和IμTL,论文建立它们之间的关系。通过ILTL和IμTL的语义函数的比较,论文论证了ILTL可以从IμTL得到(可以看成是IμTL的子集)。 论文对IμTL语义下的“假设-保证”规范进行了论述。之前的研究对这类规范通常使用不动点描述,论文应用IμTL语义来描述这样的规范。在该描述中,论文使用运行轨迹的集合,而非单个运行轨迹,不动点只是辅助性的。论文基于直觉论域下的不动点解释,建立了一种组合式推理的规则。该规则推广了对于类型为ðφ的安全性质的讨论,并且该规则具有的一般性超出LTL可表达的性质的范围。论文证明了该规则的正确性。论文在直觉论域下将这些规则应用于Moore机器的组合式循环推理。在这个意义下,论文很好地建立了安全性质的这类“假设-保证”规范的推理规则。
英文摘要: Linear time temporal logic (LTL) is a convenient way to specify and reasoning about concurrent and reactive systems. These systems primarily possess an in¯nite behavior i.e. a non-terminating sequence of interactions between system and its environment. It is sometimes desirable to reason about infinite and finite behaviors simultaneously. Various suggestions have been proposed to extend LTL in order to express finite behavior like weak and strong next operators interpretations, semantic interpretations, and uniform treatment of finite and infinite behaviors. We propose intuitionistic linear-time μ-calculus (IμTL) as an intuitionistic variant of linear-time μ-calculus (μTL). The underlying algebra of μTL is Boolean algebra, while for specifications in IμTL we have Heyting algebra of pre¯xed closed set. We define an interpretations function Iρi in order to give the semantics of IμTL based on this algebra. This novel formulation is used to specify and characterize the most important properties of reactive systems namely safety and liveness properties. Since this characterization inherits finite and infinite behaviors simultaneously and is used to define these properties in intuitionisic domain and hence intuitionistic safety and liveness properties are formulated. Furthermore, since IμTL encompasses the fixed point, therefore, fixed point interpretation of mutual exclusion problem as an intuitionistic safety property is proved. In order to compare the relative capabilities of ILTL and IμTL the correspondence between intuitionistic linea-time logic and that of intuitionistic linear-time μ-calculus is established and we compare their expressive powers. The deducibility of ILTL from IμTL is made through their corresponding interpretation functions which are used for semantic interpretation of ILTL and IμTL, and the modalities. Besides that we give the intuitionistic linear-time μ-calculus interpretation of assumption-guarantee specifications. Previously, the fixed point treatment of assumption-guarantee paradigm these specifications is made over least and greatest fixed points, while we treat the assumption-guarantee specifications over a complete domain of intuitionistic linear-time μ-calculus. In this transformation the fixed point interpretation is taken as its subsidiary since we take a set of traces or computation in stead of single trace or computation when dealing with assumption and guarantee properties. We establish the compositional rules in intuitionistic domain with fixed points interpretation.The rules extended the discussion for safety properties of the form □φ and it is quite general such that the properties are not expressible by LTL formulas. We demonstrate the soundness of the rules established in this domain.We applied these rules over the circular composition rules for compositional verification of Moore machines in the intuitionistic domain. Therefore, the assumption-guarantee specification for safety property is well established for IμTL.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6686
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_2004A8015029002Syed Asad Raza Kazmi_paper.pdf(563KB)----限制开放-- 联系获取全文

Recommended Citation:
Syed Asad Raza Kazmi. Intuitionistic Linear-time µ-Calculus[D]. 软件研究所. 中国科学院软件研究所. 2008-01-25.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Syed Asad Raza Kazmi]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Syed Asad Raza Kazmi]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace