Verification of Temporal Properties in Communicating Datalog Programs

Logic-based languages, such as Datalog and Answer Set Programming, have been recently put forward as a data-centric model to effectively specify and implement network services and protocols, seeing them as dynamic systems of distributed computational nodes where each node evolves an internal database and exchanges data with the other nodes of the network. This approach provides the basis for declarative distributed computing. A rigorous, comprehensive characterization of the decidability and complexity of verification in declarative distributed systems is yet to come. This paper provides a stepping stone towards this grand objective, considering the case where the network is a fixed connected graph, and nodes can incorporate fresh data from the external world into the system. We study the problem from different angles, delineating the decidability frontier of verification and providing tight complexity bounds for the decidable cases.