Ines Margaria and Maddalena Zacchi
A filter model for safe ambients
In Furio Honsell, Marina Lenisa, and Marino Miculan, editors,
Proc. Final Workshop Project COMETA, ENTCS, Udine, Italy, December 2003
Elsevier/Forum
The definition of filter model is extended to a variant of Ambient
Calculus:
Safe Ambient Calculus, introduced for developing an algebraic theory for
a bisimulation-based behavioral equivalence.
The types are constructed by means
of elementary and higher-order actions,
that define the moves processes can do.
Entailment rules for types allow to translate the parallel
composition of moves
into nondeterministic choice of sequences of interleaved actions,
providing a normal form
for types assigned to processes.
In the filter model obtained via the introduced
type system, any process is interpreted as the set of all its types.
The type assignment system results to be sound and complete with respect
to the given semantics.
Moreover the partial order relation induced by the filter
model is compared with observational equivalence:
the model is proved adequate,
but it is shown, by means of a counter-example, that full abstractness fails.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43