文章基本信息

标题：Conditional Bisimilarity for Reactive Systems
本地全文：下载
作者：Mathias H{"u}lsbusch ; Barbara K{"o}nig ; Sebastian K{"u}pper 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：167
页码：10:1-10:19
DOI：10.4230/LIPIcs.FSCD.2020.10
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Reactive systems Ã la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We instantiate reactive systems in order to obtain DPO graph rewriting and consider a case study in this setting.
关键词：conditional bisimilarity; reactive systems; up-to context; graph transformation