模糊安全性和活性

形式规约使用形式语言构建所开发的软硬件系统的规约,刻画系统的模型和性质.其中,性质规约中的分支时间规约对于系统验证有着非常重要的作用.在经典情形下,系统性质规约是基于二值逻辑的,不能描述不一致或不确定的信息.因此,将其推广到模糊逻辑背景下,有助于对模糊系统进行形式验证.文中首先给出了性质规约中分支时间属性在模糊背景下的形式化定义,重点研究了其中的安全性和活性;然后,定义了两种闭包操作,从而产生了4种类型的属性,即泛安全性、泛活性、存在安全性和存在活性;最后,证明了每个分支时间属性,或是存在安全性和存在活性的交,或是泛安全性和泛活性的交,或是存在安全性和泛活性的交.