How to understand proving correctness of mcrl2 translation of Reo network

[Alireza Farhadi]

Dear Members, Specially Dear Natallia and Christian,

Excuse me about weak contribution in this group.

I understood concept of translation of Reo to mCRL2 with sample that Dr Natallia Kokash sent to me. But in last section of her work she proved correctness of translation. What does this section mean. It contains many formulas and I am confused. Can I have an informal description of what happens in this section and I guess in every translation this kind of proving is needed.

And as a bigger question: When can not we prove a mapping? What aspect of mapping must be exist that we can prove that mapping?

mentioned paper is: http://homepages.cwi.nl/~kokash/documents/FACJ11.pdf

Regards,

Alireza Farhadi

[Christian Krause]

Hi Alireza,

Reo is a modeling language with formal operational semantics. The paper
you are refering to describes an encoding of Reo into the specification
language mCRL2 and correctness proofs for this encoding. In more detail,
the paper contains mCRL2 encodings for several specific Reo channel
types as well as a general mapping scheme from a simplified variant of
the constraint automata semantics of Reo into the mCRL2 specification
language.

mCRL2 is a process algebra based specification language and has on its
own a formal operational semantics. The proofs in the paper basically
show that the CA semantics of Reo and the semantics of the encodings of
Reo in mCRL2 are equivalent. For example, let "Filter(A,B)" denote a
filter channel from node A to node B. Note that this is mere syntax. Now
let CASem(Filter(A,B)) be the constraint automata semantics of this
channel. Now we also define the mCRL2 encoding of this channel:
Encoding(Filter(A,B)) -- this yields an mCRL2 spec (again mere syntax).
No we can compare the semantics of the original channel and the encoded
version of this channel, and we would like to show something like this:

CASem(Filter(A,B)) = mCRL2Sem(Encoding(Filter(A,B)))

where mCRL2Sem(_) gives us the operational semantics of an mCRL2 spec.,
and where '=' denotes so-called observational equivalence (formally:
bisimilarity).

Of course, we want this equivalence to hold for any Reo channel and even
for connectors. Since we employ composition on the mCRL2 level to encode
connectors, we need to also show that the encoding preserves composition
and hiding.

Cheers,
Christian

> <http://homepages.cwi.nl/%7Ekokash/documents/FACJ11.pdf>
>
> Regards,
> Alireza Farhadi
> --
> You received this message because you are subscribed to the Google
> Groups "reo-dev" group.
> To post to this group, send email to reo...@googlegroups.com.
> To unsubscribe from this group, send email to
> reo-dev+u...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/reo-dev?hl=en.