Abstract
Communicating Datalog Programs (CDPs) are a distributed computing model grounded on logic programming, where networks of nodes perform Datalog-like computations, leveraging also on information coming from incoming messages and databases received from interactive external services. In previous works, the decidability and complexity border of verification for different variants of CDPs was charted. While the problem is undecidable in general, model-checking FO-CTL formulae (specialized to the distributed setting) is PSPACE-complete in data-complexity for CDPs where all data-sources, except the external inputs, are bounded. While an intuitive explanation for decidability is that "a bounded state is unable to fully take advantage of an unbounded input", a formal justification is missing. At closer inspection, we have noticed that CDPs have a limited capability of handling external inputs, i.e., they cannot compare two successive instances. Thus, an alternative explanation is that an unbounded data-source does per se not cause undecidability, as long as the CDP cannot compare two successive instances. In this short paper, we report about our work in progress on this problem.