基于完备剩余格的双标号转换系统  

Doubly Labeled Transition Systems Based on Complete Residuated Lattice

作　　者：潘海玉[1,2] 张敏[2] 陈仪香[2] 

机构地区：[1]安徽工程大学计算机与信息学院,安徽芜湖241000 [2]华东师范大学上海市高可信计算重点实验室,上海200062

出　　处：《模糊系统与数学》2012年第5期21-29,共9页Fuzzy Systems and Mathematics

基　　金：国家自然科学基金资助项目(61021004);国家自然科学基金(青年基金)资助项目(61202105);973项目(2011CB302802);上海市重点学科建设项目(B412)

摘　　要：为了对不相容或不完备信息的系统进行形式化描述和满足对系统进行量化验证的需要,根据经典的双标号转换系统,提出基于完备剩余格的双标号转换系统作为此类系统的一般模型。在该模型框架下,将传统的互模拟关系推广到格值情形,来度量系统之间的接近程度。通过引入格值Hennessy-Milner逻辑的概念,给出格值互模拟关系的逻辑刻画。In this paper, combining with doubly labeled transition systems and complete residuated lattice, we provide a general framework called LLDTS for allowing imprecise or incomplete specifications to be expressed and satisfying the need of quantitative verification. We introduce lattice-valued bisimulation relation between LLDTSs that measure the degree of closeness of two systems as an element of residuated lattice. Moreover, we give its logical characterization in term of an extension of Hennessy-Milner logic.

关 键 词：双标号转换系统 互模拟 Hennessy-Milner逻辑 完备剩余格 

分 类 号：O141[理学—数学] O159[理学—基础数学]