TY - GEN
T1 - Causal semantics for the algebra of connectors
AU - Bliudze, Simon
AU - Sifakis, Joseph
PY - 2008/12/1
Y1 - 2008/12/1
N2 - The Algebra of Connectors is used to model structured interactions in the BIP component framework. Its terms are connectors, i.e. relations describing synchronization constraints between the ports of component-based systems. Connectors are structured combinations of two basic synchronization protocols between ports: rendezvous and broadcast. They are generated from the ports of P by using a binary fusion operator and a unary typing operator. Typing associates with terms (ports or connectors) synchronization types: trigger or synchron. In a previous paper, we studied interaction semantics for which defines the meaning of connectors as sets of interactions. This semantics reduces broadcasts into the set of their possible interactions and thus blurs the distinction between rendezvous and broadcast. It leads to exponentially complex models that cannot be a basis for efficient implementation. Furthermore, the induced semantic equivalence is not a congruence. For a subset of, we propose a new causal semantics that does not reduce broadcast into a set of rendezvous and explicitly models the causal dependency relation between triggers and synchrons. The Algebra of Causal Trees formalizes this subset. It is the set of the terms generated from interactions on the set of ports P, by using two operators: a causality operator and a parallel composition operator. Terms are sets of trees where the successor relation represents causal dependency between interactions: an interaction can participate in a global interaction only if its parent participates too. We show that causal semantics is consistent with interaction semantics. Furthermore, it defines an isomorphism between and the set of the terms of involving triggers. Finally, we define for causal trees a boolean representation in terms of causal rules.
AB - The Algebra of Connectors is used to model structured interactions in the BIP component framework. Its terms are connectors, i.e. relations describing synchronization constraints between the ports of component-based systems. Connectors are structured combinations of two basic synchronization protocols between ports: rendezvous and broadcast. They are generated from the ports of P by using a binary fusion operator and a unary typing operator. Typing associates with terms (ports or connectors) synchronization types: trigger or synchron. In a previous paper, we studied interaction semantics for which defines the meaning of connectors as sets of interactions. This semantics reduces broadcasts into the set of their possible interactions and thus blurs the distinction between rendezvous and broadcast. It leads to exponentially complex models that cannot be a basis for efficient implementation. Furthermore, the induced semantic equivalence is not a congruence. For a subset of, we propose a new causal semantics that does not reduce broadcast into a set of rendezvous and explicitly models the causal dependency relation between triggers and synchrons. The Algebra of Causal Trees formalizes this subset. It is the set of the terms generated from interactions on the set of ports P, by using two operators: a causality operator and a parallel composition operator. Terms are sets of trees where the successor relation represents causal dependency between interactions: an interaction can participate in a global interaction only if its parent participates too. We show that causal semantics is consistent with interaction semantics. Furthermore, it defines an isomorphism between and the set of the terms of involving triggers. Finally, we define for causal trees a boolean representation in terms of causal rules.
U2 - 10.1007/978-3-540-92188-2_8
DO - 10.1007/978-3-540-92188-2_8
M3 - Conference contribution
AN - SCOPUS:58849143408
SN - 3540921877
SN - 9783540921875
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 179
EP - 199
BT - Formal Methods for Components and Objects - 6th International Symposium, FMCO 2007, Revised Papers
T2 - 6th International Symposium on Formal Methods for Components and Objects, FMCO 2007
Y2 - 24 October 2007 through 26 October 2007
ER -