We study verification of reachability properties over Communicating Datalog Programs (CDPs), which are networks of relational nodes connected through unordered channels and running Datalog-like computations. Each node manipulates a local state database (DB), depending on incoming messages and additional input DBs from external services. Decidability of verification for CDPs has so far been established only under boundedness assumptions on the state and channel sizes, showing at the same time undecidability of reachability for unbounded states with only two unary relations or unbounded channels with a single binary relation. The goal of this paper is to study the open case of CDPs with bounded states and unbounded channels, under the assumption that channels carry unary relations only. We discuss the significance of the resulting model and prove the decidability of verification of variants of reachability, captured in fragments of first-order CTL. We do so through a novel reduction to coverability problems in a class of high-level Petri Nets that manipulate unordered data identifiers. We study the tightness of our results, showing that minor generalizations of the considered reachability properties yield undecidability of verification, both for CDPs and the corresponding Petri Net model. This paper is an abridged version of a paper published in the Proceedings of the 43rd ACM Symposium on Principles of Database Systems (PODS 2024).
Declarative approaches to the specification of distributed data-aware systems have been
extensively studied in many diferent contexts [
In this work, we are interested in the static analysis of such distributed declarative
dataaware processes, in the style of [
Declarative distributed systems with asynchronous communication occurring over multiset
channels (where multiple copies of the same message may exist, even when the sender and
receiver coincide) were considered in seminal works in the area, but only studied in connection
with static analysis in the presence of external data in [
In this work, we start from the observation that bounding communication channels is a severe
restriction, as it cannot be enforced even by suitably controlling how nodes are programmed.
At the same time, [
In this section, we informally introduce the CDP model by Ma et al. [
A CDP is a fixed network of data-centric nodes sharing messages via point-to-point channels. Each node (1) runs a Datalog-like program, written in the language D2C, (2) updates its internal state, which is maintained as a state DB over a dedicated state signature, (3) receives information from the external environment, in the form of an input DB over a dedicated input signature, and (4) shares messages, i.e., single relational facts over a dedicated transport signature. The nodes react to incoming messages: when a message from a node is delivered to a node , the latter gets activated and runs the program on its data-sources. In fact, the program input consists of the node state DB, the current input DB, the message itself, and the local structure of the network at , in the form of a network DB. The output provides a new state DB for and a set of outgoing messages, each labeled by its recipient, which, in turn, are sent on the respective channels (without labels).
We assume that communication is asynchronous and channels are reliable but unordered, that is, at each time-step, only one message is delivered (and, thus, only one node gets activated), no message can be lost, but the reception order is non-deterministic. These assumptions are useful, e.g., to model communication networks where message loss is ignored but order cannot be guaranteed (e.g., because of an underlying UDP transport protocol). Since nodes react only to incoming messages, the communication network has, for each node, a self-loop channel (from the node to itself), which initially contains a special message dedicated to node activation.
CDP nodes are exposed to information from the external environment, which represents users and/or external services. Environment interaction is abstracted away by input policies, i.e., rules to provide a new input DB. In this paper, we focus on the -bounded interactive input policies, where P N: each time a node receives a message, the current input DB is substituted by a non-deterministically chosen new one with active domain of cardinality at most . This policy is relevant to model interaction with external users that continuously provide new information, e.g., text messages for a chat application.
All these information sources are manipulated by a D2C program, i.e., a set of
Dataloglike rules specialized to the interactive and distributed setting of CDPs. The specialization is
achieved by (1) organizing relation symbols in dedicated signatures (state, input, and transport),
(2) using the in-rule flag prev to distinguish queries over the previous state DB and the new
one under computation, and (3) labeling transport literals with terms representing senders or
recipients (see [
A D2C rule over a CDP signature Λ is a formula
if 1, . . . , prev `1, . . . , `, 1, . . . , ℎ. s.t.: (1) is a state or transport literal, (2) 1, . . . , are state, input, or transport literals, (3) `1, . . . , ` are state literals, and (4) 1, . . . , ℎ are inequality constraints of the form 1 ‰ 2, where 1 and 2 are terms (constants or variables). The rule head is and the rule body is the part following if . The rule scope of prev is `1, . . . , `. The rule is safe if each variable occurring in the head, in a negated literal, or in an inequality constraint, also occurs in a positive literal in the rule body. The rule is transport consistent if each variable occurring in a transport atom in the head also occurs in a positive non-input literal.
Intuitively, in the scope of prev, state literals query the state DB available immediately before node activation. Outside the scope of prev, in the body, input literals query the input DB, transport literals the incoming message, and state literals the new state DB under computation. In the head, transport atoms deduce the outgoing messages and state atoms the facts in the new state DB. At the end of the computation, the new state DB substitutes the previous one and the outgoing messages are sent on the channel. Transport consistency states that data from the input DB cannot directly flow to the channel. This matches with the assumption that only nodes have the power to send messages, which have to be preliminarily gathered in an out-bufer that contributes to the node configuration (state DB, possibly afecting its boundedness, cf. Def. 2.4). Note that state literals in the scope of prev and transport literals in the body are not involved in forming recursive dependencies. While this feature appears as a major diference with Datalog, actually, it is just a matter of making the syntax convenient for the CDP semantics. In fact, one can provide a Datalog encoding of a set of D2C rules where this diference is ironed out. Definition 2.3. A D2C program over a CDP signature Λ is a finite set of safe and transport consistent D2C rules s.t. is stratified. Given such Λ and , a CDP is a tuple pΛ , , 0, 0q, where 0 is a state DB denoting the initial state and 0 is an initial message. Ÿ
The semantics of CDPs is given in terms of configuration graphs, which connect CDP configurations via transitions. Each configuration p, , q describes a snapshot of the system, including the state DB , the input DB , and the channel , represented as a multiset. The configuration is -input, -state, or -channel bounded, for some , , P N, if the cardinality of the active domain of , of the active domain of , or of , is at most , , or , respectively. Definition 2.4. Given , , P N, we call -CDP a CDP interpreted under the configuration graph Υ consisting of all -input bounded configurations of . A -CDP is -state or channel bounded if all configurations reachable in Υ from an initial configuration are -state or -channel bounded, respectively.
We study the problem of formal verification of CDPs. Previous work [
Unfortunately, boundedness is a semantic property, undecidable to check. In addition, while
there are diferent techniques to enforce state boundedness [
In the following, we study the problem of model checking variants of uCDPs against selected fragments of CTLCDP. The base-level fragment we use to express reachability-like properties called EFp´, , q, essentially, mixes EF CTL temporal operators with closed FO formulas over the state signature. Specifically, given a CDP “ pΛ , , 0, 0q, where Λ “ p, ℐ, q, the language EFp´, , q over is defined by the rules Φ :: “ | EF | Φ ^ Φ | Φ _ Φ
::“ 1 “ 2 | ptq | D. | ^ | _ | ␣,
where Φ are temporal formulas, are closed FO formulas over , 1 and 2 are terms, and t is a
tuple (of proper size) of terms. Such formulas are interpreted as follows: ptq queries whether
ptq is in the current state DB; D is an existential quantifier over the active domain of the
state DB and the support of the multiset channel; and EF is interpreted as in standard CTL,
i.e., there exists a path, in the CDP configuration graph, on which eventually holds [
We study variants of reachability properties starting from EFp´, , q and considering formulae consisting of (positive boolean combinations of) sentences starting with an EF operator, tuning them along three dimensions: the available temporal operators beyond EF, the presence of negations in the FO queries, and which components they inspect (state DB or also channels)1. We identify such fragments with notation EFpl, △, ˝q, where: ‚ l indicates which temporal operators can be nested; it can be one of: – ´ (no nesting), as in the grammar above, – EF` (nesting of multiple EF), obtained by adding to the grammar rule Φ :: “ EFΦ , – AG (nesting of a single AG), obtained by adding to the grammar rule Φ :: “ EFAG , or 1Input DBs are disregarded since their evolution is completely non-deterministic and its interaction with the state DB can be captured by slightly modifying the CDP program so as to include the bounded input DB in the state DB. – pEF, AXq` (nesting of multiple EF and AX, possibly interleaved), obtained by adding to the grammar rule Φ :: “ EFΦ | AXΦ ; ‚ △ indicates how negation is supported by FO formulas; it can be either – , as defined by the grammar above, or – (no negation), obtained by dropping from the grammar rule ::“ ␣ ; ‚ ˝ indicates whether formulas can only query state DBs, or also channels; it can be either: – (queries only over node states), as defined by the grammar above, or – `ℎ (queries also over the support of channel multisets), obtained by adding to the grammar rule ::“ ptq, where is in the transport signature.
For the formal syntax and semantics of these languages, we refer to the full paper.
We study the following model-checking problem variants.
Problem 3.1 (EFrl, △, ˝s-MC). Let l P t´, EF`, AG, pEF, AXq`u, △ P t, u, and ˝ P t, `ℎu. The EFrl, △, ˝s-MC problem is defined as follows: Input: A P N, P N, -state bounded single-node uCDP , initial configuration 0, and closed formula Φ P EFpl, △, ˝q.
Output: Whether the configuration graph Υ satisfies Φ from 0. Ÿ
Verification w.r.t. all initial configurations reduces to finitely many instances of EFrl, △, ˝sMC. Indeed, due to state and input boundedness, the initial configurations are finitely many up to isomorphisms, and FO formulas are invariant under isomorphisms that fix the constants in them. Establishing the decidability status of the diferent variants of this problem is challenging, due to the subtle interplay of the CDP components, e.g., how the node state is afected by the content of the multiset channel, whose access is limited by aysnchronous communication. To attack this problem, we provide a bridge with models and techniques for the verification of data-aware extensions of PNs, in particular -PNs. PNs are one of the most widely studied models for concurrent computations, particularly suited to handle asynchronous threads and message passing. Specifically, -PNs lend themselves to be connected to uCDPs. In fact, tokens carrying single data elements match constants used in unary messages, and places match unary relation symbols - so that inserting a token carrying constant in a place naturally corresponds to having message Mpcq in the channel. What is not at all clear, instead, is how to encode in the -PN the infinitely many input and state DBs that may be encountered along a computation. Recall, in fact, that even under state-boundedness, a CDP can encounter infinitely many, genuinely distinct state DBs.
To address this issue, we represent state and input DBs up to isomorphism. This can be done by introducing dedicated places for the following purposes: (1) to encode the relation symbols of messages; (2) to represent the isomorphism types of bounded input and state DBs, over a ifxed representative bounded domain; (3) to specify a mapping from the representative domain to the infinite domain of data values used to form input and state DBs; (4) to deal with the special constants that are distinguished in the CDP program, ensuring that each one of those forms a singleton isomorphism type. This constitutes the basis for reducing EFrl, △, ˝s-MC problems over uCDPs, to coverability checks over -PNs.
We proceed as follows. We first investigate the decidability status of variants of control-state reachability for -PNs (Sec. 4). We then transfer these results to uCDPs, showing reductions from variants of uCDP model checking to -PNs control-state reachability (Sec. 5).
We introduce now the language - CTL to express coverability properties on -PNs and study the decidability of the related model-checking problem. - CTL features the CTL EF temporal operator, boolean conjunctions and disjunctions, and replaces propositions with markings interpreted, each on its own, up to isomorphisms.
Definition 4.1. Given a set of places, - CTL is the language of formulas defined by the following grammar, where the atomic - CTL formulas are markings over the place set : ::“ | ^ | _ | EF
The semantics of - CTL is defined as for CTL, with the provision that the current marking of a -PN satisfies an atomic formula 1, if covers, up to isomorphisms, 1. Problem 4.2 ( - CTL-MC). The - CTL-MC problem is defined as follows: Input: A -PN “ p, , q, marking 0, and - CTL formula .
Output: Whether satisfies from 0, denoted by , 0 |ù .
Since atomic formulas perform coverability checks, - CTL-MC can be reduced to plain -PN coverability. This is done by induction on the structure of the - CTL formula. First, a given formula , to be checked on a -PN and initial marking 0, is represented as a syntax tree. Its leafs are the occurrences of atomic formulas and the other nodes are obtained by applying to the children the corresponding boolean or temporal operator. Second, from leafs to the root, each node is mapped to a -PN and initial marking 0 where (1) the net contains, as sub-nets, the nets , for each sub-formula of , (2) contains the places check and cover , (3) 0 places at least a distinguished identifier on check , and (4) transitions are added so that the place cover can be marked with a distinguished identifier if , 0 |ù . The construction for non-leaves take into account the children nets and the semantics of the respective conjunction, disjunction, or EF operator, where the latter case is the most involved one. We refer to the full paper for the details.
From decidability of -PN coverability we obtain: Theorem 4.3. For each finite place set , - CTL-MC is decidable.
To reduce uCDP model checking to -PN model checking, we encode an arbitrary -state bounded -uCDP “ pΛ , , 0, 0q with Λ “ p, ℐ, q, into a -PN “ p, , q.
1. Configuration encoding. We use identifiers to represent the domain of DBs: ID “ ∆ Y t‚u. We use places of (and related markings) to encode configurations of , reorganized in the following way: (i) channel configuration, (ii) extension, up to isomorphisms, of the state and input DBs, over a fixed active domain of representative constants, (iii) mapping, via a partial function, of the representative constants to the represented state and input DB constants. 6. Conclusions 2. Step encoding. We use the transitions of to encode the steps of , organized as: (i) input update, and (ii) D2C computation, including message reception, casting, and state DB update.
3. Formula encoding. We encode a formula P EFpEF`, , q into - CTL. In the full paper, we show that it is enough to handle FO formulas. Since ranges only over the state signature, it is satisfied by any configuration p, , q s.t. |ù . Since is -state bounded, up to isomorphism there is only a finite set t1, . . . , u of state DBs satisfying . Thus, is equivalent to the disjunction of markings encoding the configurations p, H, Hq, for each P t1, . . . , u. Similarly, we can encode also formulas from EFpEF`, , `ℎq. In fact, since is positive, it can only assert the existence of a fixed number of tuples in the state or in the channel. Thus, because of state boundedness, up to isomorphisms and channel inclusion there is only a finite set tp1, H, 1q, . . . , p, H, qu of configurations satisfying . Thus, is equivalent to the disjunction of markings encoding the configurations p, H, q, for each P t1, . . . , u.
Theorem 5.1. EFrEF`, , s-MC and EFrEF`, , `ℎs-MC are decidable.
Theorem 5.1 is essentially tight, as shown by the next result.
Theorem 5.2. EFrAG, , s-MC, EFrAX2, , s-MC, and EFr´, , `ℎs-MC are undecidable.
We recap decidability (D) and undecidability (U) for EFrl, △, ˝s-MC on uCDPs: ´
D U
EF` D D
EF`
D U
AG U U
AX2
U
U
The properties refer to branching-time first-order properties verified over CDPs where nodes
asynchronously exchange messages with at most a unary signature, the state of each node
has a bounded size, while communication channels have unbounded capacity. Our results are
obtained by encoding such verification problems into corresponding coverability verification
problems over -PNs. In spite of the extremely high complexity in the analysis of such nets,
several efective techniques and tools for the (symbolic) exploration of their state space exist
(see, e.g., [
This research has been partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation, by the Province of Bolzano and DFG through the project D2G2 (DFG grant n. 500249124), and by the HEU project CyclOps (under GA n. 101135513). 1–10