Arrow Research search

Author name cluster

R. Gorrieri

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

I&C Journal 1995 Journal Article

A Causal Operational Semantics of Action Refinement

  • P. Degano
  • R. Gorrieri

A TCSP-like concurrent language is extended with an operator for action refinement which plays a role similar to that of procedure-call for sequential languages. The language is given a denotational semantics that fully expresses causality in terms of Causal Trees. These are Synchronization Trees where each arc has a richer labelling containing, besides an action name, also the set of backward pointers to those arcs "causing" the present action. An operational semantics reflecting causality is also defined in SOS style by a causal transition system, the unfoldings of which are causal trees. The denotational and operational semantics agree up to causal bisimulation, which is proved to be a congruence for ail the operators of the calculus; notably, for the refinement operator. Also, a complete set of axioms is provided that characterizes the congruence classes of causal bisimulation for finite agents. The main result of the paper is an operational semantics firmly based on a view of action refinement as purely semantic substitution. Therefore, its operational definition provides a "parallel copy rule, " i. e. , the concurrent analogous of the classic "copy rule" for sequential languages.

Details DOI

I&C Journal 1995 Journal Article

Split and ST Bisimulation Semantics

  • R. Gorrieri
  • C. Laneve

In this paper the notion of action atomicity is relaxed by permitting actions to be observed in the middle of their evolution. Non-atomic semantic equivalences, based on the notion of bisimulation, are studied over stable event structures, Split n bisimulation equivalence (denoted ∼ n considers each event as composed of n phases. ST bisimulation equivalence (denoted ∼ ST ) is a slight refinement of ∼2 where each ending phase is unambiguously associated to a beginning phase, We prove that, by increasing n, we get finer and finer equivalences (i. e. , ∼ n + 1 ⊆ ∼ n ) and, moreover, that ∼ n + 1 coincides with ∼ ST over those event structures whose autoconcurrency is at most n. The main consequence of these results is that, for image finite event structures, ∼ ST is the intersection of all the ∼ n.

Details DOI
v2026.09.13