Completeness and Incompleteness of Trace-Based Network Proof Systems.

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1986
Accession Number
ADA170710

Entities

People

  • David Gries
  • Fred B. Schneider
  • Jennifer Widom

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Communication Channels
  • Computations
  • Computer Graphics
  • Computer Programming
  • Computer Science
  • Computers
  • Information Processing
  • Language
  • Logic
  • Military Research
  • Models
  • New York
  • Number Theory
  • Programming Languages
  • Software Development
  • Theorems
  • Verification

Readers

  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design