Abstract
Communicating Datalog Programs (CDPs) are a distributed computing model grounded on logic programming: networks of nodes perform Datalog-like computations, leveraging on information coming from incoming messages and databases received from external services. In previous works, the decidability and complexity border of verification for different variants of CDPs was charted. In general, the problem is undecidable, but model-checking of CTL formulas specialized to the data-centric and distributed setting is decidable for CDPs where all data-sources, except the external inputs, are bounded. An intuitive explanation is that “a bounded state is unable to fully take advantage of an unbounded input”, a formal justification is missing. However, we note that traditional CDPs have a limited capability of handling external inputs, i.e., they cannot directly compare two successive inputs or messages. 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.