Communicating Datalog Programs (CDPs) are a distributed computing model grounded on logic programming, where networks of nodes perform Datalog-like computations, leveraging also on information coming from incoming messages and databases received from interactive external services. In previous works, the decidability and complexity border of verification for diferent variants of CDPs was charted. While the problem is undecidable in general, model-checking FO-CTL formulae (specialized to the distributed setting) is PSPACE-complete in data-complexity for CDPs where all data-sources, except the external inputs, are bounded. While an intuitive explanation for decidability is that "a bounded state is unable to fully take advantage of an unbounded input", a formal justification is missing. At closer inspection, we have noticed that CDPs have a limited capability of handling external inputs, i.e., they cannot compare two successive instances. 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. In this short paper, we report about our work in progress on this problem.
Declarative languages are appreciated for their capability of specifying queries and algorithms
in an elegant and succinct way. For that reason, in the last decades, Datalog-like languages
have been proposed as a programming language for distributed systems. Some examples are
Webdamlog [
Since DDSs are formalized in logic, one can directly apply formal methods for verification. However, the verification of data-aware systems is hard, since they can manipulate fresh data provided by input databases (DBs) from external services, resulting in infinite state systems. Unsurprisingly, verification of problems like control-state reachability is undecidable.
Nevertheless, previous works [
However, this fact could also depend on additional reasons, based on the peculiarity of the interaction of DDSs with external sources, e.g., lack of queries over previously provided external data. In fact, remarkably, the traditional DDS model assumes that nodes can query the previous configuration of their internal memory but not the external inputs. Thus, it may be the case that combinations of boundedness/unboundedness conditions and the ability/inability to query previous instances of the data-sources may have an important impact on the decidability and complexity boundary of verification problems for DDSs.
In this paper, we report about our work in progress towards the study of this problem. To that
end, first, we consider a type of DDS, called Communicating Datalog Programs (CDP), already
studied by Calvanese et al. [
We assume that the reader is familiar with the notion of Database (DB), under the logic
programming perspective, and with variants of the Datalog language (see [
A CDP is a network of nodes running a program, in the Datalog-like language D2C, sharing messages containing single facts. We assume that the network is a connected, reflexive, and symmetric directed graph, where each edge represents a channel. Each node has access to a DB containing its own name and the names of all its neighbors.
Messages are sent on a channel (, ) from the source node to the destination node . They are single relational facts over a dedicated transport signature . Messages are received according to the asynchronous policy, i.e., at each computation step only one sent message is delivered. A configuration for a channel represents the messages sent on the channel that have not yet been received. In CDPs, channels are assumed to be unordered, i.e., messages are never lost but the sending order may be diferent from the delivery one. 1 Thus, channel configurations are assumed to be bag-DBs, i.e., a finite bag of facts.
Next to channels, CDP nodes receive information from external services. This is modeled by the availability to each node of an input DB over an input signature ℐ. We assume that the input DB can freely change over time, i.e., at each computation step, the input DB may be updated to a diferent (possibly unrelated) DB over ℐ. On top of that, nodes have a local memory, which 1This choice is in line with the fact that, in general, Datalog rules (responsible for the production of messages) do not have to be computed in a specific order. contains auxiliary information deduced by the node during the previous computation step. The latter is stored in a state DB over a state signature .
The reception of a message at a node triggers a new computation step.2 First, is removed from its channel. Then, while all other nodes remain inactive, i.e., their state DB is not updated, the node combines the input DB, its previously computed state DB, and the message labeled by the sender name (i.e., a labeled transport fact @) in a single DB, used as extensional data on which a D2C program is computed. The program returns a new state DB and a set of outgoing messages labeled with destinations. Finally, the CDP configuration is upadated by (1) updating the state DB of with the new one and (2) adding the outgoing messages (without addresses) to the respective channel configurations.
A D2C program is a finite set of Datalog-like rules with special features to handle the reception
and sending of messages and the query of the previous state DB. Communication is handled
by labeling transport literals with addresses , resulting in the formulas @: in the body
of a rule, the address represents the node sending the incoming message; in the head, the
address represents the recipient of the outgoing message. To query the previous state DB, a
special flag prev is used: all predicates in its scope should be considered as ranging over the
(extensional) previous input, state, and locally received message, while all other predicates
should be considered as ranging over the (intensional) current state DB. Traditionally, it is
required that only state literals can occur in the scope of prev. In this paper, we allow all
literals, irrespective of their signature, to occur in the scope of prev. D2C rules can also make
use of inequality constraints and choice operators choice(X, Y) and choice(Y) a la Saccà and
Zaniolo [
Finally, the D2C program must be stratified , i.e., stratified a la Datalog when the transport predicates in the body and the predicates in the scope of prev are interpreted as extensional predicates. Both stratification and formal semantics of the program can be formalized via an encoding in traditional Datalog rules. Moreover, we assume that the payload of outgoing messages is retrieved from the state DBs, so that it is not possible to directly transfer the active domain of the input DB into the channels.
We now define constraints on the various CDP data-sources, i.e., state, input, and channel. A configuration is reachable if it can be obtained from the initial configuration in a finite number of computation steps. Given a ∈ N, we say that a CDP is -state bounded (or that the state data-source is -bounded) if, for each reachable configuration , the active domains of all state DBs in contain at most constant. We say that it is -channel bounded (or that the channel data-source is -bounded) if all the channel bag-DBs contain at most facts (considering multiplicities). A similar constraint can be put on the input. However, in this case, we have to change the semantics of CDPs. Specifically, a -input bounded CDP is a CDP with the provision that the available input DBs have active domain bounded by . A data-source is bounded if it is -bounded for some . A CDP is bounded if all its data-sources are bounded.
Given a CDP with program Π , a data-source is prev-free if there is no literal in the signature of that occurs in the scope of prev in some rule of Π . Otherwise, it is prev-aware. 2At startup, each self-loop channel contains a special activation message, used to trigger the first computation step.
PF B B D
BPF ⊤ BPF U
BPF
B PF U
PF PF BPF U ⊤ BPF BPF U
B B B D
BPF PF PF D
BPF BPF ⊤ U
PF BPF PF D
B BPF PF U
B PF B D
Previous results on the verification of CDPs showed that CTL DDS model checking is decidable
only if all the data-sources are bounded [
However, the input data-source is unique in its kind because it is the only one on which it is not possible to simulate a prev by exploiting the prev on the state, without violating state boundedness assumptions. In other words, the absence, by definition, of prev over the input data-source is not without loss of generality and may (1) motivate the unique impact of inputunboundedness on decidability of verification and (2) prevent the formulation of interesting CDP fragments, with decidable verification, based on combinations of boundedness conditions and non-availability of the prev operator over the various data-sources.
We name fragments by means of a triple of constraints on the various data-sources. Specifically, − − denotes the family of all CDPs whose input data-source is constrained by , whose state data-source is constrained by , and whose channel data-source is constrained by . We consider four types of constraints: BPF enforces both boundedness and prev-freeness, B enforces boundedness but not necessarily prev-freeness, PF enforces prev-freeness but not necessarily boundedness, and ⊤ does not enforce any constraint. Thus, we are dealing with 64 fragments. We call them prev-based fragments.
As verification task, we focus on the problem of termination4 because (1) this is one of the problems that characterises the decidability status of model checking problems against CTLDDS and (2) it is closely related with other problems, such as control-state reachability and convergence.5
The decidability of termination of some of these fragments is an immediate consequence of
the results by Calvanese et al. [
Finally, we focus on single-node networks. This comes without loss of generality, since any arbitrary network can be encoded in a single-node network, at the cost of considering a sort of disjoint union of the CDP signatures and program.
PF-PF-BPF This fragment has undecidable termination, since, given a 2-counter machine (2CM) , we can build a PF-PF-BPF CDP that terminates if terminates, which, in turn, is an undecidable problem. This can be done by encoding finite runs of in input DBs. By exploiting the unbounded state DB, we can write a program Π that does not make use of prev such that, as soon as an input DB is received, it produces a terminate flag if encodes a terminating run of . In this case, no message is sent on the channel (making it empty). Otherwise, foo messages will be sent on the channel forever. The program Π exists because it can make use of an unbounded state DB, which can be used to compute, most notably, transitive closures of unbounded graphs in input DBs. ⊤-BFP-BPF Also this fragment has undecidable termination. In fact, we can modify the previous technique by scattering the provision of a 2CM run along many steps. Specifically, we can encode the next configuration of the (unbounded) counters of in the input DB and use prev on the input to check whether the new configuration can be reached via a transition of . If this test fails, non-termination is triggered as above. Otherwise, termination is triggered only if the final state of is reached.
B-B-B This fragment has decidable termination. In fact, since all data-sources are bounded,
we can use the same technique as for BPF-B-BPF CDPs by Calvanese et al. [
BPF-PF-PF This fragment has decidable termination. Since the state is prev-free, the new state
contains only constants from the incoming message (which are in bounded number because the
transport signature has a maximal finite arity) and from the input DB, which is bounded. Thus,
also the state is bounded. Notice that, since all sources are prev-free, the name of constants in
the messages on the channel are irrelevant. Thus, we can abstract away the messages up to
isomorphisms. Since each message contains a bounded number of constants, they result in a
ifnite family of messages. We interpret them as non-terminal symbols of a context free grammar
(CFG). The reception of one of these symbols results in the production of a (possibly empty)
set of non-terminal symbols, by sending outgoing (abstracted) messages. Thus, the program
can be encoded in a finite number of production rules, defining a CFG. Hence, termination of
BPF-PF-PF CDPs reduces to the emptyness problem of CFGs, which is decidable.
BPF-BPF-⊤ This fragment has undecidable termination. The idea is that we can, at each
step, encode in the unbounded channel an arbitrary natural number. This can be achieved via a
binary predicate succ, maintaining a structure of the form: succ(min, n0), . . . , succ(nm, max)
where min and max are special constants mentioned in the program and the nis are pairwise
diferent constants retrieved from the input. By exploiting the prev-awareness of the channel
and exploiting a technique similar to the one from Theorem 2 in [
PF-BPF-PF This fragment has decidable termination. In fact, we can extend the technique
from Theorem 4 in [
B-BPF-PF This fragment has undecidable termination. In fact, we can use the prev on the input to simulate a prev on the channels. It sufices to require that the current received message is also mentioned in the current input DB. If that is not the case, an error is deduced and non-termination is triggered. Thus, this fragment can encode an extension of BPF-BPF-⊤, which was argued to be undecidable.
B-PF-B This fragment has decidable termination. In fact as in a previous case, the state turns out to be bounded, thus boiling down to the decidable fragment B-BPF-B.
We have sketched proofs to establish the decidability status of termination for 8 prev-based
fragments. Together with the previous results in [