基于关系闭集的模糊互模拟算法函数式建模及其机械化验证  

The Functional Algorithm and Mechanized Verification of Fuzzy Bisimulation Based on Relational Closed Sets

作　　者：吴嘉伟 游珍 左正康[1] 张晗庆[1] 程着 WU Jiawei;YOU Zhen;ZUO Zhengkang;ZHANG Hanqing;CHEN Zhuo(School of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;State International S&T Cooperation Base of Networked Supporting Software,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学网络化支撑软件国家科技合作基地,江西南昌330022

出　　处：《江西师范大学学报(自然科学版)》2024年第6期640-645,共6页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(62462036,62102171);江西省自然科学基金(20232BAB202010,20212BAB202018);江西省教育厅科学技术研究重点课题(GJJ210340,GJJ2409405)资助项目.

摘　　要：该文在基于关系提升的模糊互模拟算法基础上,设计了一种基于关系闭集的模糊互模拟函数式算法,并使用Isabelle/HOL定理证明器对算法的终止性和正确性进行了机械化证明,为模糊互模拟算法的形式化和自动化验证提供了参考.Based on the fuzzy bisimulation algorithm of relation lifting,the functional algorithm for fuzzy bisimulation based on relation closed sets has been proposed.Using the Isabelle/HOL theorem prover,the termination and correctness of the algorithm are mechanically verified,ensuring the algorithm′s strict correctness.This work provides valuable references for the formalization and automated verification of fuzzy bisimulation algorithms.

关 键 词：模糊互模拟算法 不确定型模糊迁移系统 函数式建模 机械化验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]