Trace refinement of action systems

Abstract. Action systems provide a general description of reactive systems, capable of modeling terminating, aborting and infinitely repeating systems. Arbitrary sequential program statements can be used to describe the behavior of atomic actions. Action systems are used to extend program refinement methods for sequential programs to parallel and reactive system refinement. We give here a behavioral semantics of action systems in terms of execution traces, and define refinement of action systems in terms of this semantics. We give a simulation based proof rule for action system refinement in a reactive context, and illustrate the use of this rule with an example. The proof rule is complete under certain restrictions.