2024. Submitted for publication to an international journal.
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.
@article{TODS-2026,
title = "Verification of Temporal Properties in Declarative Distributed
Systems",
year = "2024",
author = "Diego Calvanese and Di Cosmo, Francesco and Jorge Lobo and
Marco Montali",
note = "Submitted for publication to an international journal",
}