We extend the stochastically timed process algebra EMPA by allowing for value passing. The proposal of Hennessy and Lin relying on symbolic labeled transition systems and symbolic bisimulations is adapted to EMPA by providing suitable semantic rules based on lookahead in order to benefit as much as possible from the inherent parametricity of value passing. This turns out to be quite useful from the analysis point of view, especially to take advantage from symmetries as the example at the end of the paper demonstrates.
Enriching EMPA with Value Passing: A Symbolic Approach Based on Lookahead
Bernardo, Marco
1997
Abstract
We extend the stochastically timed process algebra EMPA by allowing for value passing. The proposal of Hennessy and Lin relying on symbolic labeled transition systems and symbolic bisimulations is adapted to EMPA by providing suitable semantic rules based on lookahead in order to benefit as much as possible from the inherent parametricity of value passing. This turns out to be quite useful from the analysis point of view, especially to take advantage from symmetries as the example at the end of the paper demonstrates.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
