Verification of Unary Communicating Datalog Programs (Discussion Paper) C. Aiswarya1 , Diego Calvanese2,3,˚ , Francesco Di Cosmo2 and Marco Montali2 1 Chennai Mathematical Institute, Chennai, India 2 Free University of Bozen-Bolzano, Bolzano, Italy 3 Umeå University, Umeå, Sweden Abstract 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). Keywords Formal verification, Data-aware processes, Communicating Datalog Programs, Distributed computation, CTL-FO 1. Introduction Declarative approaches to the specification of distributed data-aware systems have been ex- tensively studied in many different contexts [1, 2, 3, 4, 5]. These approaches share the general idea that the overall behavior of the system emerges from the interaction of a number of local components (hereafter called nodes), mutually connected in a given topology, each running a declarative program that describes at once the input/output behavior to exchange messages with the other nodes, and the update of the node internal state. Both the state and the exchanged mes- sages are relational, thus making the overall system a distributed version of so-called data-aware SEBD 2024: 32nd Symposium on Advanced Database Systems, June 23–26, 2024, Villasimius, Sardinia, Italy ˚ Corresponding author. $ aiswarya@cmi.ac.in (C. Aiswarya); diego.calvanese@unibz.ir (D. Calvanese); francesco.dicosmo@unibz.it (F. Di Cosmo); marco.montali@unibz.it (M. Montali)  0000-0002-4878-7581 (C. Aiswarya); 0000-0001-5174-9693 (D. Calvanese); 0000-0002-5692-5681 (F. Di Cosmo); 0000-0002-8021-3430 (M. Montali) © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 1 CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings C. Aiswarya et al. CEUR Workshop Proceedings 1–10 processes, extensively studied within the foundations of data management from the modelling and static analysis point of view [6, 7, 8, 9, 10]. In this work, we are interested in the static analysis of such distributed declarative data- aware processes, in the style of [6, 7, 8]. We focus in particular on the D2C language originally introduced in [4], which employs a suitably extended version of Datalog equipped with commu- nication primitives and the possibility of referring to the previous and current node state. On top of the resulting model of what we call Communicating Datalog Programs (CDPs), two aspects become particularly important in the light of static analysis: (i) the presence of communication channels with different properties on faithfulness and ordering; (ii) the distinction between closed systems where new data are never created, but only the data present in the initial node states can be used and exchanged, and interactive systems where new data can be acquired and exchanged during the computation. 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 [11]. Such systems are infinite-state, with the consequence that even for very simple reachability properties, static analysis is un- decidable [11]. Decidable subclasses have been singled out by importing and adapting the notion of state-boundedness originally introduced in [12, 13, 14], and applied in [13, 15, 16] to obtain decidability of verification of data-aware processes against rich variants of first-order branching-time temporal logics. In a state-bounded system, infinitely many objects may be seen within and across runs of the system, but in each single configuration reached during the computation, their number remains bounded. In the context of CDPs, this notion has a twofold effect: it essentially bounds the number of constants that can be simultaneously stored in each node state, as well as the size of each communication channel. Under such restrictions, it has been shown that model checking first-order CTL properties is decidable [11]. 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, [11] has shown that even propositional reachability is undecidable to check over severely restricted CDPs that employ messages with a binary signature. We consequently focus on the verification of unary CDPs, i.e., CDPs where the messages range over a signature of at most unary relational symbols, and while the local memory and interaction with external services is bounded, the channel capacity is not. This is also interesting to study in the light of multiset channels, since adopting queues, as in [9, 10], would immediately yield undecidability for unary, unbounded channels. We show that the resulting model is still powerful enough to model real-case scenarios, and engage in a fine-grained study of CDP verification against variants of reachability, expressed as fragments of first-order CTL. Specifically, we establish an equivalence between this problem and that of verifying coverability over a variant of Petri nets with unordered data [17], a property that is decidable to check despite the fact that these nets are essentially infinite-state. This yields decidability for positive nested reachability queries over unary CDPs, even in the case where the logic has not only the ability of querying the states, but also that of inspecting communication channels. We finally investigate the tightness of our decidability results, showing that minor generalizations fall back into undecidability. 2 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 2. The CDP Model In this section, we informally introduce the CDP model by Ma et al. [4]. However, for simplicity, we formalize only the fragment relevant for our study, which is the one over unordered channels, non-deterministic bounded inputs, and single-node networks. 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 Datalog- like 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 [11] for a non-deterministic extension of D2C). However, in this paper, we focus on a simple D2C fragment, specialized for single-node networks. In fact, while inconvenient for modelling, single-node CDPs are enough for the technical study of verification of CDPs employing unordered channels, since each such CDP can be encoded over a single node network. 2.1. Single-node CDPs We now formalize bounded-interactive, single-node CDPs. With a slight abuse, we refer to this fragment as, simply, CDPs and ignore all other CDP variants (see [11] for the full model). 3 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 Definition 2.1. A CDP signature is a tuple Λ “ p𝒮, ℐ, 𝒯 q, where 𝒮, ℐ, and 𝒯 are pairwise disjoint relational signatures, respectively called state, input, and transport. A state, input, or transport atom (resp., literal) is an atom (resp., literal) over 𝒮, ℐ, or 𝒯 , respectively. Ÿ CDP programs are, syntactically, reminiscent of stratified Datalog with negation and inequality. Definition 2.2. 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-buffer that contributes to the node configuration (state DB, possibly affecting 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 difference 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 difference 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 , 𝑚0 q, 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. Ÿ 4 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 3. The Verification Problem for CDPs We study the problem of formal verification of CDPs. Previous work [11] showed that control- state reachability (that is, whether there is an initial configuration from which the target state DB is reachable — ignoring the configuration of the channel) is undecidable even for restricted CDPs that (i) have a single-node network, (ii) use the channel solely to (re)activate the node, and (iii) employ a unary state signature. Decidability can be gained by imposing boundedness conditions on the various CDP data sources [11]. In fact, for state- and channel-bounded CDPs, decidability holds for temporal model checking againts formulae in CTLCDP , a branching-time logic mixing CTL operators to analyze the system evolution, and FOL to query the data sources. Unfortunately, boundedness is a semantic property, undecidable to check. In addition, while there are different techniques to enforce state boundedness [14, 18], the same does not hold for channels. Furthermore, as pointed out in the introduction, imposing boundedness is particularly restrictive for communication channels. Interestingly, while undecidability of control-state reachability over state-unbounded CDPs already holds for unary signatures, in the case of CDPs with bounded states and unbounded channels it has been proved only for binary transport signatures [11]. This makes CDPs that are state- and input-bounded, but operate over unbounded channels carrying unary messages, worth investigating. We call such CDPs unary CDPs (uCDPs). 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 , 𝑚0 q, 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 [19]. For example, reachability of a state DB containing the fact 𝑆paq is expressed by the formula EF𝑆paq, while reachability of the state that contains only that fact by EFp𝑆paq ^ ␣D𝑥.𝑆p𝑥q ^ ␣𝑥 “ aq. 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 1 Input 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. 5 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 – 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, △, ˝s- MC. 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 different variants of this problem is challenging, due to the subtle interplay of the CDP components, e.g., how the node state is affected 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 fixed 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). 6 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 4. 𝜌-PN Verification 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 iff 𝑁 𝜓 , 𝑀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. 5. uCDP Model Checking To reduce uCDP model checking to 𝜌-PN model checking, we encode an arbitrary 𝑠-state bounded 𝑏-uCDP 𝐷 “ pΛ, 𝒫, 𝑆0 , 𝑚0 q 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. 7 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 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 t𝑆1 , . . . , 𝑆𝑘 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 tp𝑆1 , H, 𝐶1 q, . . . , 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 un- decidable. 6. Conclusions We recap decidability (D) and undecidability (U) for EFrl, △, ˝s-MC on uCDPs: l ´ ´ EF` EF` AG AX2 ˝ △ 𝑝𝑜𝑠 𝑏𝑜𝑜𝑙 𝑝𝑜𝑠 𝑏𝑜𝑜𝑙 𝑝𝑜𝑠 𝑝𝑜𝑠 𝑠𝑡 D D D D U U 𝑠𝑡`𝑐ℎ D U D U 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 effective techniques and tools for the (symbolic) exploration of their state space exist (see, e.g., [20, 21]). Our work consequently paves the way towards the application of such techniques to the practical analysis of declarative distributed systems. Acknowledgments 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). 8 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 References [1] J. M. Hellerstein, The declarative imperative: Experiences and conjectures in distributed logic, SIGMOD Record 39 (2010) 5–19. doi:10.1145/1860702.1860704. [2] P. Alvaro, T. J. Ameloot, J. M. Hellerstein, W. Marczak, J. Van den Bussche, A Declarative Semantics for Dedalus, Technical Report UCB/EECS-2011-120, EECS Department, Univer- sity of California, Berkeley, 2011. URL: http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/ EECS-2011-120.html. [3] T. J. Ameloot, J. Van den Bussche, Positive Dedalus programs tolerate non-causality, J. of Computer and System Sciences 80 (2014) 1191–1213. doi:10.1016/j.jcss.2014.01. 005. [4] J. Ma, F. Le, A. Russo, J. Lobo, Declarative framework for specification, simulation and analysis of distributed applications, IEEE Trans. on Knowledge and Data Engineering 28 (2016) 1489–1502. doi:10.1109/TKDE.2016.2515604. [5] S. Abiteboul, É. Antoine, G. Miklau, J. Stoyanovich, J. Testard, Rule-based application development using Webdamlog, in: Proc. of the 34th ACM Int. Conf. on Management of Data (SIGMOD), ACM, 2013, pp. 965–968. doi:10.1145/2463676.2465251. [6] V. Vianu, Automatic verification of database-driven systems: a new frontier, in: Proc. of the 12th Int. Conf. on Database Theory (ICDT), 2009, pp. 1–13. doi:10.1145/1514894. 1514896. [7] D. Calvanese, G. De Giacomo, M. Montali, Foundations of data-aware process analysis: a database theory perspective, in: Proc. of the 32nd ACM Symp. on Principles of Database Systems (PODS), ACM, 2013, pp. 1–12. doi:10.1145/2463664.2467796. [8] A. Deutsch, R. Hull, Y. Li, V. Vianu, Automatic verification of database-centric systems, ACM SIGLOG News 5 (2018) 37–56. doi:10.1145/3212019.3212025. [9] A. Deutsch, L. Sui, V. Vianu, D. Zhou, Verification of communicating data-driven web services, in: Proc. of the 25th ACM Symp. on Principles of Database Systems (PODS), 2006, pp. 90–99. doi:10.1145/1142351.1142364. [10] A. Deutsch, L. Sui, V. Vianu, Specification and verification of data-driven web applications, J. of Computer and System Sciences 73 (2007) 442–474. doi:10.1016/J.JCSS.2006.10. 006. [11] D. Calvanese, F. Di Cosmo, J. Lobo, M. Montali, Convergence verification of declarative distributed systems, in: Proc. of the 36th Italian Conf. on Computational Logic (CILC), volume 3002 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp. 62–76. [12] F. Belardinelli, A. Lomuscio, F. Patrizi, Verification of deployed artifact systems via data abstraction, in: Proc. of the 9th Int. Joint Conf. on Service Oriented Computing (ICSOC), volume 7084 of Lecture Notes in Computer Science, Springer, 2011, pp. 142–156. doi:10.1007/978-3-642-25535-9_10. [13] B. Bagheri Hariri, D. Calvanese, G. De Giacomo, A. Deutsch, M. Montali, Verification of relational data-centric dynamic systems with external services, in: Proc. of the 32nd ACM Symp. on Principles of Database Systems (PODS), 2013, pp. 163–174. doi:10.1145/ 2463664.2465221. [14] B. Bagheri Hariri, D. Calvanese, M. Montali, A. Deutsch, State-boundedness in data-aware dynamic systems, in: Proc. of the 14th Int. Conf. on Principles of Knowledge Representation 9 C. Aiswarya et al. CEUR Workshop Proceedings 1–10 and Reasoning (KR), AAAI Press, 2014, pp. 458–467. [15] G. De Giacomo, Y. Lespérance, F. Patrizi, Bounded Situation Calculus action theories, Artificial Intelligence 237 (2016) 172–203. doi:10.1016/j.artint.2016.04.006. [16] D. Calvanese, G. De Giacomo, M. Montali, F. Patrizi, First-order mu-calculus over generic transition systems and applications to the Situation Calculus, Information and Computation 259 (2018) 328–347. doi:10.1016/j.ic.2017.08.007. [17] F. Rosa-Velardo, Ordinal recursive complexity of Unordered Data Nets, Information and Computation 254 (2017) 41–58. doi:10.1016/J.IC.2017.02.002. [18] D. Solomakhin, M. Montali, S. Tessaris, R. De Masellis, Verification of artifact-centric systems: Decidability and modeling issues, in: Proc. of the 11th Int. Joint Conf. on Service Oriented Computing (ICSOC), volume 8274 of Lecture Notes in Computer Science, Springer, 2013, pp. 252–266. doi:10.1007/978-3-642-45005-1_18. [19] C. Baier, J.-P. Katoen, Principles of Model Checking, The MIT Press, 2008. [20] M. Westergaard, S. Evangelista, L. M. Kristensen, ASAP: an extensible platform for state space analysis, in: Proc. of the 30th Int. Conf. on Application and Theory of Petri Nets (PETRI NETS), volume 5606 of Lecture Notes in Computer Science, Springer, 2009, pp. 303–312. doi:10.1007/978-3-642-02424-5_18. [21] S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Petri net-based object-centric processes with read-only data, Information Systems 107 (2022) 102011. doi:10.1016/J.IS.2022. 102011. 10