@Article{BliSif10-causal-fmsd,
author = {Simon Bliudze and Joseph Sifakis},
title = {Causal semantics for the algebra of connectors},
journal = {Formal Methods in System Design},
year = 2010,
volume = 36,
number = 2,
pages = {167--194},
month = jun,
publisher = {Springer},
doi = {10.1007/s10703-010-0091-z}
}
@InProceedings{BliSif08-causal-fmco,
author = {Simon Bliudze and Joseph Sifakis},
title = {Causal Semantics for the Algebra of Connectors
(Extended abstract)},
booktitle = {FMCO 2007},
year = 2008,
editor = {Frank de Boer and Marcello Bonsangue},
series = {LNCS},
number = 5382,
pages = {179--199},
publisher = {Springer-Verlag},
address = {Berlin Heidelberg},
doi = {10.1007/978-3-540-92188-2_8}
}
@TechReport{BliSif08-causal-tr,
author = {Simon Bliudze and Joseph Sifakis},
title = {Causal Semantics for the Algebra of Connectors},
institution = {Verimag},
year = 2008,
month = mar,
number = {TR-2008-4},
address = {Centre \'Equation, 38610 Gi\`eres},
url = {http://www-verimag.imag.fr/index.php?page=techrep-list}
abstract = {
The Algebra of Connectors $\ac(P)$ is used to model structured
interactions in the BIP component framework. Its terms are
\emph{connectors}, relations describing synchronization constraints
between the ports of component-based systems. Connectors are
structured combinations of two basic synchronization protocols
between ports: \emph{rendezvous} and \emph{broadcast}.
In a previous paper, we have studied interaction semantics for $\ac(P)$
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 $\ac(P)$, we propose a new \emph{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 $\ct(P)$ formalizes this subset. It is the set
of the terms generated from interactions on the set of ports $P$, by
using two operators: a \emph{causality} operator and a \emph{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 father
participates too. We show that causal semantics is consistent with
interaction semantics. Furthermore, it defines an isomorphism between
$\ct(P)$ and the set of the terms of $\ac(P)$ involving triggers.
Finally, we define for causal trees a boolean representation in terms of
\emph{causal rules}. This representation is used for their manipulation
and simplification as well as for synthesizing connectors.
}
}