Abstract
Declarative Distributed Systems (DDSs) are a model of distributed computation grounded in declarative, logic programming. A DDS consists of a finite network of computing nodes maintaining an internal state while sharing messages via point-to-point channels and receiving information from external services and/or users. The nodes run declarative programs, written in specializations of Datalog, a query language grounded in logic programming, to the distributed setting. The interest in DDSs first arose in the area of Declarative Networking, in which the declarative paradigm is used to simplify the modeling, implementation, and analysis of network services and distributed systems. For example, DDSs have been used for security and provenance in distributed query processing, the analysis of asynchronous event systems, and as the core of the Webdam language for distributed Web applications. The DDS approach has several advantages, such as the program conciseness, the focus on declaring the system behavior, and the close correspondence between the system and its formal semantics. Moreover, since all of their components are dedicated solely to the manipulation of relational databases, DDSs are examples of data-aware processes and, thus, are of interest in the area of Business Process Management. Despite some previous works on the foundations of DDSs, a rigorous study of verification of these systems has been carried out only recently. In fact, in this thesis, we present our studies on the problem of formal verification of DDSs, focusing on the impact of the main DDS features, i.e., the combination of communication, data-awareness, and logic programming. Specifically, we chart the decidability and complexity boundary of model checking problems for DDSs: while the problem is, in general, undecidable, we identify and motivate interesting decidable fragments. The main complexity in the analysis of DDSs is that they are infinite-state systems. In fact, external services and/or users can provide an infinite flow of fresh data that spread throughout the node states and the channels. The main technique to gain decidability of verification is, thus, to tame this infinity of states, e.g., by enforcing bounds on the size of the DDS components, which, thanks to the features of Datalog-like languages, enable finite abstractions. However, the problem of checking whether these boundedness conditions apply is, in turn, undecidable. Thus, by further studying the interplay of boundedness with the programming language features and with the expressiveness of data-aware messages, we obtain decidable cases in which boundedness is, at least partially, lifted. In doing so, we unveil deep connections with sophisticated models of concurrent computation, i.e., data-aware Petri Nets. Overall, our results enable a deep understanding of the interplay of the DDS features towards the decidability and complexity of DDS model checking and pave the way to the implementation of declarative frameworks for DDS analysis.