The Impact of Propositional Messages on Termination of Declarative Distributed Systems

Declarative Distributed Systems (DDSs) are data-centric distributed systems grounded in logic programming. Enjoying a close correspondence between the distributed programs and their formal semantics, they configure as an interesting model for studying formal verification of distributed systems. Unfortunately, recent studies proved that the DDS model-checking problem is undecidable, unless boundedness conditions are imposed on the various DDS data-sources. Nevertheless, to check boundedness is, again, undecidable. Thus, we investigate whether it is possible to lift it in favor of syntactic, decidable conditions on the expressiveness of the data-sources. Considering the available decidability results, in this paper we study the impact of weak message expressiveness in place of channel-boundedness and obtain flexible decidability results on DDS verification. Those indicate that boundedness can sometimes be lifted in favor of decidable constraints, while retaining the decidability of the verification problem.