Complete Inference System for Regular Processes with Silent Moves

摘要

Bisimulation between process graphs with silent or invisible steps (tau steps) was studied. The analysis provides a normalization or minimalization result for regular processes, and leads to a complete proof system for regular processes with tau-steps and subject to operations + (alternative composition), . (sequential composition) and // (parallel composition or free merge), thereby proving the consistency of a version of Koomen's fair abstraction rule. It is shown that joining Milner's tau-laws to a regular process without tau-steps does not result in a complete proof system for regular processes with tau steps.