首页/论文/2002.11459

arXiv 2002.114592020-02cs.LO

Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas

Barbara König, Christina Mika-Michalski, Lutz Schröder

备注：: Long version of CMCS 2020 paper
DOI：: 10.1007/978-3-030-57201-3_8

英文摘要：

Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-bisimilar states. The modalities required for the formula are also synthesized on-the-fly, and we present a recipe for re-coding the formula with different modalities, given by a separating set of predicate liftings. Both the game and the generation of the distinguishing formulas have been implemented in a tool called T-BEG.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations

The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial structures, such as finite graphs and digital images, with applications in various case studies including medical image analysis. These recent developments required a generalisation step, from topological spaces to closure spaces. In this work we initiate the study of bisimilarity and minimisation algorithms that are consistent with the closure spaces semantics. For …

2020-05-12cs.LO

Coalgebraic Tools for Bisimilarity and Decorated Trace Semantics

The modelling, specification and study of the semantics of concurrent reactive systems have been interesting research topics for many years now. The aim of this thesis is to exploit the strengths of the (co)algebraic framework in modelling reactive systems and reasoning on several types of associated semantics, in a uniform fashion. In particular, we are interested in handling notions of behavioural equivalence/preorder ranging from bisimilarity for systems that can be represented as non-deterministic coalgebras, to decorated trace semantics for labelled transition systems and probabilistic sy…

2015-02-10cs.FLcs.LO

Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically

Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions in particular. In this paper, the notion of bisimulation induced by a FuTS is addressed from a coalgebraic point of view. A correspondence result is established stating that FuTS-bisimilarity coincides with behavioural equivalence of the associated functor. As ge…

2015-12-21cs.LO

Neighbourhood Structures: Bisimilarity and Basic Model Theory

Neighbourhood structures are the standard semantic tool used to reason about non-normal modal logics. The logic of all neighbourhood models is called classical modal logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, denoted by 2^2. We use this coalgebraic modelling to derive notions of equivalence between neighbourhood structures. 2^2-bisimilarity and behavioural equivalence are well known coalgebraic concepts, and they are distinct, since 2^2 does not preserve weak pullbacks. We introduce a third, intermediate notion…

2009-04-20cs.LO

Symbolic and Asynchronous Semantics via Normalized Coalgebras

The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics (that is defined in terms of bisimilarity) is characterized by the final morphism in some category of coalgebras. Since the behaviour of interactive systems is for many reasons infinite, symbolic semantics were introduced as a mean to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, symbolic bisimilarity has a different shape with respect to ordinary bisimilarity, and thus the standard…

2011-05-13cs.LO

Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic

We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an Eilenberg-Moore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from a relation lifting (a special kind of indexed morphism) and we give a general recipe to construct such liftings in the above three cases. Lastly, we apply this framework to derive logical characteris…

2022-02-04cs.LO

更多相关论文收起更多论文

On Star Expressions and Coalgebraic Completeness Theorems

An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this pape…

2022-03-08cs.FLcs.LO

Abstract Congruence Criteria for Weak Bisimilarity

We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.

2021-10-13cs.LOmath.CT

马尔可夫链上双相似距离的完整定量演绎系统

A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains

本文为有限标记马尔可夫链上的双相似距离提出完全公理化，扩展了定量等式逻辑，并用于度量化的Kleene表示定理。

2018-11-15cs.LO

Generating Witness of Non-Bisimilarity for the pi-Calculus

In the logic programming paradigm, it is difficult to develop an elegant solution for generating distinguishing formulae that witness the failure of open-bisimilarity between two pi-calculus processes; this was unexpected because the semantics of the pi-calculus and open bisimulation have already been elegantly specified in higher-order logic programming systems. Our solution using Haskell defines the formulae generation as a tree transformation from the forest of all nondeterministic bisimulation steps to a pair of distinguishing formulae. Thanks to laziness in Haskell, only the necessary pat…

2017-05-31cs.LO

Simulations and Bisimulations For Coalgebraic Modal Logics

We define a notion of Lambda-simulation for coalgebraic modal logics, parametric on the choice Lambda of predicate liftings for a functor T. We show this notion is adequate in several ways: i) it preserves truth of positive formulas, ii) for Lambda a separating set of monotone predicate liftings, the associated notion of Lambda-bisimulation corresponds to T-behavioural equivalence (moreover Lambda-n-bisimulations correspond to T-n-behavioural equivalence), and iii) in fact, for Lambda-separating and T preserving weak pullbacks, difunctional Lambda-bisimulations are T-bisimulations. In essence,…

2013-04-11cs.LOmath.LO

证明行为分离性

Proving Behavioural Apartness

针对余代数互模拟性证明的局限性，提出通过对偶行为等价定义行为分离性，在子分布函子等系统中将无限量化转化为有限规则，并提供优化证明规则及示例验证。

2024-04-25cs.LO

分支互模拟与弱迹语义之间谱系的单一能量博弈

One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics

本文首次用单一多维能量博弈统一刻画并判定带静默步的线性时间—分支时间谱系中从分支互模拟到弱迹等价的行为等价，并通过 Hennessy–Milner 逻辑的八个表达力维度建立正确性。

2024-11-21cs.LO

开放互模拟的一种直觉主义模态逻辑刻画

A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

本文提出直觉主义模态逻辑$\mathcal{OM}$刻画开放互模拟，通过模态在代换下封闭实现直觉主义遗传性，并在Abella中机械化验证可靠性，同时给出生成区分公式的算法。

2021-08-09cs.LO

Logic-Induced Bisimulations

We define a new logic-induced notion of bisimulation (called $ρ$-bisimulation) for coalgebraic modal logics given by a logical connection, and investigate its properties. We show that it is structural in the sense that it is defined only in terms of the coalgebra structure and the one-step modal semantics and, moreover, can be characterised by a form of relation lifting. Furthermore we compare $ρ$-bisimulations to several well-known equivalence notions, and we prove that the collection of bisimulations between two models often forms a complete lattice. The main technical result is a Hennessy-M…

2020-08-21cs.LOmath.LO

Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus

This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied $π$-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarity, preserving causality. We point out that corresponding similarity preorders expose clearly distinctions between these semantics. We draw particular attention to the distinguishing power of HP failur…

2022-09-06cs.CRcs.DCcs.LO