文章基本信息

标题：Visible Bisimulation Equivalence — A Unified Abstraction for Temporal Logic Verification ⁎
本地全文：下载
作者：Bengt Lennartson ; Mona Noori-Hosseini
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2018
卷号：51
期号：7
页码：400-407
DOI：10.1016/j.ifacol.2018.06.332
语种：English
出版社：Elsevier
摘要：AbstractBisimulation is an abstraction method that can be used to reduce the number of states for transition systems. This paper presents an alternative formulation of bisimulation, directly based on an equivalence relation and partitioning of the state space. The formulation, here called visible bisimulation equivalence, unifies stuttering and branching bisimulation by including both state and event labels in the abstraction. The proposed divergence-sensitive visible (DSV) bisimulation equivalence is shown to be equivalent to a temporal logic called ECTL*, where CTL* is extended with events. This means that DSV bisimulation equivalence preserves most temporal temporal logic properties that are of interest. The proposed 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. Since the abstraction is polynomial in the number of states and transitions, this is an attractive method for verification and synthesis based on temporal logic.
关键词：Keywordstransition systemsbisimulationabstractiontemporal logic verificationmodular systems