Abstract:
|
Logic-based languages, such as Datalog and Answer Set Programming,
have been recently put forward as a data-centric model to specify and implement
network services and protocols. This approach provides the basis for
declarative distributed computing, where a distributed system consists of a network
of computational nodes, each evolving an internal database and exchanging
data with the other nodes. Verifying these systems against temporal dynamic
specifications is of crucial importance. In this paper, we attack this problem by
considering the case where the network is a fixed connected graph, and nodes
can incorporate fresh data from the external environment. As a verification formalism,
we consider branching-time, first-order temporal logics. We study the
problem from different angles, delineating the decidability frontier and providing
tight complexity bounds for the decidable cases. |