Expressiveness Bounds for Completeness in Trace-Based Network Proof Systems
Collections
Author
Widom, Jennifer
Panangaden, Prakash
Abstract
Network proof systems based on first-order specifications over channel traces are incomplete unless reasoning over the interleaving of communication events is permitted. Relatively complete trace-based proof systems using temporal logic have been described, but full temporal logic is more powerful than necessary. Using the interleaving approach, we isolate the expressiveness required of a relatively complete trace logic. A hierarchy of temporal logic subsets is then defined; a certain subset is shown to have necessary and sufficient expressive power for relative completeness.
Date Issued
1987-09
Publisher
Cornell University
Keywords
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-867
Type
technical report