Completeness and Incompleteness of Trace-Based Network Proof Systems

摘要

Most trace based proof systems for networks of processes are known to be incomplete. Extensions to achieve completeness are generally complicated and cumbersome. In this paper, a simple trace logic is defined and two examples are presented to show its inherent incompleteness. Surprisingly, both examples consist of only one process, indicating that network composition is not required for incompleteness. Axioms necessary and sufficient for the relative completeness of a trace logic are then presented. The axioms are substantially simpler than existing extensions intended to achieve the same goal.