Reactive systems, (semi-)saturated semantics and coalgebras on presheaves
详细信息 查看全文
- 作者：Filippo Bonchi ; Ugo Montanari
- 关键词：Behavioral equivalences ; Reactive systems ; Logic programming ; Petri nets
- 刊名：Theoretical Computer Science
- 出版年：2009
- 出版时间：15 September 2009
- 年：2009
- 卷：410
- 期：41
- 页码：4044-4066
- 全文大小：1582 K
文摘
The semantics of process calculi has traditionally been specified by labelled transition systems (ltss), but, with the development of name calculi, it turned out that reaction rules (i.e., unlabelled transition rules) are often more natural. This leads to the question of how behavioral equivalences (bisimilarity, trace equivalence, etc.) defined for lts can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an lts from reaction rules in such a way that the resulting equivalences are congruences. Furthermore, these equivalences should agree with the standard semantics, whenever one exists.
In this paper, we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and open Petri nets. We also show that saturated semantics can be efficiently characterized through the so called semi-saturated games. Finally, we provide coalgebraic models relying on presheaves.