基于组合不可行路径的组合线性混成自动机可达性验证研究

是 否 +2 论坛币

k人 参与回答

经管之家送您一份

应届毕业生专属福利!

求职就业群

赵安豆老师微信：zhaoandou666

经管之家联合CDA

送您一个全额奖学金名额~ !

立即领取

感谢您参与论坛问题回答

经管之家送您两个论坛币！

+2 论坛币

基于组合不可行路径的组合线性混成自动机可达性验证研究
信息物理系统广泛应用于安全攸关领域,因此要保证其正确性与安全性至关重要。混成自动机是一种既包含了离散的状态转移,又存在连续变量变化的形式化建模语言。
其中离散的逻辑跳转与连续的变量变化混合的特性使得其可以用于对信息物理系统建模与验证。然而正因为离散跳转与连续行为的交织,使得其状态空间极为复杂,即便是对混成自动机安全性问题的可达性问题的验证也异常困难。
在实际的信息物理系统中,由于不同组件通信协作行为的大量存在,组合混成自动机才能满足其建模需求。组合混成自动机由多个单一混成自动机通过同步行为协作构成,其行为比单一混成自动机更为复杂。
目前的研究工作能解决的组合混成自动机验证问题的规模极为有限。因此如何提高组合混成自动机可达性验证规模,提升验证效率是十分值得关注与研究的课题。
本文针对组合混成自动机的子类——组合线性混成自动机的可达性验证进行了系统化研究,研究内容包括:1.基于混合语义的组合线性混成自动机有界可达性验证。本文工作提出了一种基于混合语义的组合线性混成自动机有界可达性验证方法。
该方法采用传统交替语义枚举候选路径,浅同步语义 ...

扫码加我 拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

分享0 收藏0 回帖

关键词：可达性 自动机 如何提高 连续变量 状态空间