f6a4748bb9a859a1f23030107d76150b61d438c9Till MossakowskiCsp institution
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski---------------
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski- allow for arbitrary alphabet translations, using extra alphabet interpretation component
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski in the models? This would be consistent with CspCASL.
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski That is, for a signature (N,A) (A=syntactic alphabet), a model M=(S,f,T) consists of
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski - a semantic alphabet S
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski - a map f:A->S
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski - for each n\in N, a prefix-closed set T(n) of traces over S
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski The reduct of M along (\nu,\alpha):(N',A')->(N,A) is given by (S,f\circ\alpha,T\circ\nu)
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski The satisfaction condition holds trivially
f6a4748bb9a859a1f23030107d76150b61d438c9Till MossakowskiThis is basically the extension semantics of the WADT 04 polymorphism paper,
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski restricted to signature morphisms that map process names identically
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski that is, in terms of that paper, if we take PI = plain Csp, that is, with
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski arbitrary alpha, but without the extra f component in the models, then the
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski about institution is Ext(PI). Note that plain Csp is neither rps (see Markus' example), nor
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski eps: a->skip ||_a b->skip = stop does not hold iff a=b.
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowskiadd mu to process language, and use modal logic
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski... but this is probably most useful with the LTS semantics for CSP
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski-> develop CSP and CCS and extensions, using Markus' alphabet construction, with LTS semantics,
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski but this is a project on its own...
f6a4748bb9a859a1f23030107d76150b61d438c9Till MossakowskiCspCASL institution
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski-------------------
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski- we can allow for arbitrary (also non-injective) signature morphisms, because:
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski if sigma maps a,b:s to c:s and M |= c.skip=c.skip, then M|_\sigma |= a.skip=b.skip,
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski because a and b are equal in M|_\sigma.
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski- this probably leads to a very natural definition of the CspCASL institution in terms
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski of the Csp institution:
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski Csp-alphabet A = CASL data terms (of any sort)
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski for a model, the semantic alphabet S = \biguplus_{s\in S} M_s \uplus \{\bot\} / ~
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski f = interpretation of CASL terms
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowskichannels are typed in CspCASL -> hence we can statically check that the
f6a4748bb9a859a1f23030107d76150b61d438c9Till Mossakowski sort of a term matches with the sort of the channel over which it is communicated ?!?