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机器的组合式循环推理。在这个意义下，论文很好地建立了安全性质的这类“假设-保证”规范的推理规则。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 94 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6686]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | Syed Asad Raza Kazmi. Intuitionistic Linear-time µ-Calculus[D]. 软件研究所. 中国科学院软件研究所. 2008. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。