Verification of Sometimes Termination of Lazy-Bounded Declarative Distributed Systems

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.

Published in the online proceedings of the ESSLLI 2021 Student Session