文章基本信息

标题：Compositional Visible Bisimulation Abstraction Applied to Opacity Verification ⁎
本地全文：下载
作者：Mona Noori-Hosseini ; Bengt Lennartson ; Christoforos Hadjicostis 等
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2018
卷号：51
期号：7
页码：434-441
DOI：10.1016/j.ifacol.2018.06.337
语种：English
出版社：Elsevier
摘要：AbstractIn this paper, an alternative equivalence based definition of bisimulation is proposed, called visible bisimulation equivalence. It includes both state and transition labels and therefore unifies stuttering and branching bisimulation. Furthermore, it is equivalent to a temporal logic called ECTL*, where CTL* is extended with events. The presented bisimulation abstraction is applied to a set of synchronized submodels, where local events are identified incrementally and abstracted after each synchronization. Since the bisimulation reduction is applied after each synchronization, a significant part of the state space explosion in ordinary synchronization is avoided. This compositional abstraction is used for opacity verification, where it is shown that local observers can be generated before they are synchronized, a key factor to be able to apply compositional opacity verification. The efficiency of this method is illustrated on a modular opacity problem with mutual exclusion of moving agents.
关键词：Keywordstransition systemsbisimulationabstractiontemporal logic verificationmodular systemsopacity