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
基金
英国工程与自然科学研究理事会;
关键词
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 条
[21]   Bisimulations for fuzzy automata [J].
Ciric, Miroslav ;
Ignjatovic, Jelena ;
Damljanovic, Nada ;
Basic, Milan .
FUZZY SETS AND SYSTEMS, 2012, 186 (01) :100-139
[22]   Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems [J].
Wu, Hengyang ;
Chen, Yixiang ;
Bu, Tianming ;
Deng, Yuxin .
FUZZY SETS AND SYSTEMS, 2018, 333 :106-123
[23]   Composing Codensity Bisimulations [J].
Kori, Mayuko ;
Watanabe, Kazuki ;
Rot, Jurriaan ;
Katsumata, Shin-ya .
PROCEEDINGS OF THE 39TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS 2024, 2024,
[24]   Distribution-based limited fuzzy bisimulations for nondeterministic fuzzy transition systems [J].
Qiao, Sha ;
Feng, Jun-e ;
Zhu, Ping .
JOURNAL OF THE FRANKLIN INSTITUTE-ENGINEERING AND APPLIED MATHEMATICS, 2024, 361 (01) :135-149
[25]   NOTES IN DELAYS AND BISIMULATIONS OF SPIKING NEURAL P SYSTEMS USING SNP ALGEBRA [J].
Adorna, Henry N. ;
Buno, Kelvin C. ;
Cabarle, Francis George C. .
THEORY AND PRACTICE OF COMPUTATION, 2015, :15-34
[26]   The refinement calculus of reactive systems [J].
Preoteasa, Viorel ;
Dragomir, Iulia ;
Tripakis, Stavros .
INFORMATION AND COMPUTATION, 2022, 285
[27]   The Experiment Results of Webcam Broadcasting Systems [J].
Kim, Jeong-Myeong ;
Park, Geun-Duk .
2013 INTERNATIONAL CONFERENCE ON IT CONVERGENCE AND SECURITY (ICITCS), 2013,
[28]   BISIMULATIONS OF BOOLEAN CONTROL NETWORKS [J].
Li, Rui ;
Chu, Tianguang ;
Wang, Xingyuan .
SIAM JOURNAL ON CONTROL AND OPTIMIZATION, 2018, 56 (01) :388-416
[29]   Ackermann encoding, bisimulations and OBDDs [J].
Piazza, C ;
Policriti, A .
THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2004, 4 :695-718
[30]   Process equivalences as global bisimulations [J].
de Frutos Escrig, David ;
Rodriguez, Carlos Gregorio .
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2006, 12 (11) :1521-1550