Probabilistic Action System Trace Semantics

Abstract. Action systems are a construct for reasoning about concur-rent, reactive systems, in which concurrent behaviour is described by in-terleaving atomic actions. Sere and Troubitsyna have proposed an exten-sion to action systems in which actions may be expressed and composed using discrete probabilistic choice as well as demonic nondeterministic choice. In this paper we develop a trace-based semantics for probabilis-tic action systems. This semantics provides a simple theoretical base on which practical refinement rules for probabilistic action systems may be justified.