Bisimulations for a calculus of broadcasting systems

被引：15

作者：

Hennessy, M ^{[1
]}

Rathke, J ^{[1
]}

机构：

[1] Univ Sussex, Dept Cognit & Comp Sci, Brighton BN1 9QH, E Sussex, England

来源：

THEORETICAL COMPUTER SCIENCE | 1998年 / 200卷 / 1-2期

基金：

英国工程与自然科学研究理事会;

关键词：

broadcasting; bisimulation; barbed equivalence; verification; proof systems;

D O I：

10.1016/S0304-3975(97)00261-2

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence we study are justified in terms of a characterisation as the largest CBS congruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over finite terms. The first system we give contains an infinitary proof rule to accommodate input prefixes. We improve on this by presenting a finitary proof system where judgements are relative to properties of the data domain. (C) 1998-Elsevier Science B.V. All rights reserved.

引用

页码：225 / 260

页数：36

共 50 条

[41] Bisimulations Generated from Corecursive Equations [J].

Capretta, Venanzio .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2010, 265 :245-258

[42] COST PRESERVING BISIMULATIONS FOR PROBABILISTIC AUTOMATA [J].

Turrini, Andrea ;

Hermanns, Holger .

LOGICAL METHODS IN COMPUTER SCIENCE, 2014, 10 (04)

[43] Bisimulations for Probabilistic Linear Lambda Calculi [J].

Deng, Yuxin ;

Feng, Yuan .

PROCEEDINGS 11TH 2017 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2017, :24-31

[44] Labeled fuzzy approximations based on bisimulations [J].

Du, Yibin ;

Zhu, Ping .

INTERNATIONAL JOURNAL OF APPROXIMATE REASONING, 2018, 94 :43-59

[45] The Marriage of Bisimulations and Kripke Logical Relations [J].

Hur, Chung-Kil ;

Dreyer, Derek ;

Neis, Georg ;

Vafeiadis, Viktor .

ACM SIGPLAN NOTICES, 2012, 47 (01) :59-72

[46] Computing maximal weak and other bisimulations [J].

Boulgakov, Alexandre ;

Gibson-Robinson, Thomas ;

Roscoe, A. W. .

FORMAL ASPECTS OF COMPUTING, 2016, 28 (03) :381-407

[47] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems [J].

Xu, Xian .

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2009, 24 (01) :122-137

[48] First-order μ-calculus over generic transition systems and applications to the situation calculus [J].

Calvanese, Diego ;

De Giacomo, Giuseppe ;

Montali, Marco ;

Patrizi, Fabio .

INFORMATION AND COMPUTATION, 2018, 259 :328-347

[49] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems [J].

Xian Xu .

Journal of Computer Science and Technology, 2009, 24 :122-137

[50] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems [J].

徐贤 .

Journal of Computer Science & Technology, 2009, 24 (01) :122-137

← 1 2 3 4 5 →