Revising Distributed UNITY Programs is NP-Complete

Abstract

We focus on automated revision techniques for adding Unity properties to distributed programs. We show that unlike centralized programs where multiple safety properties and one progress property can be added in polynomial-time, addition of a safety or a progress Unity property to distributed programs is significantly more difficult. Precisely, we show that such addition is NP-complete in the size of the given program's state space. We also propose an efficient symbolic heuristic for addition of a leads-to property to distributed programs, which has applications in automated program synthesis.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2008
Accession Number
ADA488092

Entities

People

  • Borzoo Bonakdarpour
  • Sandeep S. Kulkarni

Organizations

  • Michigan State University

Tags

Communities of Interest

  • C4I
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Algorithms
  • Computations
  • Computer Science
  • Computers
  • Construction
  • Cycles
  • Detection
  • Distributed Computing
  • Engineering
  • Fault Tolerance
  • Fault Tolerant Computing
  • Language
  • Polynomials
  • Recovery
  • Sequences
  • Specifications
  • Transitions

Fields of Study

  • Computer science

Readers

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

Technology Areas

  • Space