Volume 42, Numbers 6-7, 389-418, DOI: 10.1007/s00236-005-0172-4

Refinement of actions for real-time concurrent systems with causal ambiguity

Mila Majster-Cederbaum, Jinzhao Wu and Houguang Yue

View Related Documents

Abstract

Refinement of actions is a core operation in the hierarchical design methodology for concurrent systems. In this paper, we develop an approach of action refinement for concurrent systems with not only the notation of real-time but also with causal ambiguity, which often exists and appears in real application areas. The systems are modeled in terms of a timed extension of bundle event structures with causal ambiguity. Under a certain partial order semantics, the behavior of the refined system can be inferred compositionally from the behavior of the original system and from the behavior of the systems used to refine actions with explicitly represented start points. A variant of a linear-time equivalence termed pomset trace equivalence and a variant of a branching-time equivalence termed history preserving bisimulation equivalence based on the partial order semantics are both congruences under the refinement. The refinement operation behaves thus well and meets the commonly expected properties.

Keywords  Concurrency - Action refinement - Causal ambiguity - Timed bundle event structure with causal ambiguity

Fulltext Preview

Image of the first page of the fulltext document