An algebra of concurrent non-deterministic processes (Q1179704)

An algebra of finite processes (\(\text{AFP}_ 1\)) is introduced. The semantics of a process is defined as a set of partial orders. Besides two relations between process elements (i.e. precedence and concurrency) the relation of alternative is implicitly represented by an alphabet of ''non-actions'' (reflecting the fact the action was not chosen due to alternative). Another special alphabet is introduced to denote deadlock actions. The axiomatization is proved to be sound and complete and it is shown how properties of processes may be deduced from a given system of axioms.