Verification of Sometimes Termination of Lazy-Bounded Declarative Distributed Systems

TL;DR

This paper investigates conditions under which the termination of lazy-bounded declarative distributed systems can be verified, identifying decidable cases by adjusting data bounds, message expressiveness, and channel types.

Contribution

It introduces a method to determine termination in DDSs by modifying system parameters, providing a new approach to verify complex distributed logic programs.

Findings

Decidable termination cases identified through parameter adjustments

Tweaking data-source bounds affects system decidability

Channel type modifications influence termination verification

Abstract

Declarative Distributed Systems (DDSs) are distributed systems grounded in logic programming. Although DDS model-checking is undecidable in general, we detect decidable cases by tweaking the data-source bounds, the message expressiveness, and the channel type.