We study the verification of coverability for Positive Interactive Datalog Programs (posIDP), a fragment of Communicating Datalog Programs (CDPs) where the programs are positive, i.e., make no use of negation. CDPs are a message passing system model grounded in logic programming, where nodes update their configuration by running a Datalog̸= program while sharing database tuples and receiving information from external services and/or users. While CDP verification has been extensively studied in the last few years, studies on CDP formal verification disregarded the role of negation in the node programs. In this paper, we study the impact on verification of positive programs when no meaningful use of negation is made. We show that the coverability problem remains undecidable despite the monotonicity of Datalog. We discuss the results in the framework of the Well Structured Transition System theory, motivating the introduction of novel semantics for data-aware processes that arguably enjoy better verification properties.
Communicating Datalog Programs (CDPs) are a model of distributed computation where computational
units run a data-aware process while sharing messages and receiving inputs from external
users/services [
These features make CDPs interesting in several areas. First, they are tightly related with, and
ofer new perspectives on, well studied computational models of communication and concurrency,
such as Communicating Finite State Machines [
Starting from [14], formal verification of CDPs has been extensively studied. CDP verification is
challenging, since interactivity and communication make CDPs infinite state systems. In general,
even simple problems, e.g., control-state reachability, are undecidable [15]. Nevertheless, several CDP
fragments enjoying decidability have been detected. For example, the constraint of data-boundedness,
where the capacity of the channels and the size of the active domains of the DBs involved in the
computation are bounded (even if still from an infinite domain), yields PSPACE-completeness for
CDPCTL [
In this paper, we further study the verification of CDPs, by considering the limited setting of singlenode CDPs running positive Datalog-like programs and using communication only as a mechanism for triggering computation steps (via a self-loop channel). Since, in this setting, communication is negligible and only interactivity is relevant, we call the resulting model Positive Interactive Datalog Programs (posIDP). posIDP appear promising for verification, since it is known that positive Datalog queries are monotone and, as a rule of thumb, monotonicity is related to better computational properties. In the area of verification, this principle is formalized by the theory of Well Structured Transition Systems (WSTS) [20], which provides general algorithms for the verification of properties like coverability on models that enjoy, among some other property, the notion of compatibility, which recasts monotonicity over transition systems. Despite the good properties of positive Datalog, we show that even the basic problem of coverability of propositional target configurations remains undecidable on posIDP. This motivates a discussion on why WSTS theory is not applicable on posIDP and, more in general, on data-aware processes. This leads to the proposal of new CDP semantics, arguably related to better verification properties. Our main technical contributions are undecidability results for posIDP coverability, irrespective of boundedness conditions on the information provided by external services. Moreover, we motivate and discuss a new conjecture about the decidability of a variant of coverability for posIDP whose semantics is based on the notion of graph-minor.
In Sec. 2 we provide preliminaries on WSTSs and 2CM. In Sec. 3 we define posIDP and the technical problem studied in the paper. In Sec. 4 we prove the undecidability results. In Sec. 5 we discuss why WSTS theory cannot be applied on posIDP and conjecture decidability for posIDP based on graph-minors. Finally, in Sec. 6, we draw the conclusions.
2.1. WSTS
Definition 1. A quasi-order (QO) ⪯ on a set is a reflexive and transitive binary relation on . The QO ⪯ is a WQO if, for each infinite sequence ()∈N over , there are , ∈ N such that < and ⪯ .
Given a QO ⪯ on , for each 1, 2 ∈ , we write 1 ≺ 2 if 1 ⪯ 2 and 1 ̸= 2, and write 2 ⪰ 1 (respectively 2 ≻ 1) if 1 ⪯ 2 (1 ≺ 2).
Definition 2. Given a QO ⪯ on , the up-ward closure ↑ of a subset ⊆ is the set { ∈ | ∃′ ∈ : ′ ⪯ }. The set is upward-closed if = ↑ . A base for an up-ward closed set is a set ′ ⊆ such that, for each ∈ , there is some ′ ∈ such that ′ ⪯ .
It is well-known that, under any WQO, each upward-closed set has a finite base [21]. Definition 3. A transition system (TS) is a pair = ⟨Conf, →⟩ where Conf is a (possibly infinite) set of configurations and → is a binary relation on Conf. We denote by →* the reflexive and transitive the following decision problem: Input Two configurations , ∈ Conf. is compatible with ⪯ . closure of →. Given a QO ⪯ on Conf, the TS is compatible (strongly compatible) with ⪯ if, for each 1, 2, 3 ∈ Conf such that 1 ⪰ 2 → 3, there is some 4 ∈ Conf such that 1 → * 4 ⪰ 3 (respectively 1 → 4 ⪰ 3). A WSTS is a tuple ⟨Conf, →, ⪯⟩
where ⟨Conf, →⟩ is a TS, ⪯ is a WQO over Conf, and
Given a TS = ⟨Conf, →⟩ and a QO ⪯ over Conf, the ⪯ -coverability problem for is Output Whether there is a configuration ∈ Conf such that →* ⪰ .
This problem is decidable if the WSTS enjoys a couple of efectiveness assumptions. Specifically, given a WSTS = ⟨Conf, →, ⪯⟩ and a set ⊆
such that, given 1, 2 ∈ , it decides whether 1 ⪯ 2. of configurations in , i.e., Pred( ) = { ∈ Conf | ∃′ ∈ : → ′}. We say that a WSTS has the Efective Pred-Basis (EPB) property if there is an algorithm such that, given a configuration , it returns a finite basis of ↑Pred(↑{}). Moreover, we say that a QO ⪯ over is decidable if there is an algorithm Theorem 1. The ⪯ -coverability problem is decidable for WSTSs ⟨Conf, →, ⪯⟩ with EPB and decidable ⪯ . 2.2. 2-Counter Machines A 2-Counter Machine (2CM), also called Minsky Machine, is a Finite State Automaton (FSA) whose transitions can handle two counters, by performing increments and conditional decrements. ifrst components of 1 and 2 are distinct.
A 2CM is a tuple = ⟨, Δ, , ⟩ where is a non-empty finite set of states, , ∈ , and Δ is a finite set of instructions such that, for each ∈ Δ, either = (, +, , ′), called increment transition, or = (, − , , ′, ′′), called conditional decrement transition, for some , ′, ′′ ∈ and ∈ {1, 2}.1 The 2CM is deterministic if, for each two transitions 1, 2 ∈ Δ, the 2CM configurations track the FSA state and the numbers in the counters.
The set Conf of configurations of a 2CM = ⟨, Δ, , ⟩ is the set × The transition system of is the directed graph (Conf, →) such that →= ⋃︀ 1, 2 ∈ , ∈ Δ, and ∈ {0, 1}, we have ⟨, 0, 1⟩ → ⟨′, ′0, ′2⟩ if ′1− = 1− and: ∈Δ → where, for each
N2. 1. = ⟨, +, , ′⟩, and ′ = + 1, 2. = ⟨, − , , ′, ′′⟩, > 0, and ′ = − 1, or 3. = ⟨, − , , ′′, ′⟩, and = 0 = ′. that is, once is reached, the computation terminates.
The 2CM termination problem asks, given a 2CM ⟨, Δ, , ⟩, whether → * . It is well known that termination of deterministic 2CM is undecidable [22]. We assume, without loss of generality that, for each 2CM = ⟨, Δ, , ⟩, there is no instruction in Δ with in its first component,
general CDPs in [
In this section we define posIDP. Because this CDP fragment features a single node, essentially no communication, and only positive programs, it enjoys the concise formalization below (cf. definition of 1The components of indicate, respectively: the state on which the transition fires; the type of the transition; the counter on which transition operates; the state reached after the increment or, if the counter is not zero, the decrement; the state reached after the decrement when the counter is zero. 3.1. Positive D2C D2C is a Datalog-like query language specialized to the distributed and interactive setting of CDPs. Here we define its positive fragment. We assume that the reader is familiar with Datalog and relational databases (see [23] for an introduction). We work with DBs over a fixed infinite domain Δ of constants and denote the active domain of a DB by Δ().
Given a relational signature = {1/1, . . . , /}, we work with pair-wise disjoint relational signatures = {1/1, . . . , /}, = {1/1, . . . , /}, and = {1/1, . . . , /} of fresh symbols. These are used to refer to facts stored in the current state of the node (), the previous state (), outgoing messages (), and incoming message (). We lift this notation also to DBs, i.e., given a DB over , , , or ), we denote by , , , the DB obtained by substituting each fact (a) of , where is either the empty string or ∈ {, , }, by the fact (a), (a), (a), or (a) respectively. Definition 7. A D2C signature is a tuple Λ = ⟨Δ, , ℐ, ⟩ where Δ ⊂ Δ is a finite set of constants, , ℐ, and are pair-wise disjoint signatures, called, respectively state, input, and channel signatures, and start/0 ∈ .
In this section, we work with a fixed signature Λ = ⟨Δ, , ℐ, {/0}⟩. A positive D2C (posD2C) rule is a Datalog (with inequalities) rule extended with dedicated symbols for sending messages (in the head), receiving messages and inputs (in the body), and querying the previous state (in the body). Let be an infinite set of variables.
Definition 8. A posD2C rule over Λ is a formula ‘ if 1, . . . , , 1, . . . , .’ where: 1. , called the head, is an FO atomic formula over , Δ, and ∪ , 2. 1, . . . , , called the body, is a sequence of FO atomic formulas over , Δ, and ∪ ∪ ∪ , 3. and 1, . . . , is a sequence of inequalities 1 ̸= 2 where 1, 2 ∈ Δ ∪ .
The rule is safe if each variable appearing in the head or in some inequality appears also in the body. A posD2C program over Λ is a finite set of posD2C rules over Λ.
Notation 1. Given FO formulas 1, . . . , over , Δ, and , we write prev {1, . . . , } to denote 1, . . . , . Moreover, we denote the set of rules {1 if ., . . . , if .} by ‘ 1; . . . ; if .’.
Since posD2C programs are special forms of Datalog programs, they inherit the Datalog semantics. The semantics of D2C is given as in Datalog, with the provision that D2C works over extensional DBs of a specialized form: it contains information about the previous state, the incoming input, and a single incoming message (i.e., a single tuple over the signature ).
Definition 9. Given a posD2C and DBs over , over , and {} over , the output (, , ) of over , , and is the DB computed according to Datalog semantics by ∪ ∪ ∪ {}).
In what follows, we are not interested in the D2C output as a whole, but as split into a state and a channel part, used as new previous state and new messages on the channel. Specifically, we denote: by state(, , , ) is the projection of (, , ) over ; by channel(, , , ) the DB where is the projection of (, , ) over . Since Datalog with inequalities is monotone, also posD2C programs are monotone: Lemma 1. Given a posD2C program and DBs 1 and 2 over , 1 and 2 over ℐ, and {} over such that 1 ⊆ 2, and 1 ⊆ 2, it is true that (1, 1, {}) ⊆ (2, 2, {}), state(, 1, 1, {}) ⊆ state(, 2, 2, {}), and channel(, 1, 1, {}) ⊆ channel(, 2, 2, {}).
It is immediate to see that D2C programs inherit also genericity of Datalog.
Definition 10. Given a finite set Δ ⊆ Δ, a Δ-isomorphism is a bijection : Δ →− Δ such that, for each ∈ Δ, () = . We say that a DB 1 is embedded in a DB 2 via a Δ-isomorphism , denoted 1 ⊑ 2, if (1) ⊆ 2. We write 1 ⊑ 2 if there is some such that 1 ⊑ 2. Lemma 2. Given a posD2C program , a Δ-isomorphism, DBs 1 and 2 over , 1 and 2 over ℐ, and {} over such that 1 ⊑ 2, and 1 ⊑ 2, it is true that (1, 1, {}) ⊑ (2, 2{}), state(, 1, 1, {}) ⊑ state(, 2, 2, {}), and channel(, 1, 1, {}) ⊑ channel(, 2, 2, {}). 3.2. PosIDP definition Syntactically, a posIDP is a computational node with a self-loop channel running a posD2C program where the only possible message is . This captures the case where the messages are used only as a triggering mechanism for the node computation, instead of a proper communication mechanism. Definition 11. A posIDP is a tuple = ⟨Λ, , 0⟩ where Λ = ⟨Δ, , ℐ, {}⟩, is a posD2C program over Λ, and 0, called initial state-DB, is a DB over with Δ() ⊆ Δ.
posIDP semantics is given in terms of configuration graphs. Diferent input policies (bounded and unbounded) amount to diferent graphs.
Definition 12. A configuration of a posIDP = ⟨Λ, , 0⟩ is a pair = ⟨, ⟩ where , called state-DB, is a DB over and is either {} or ∅. We denote the set of configurations of by Conf. The initial configuration of is ⟨0, {start}⟩.
The unbounded input semantics is obtained by feeding the program, at each step, with an arbitrary input DB next to a message coming from the channel. If the channel is empty, the computation stops. Definition 13. The input-unbounded configuration graph of a posIDP = ⟨Λ, , 0⟩ is the directed graph ϒ = ⟨Conf, →⟩ such that (1, 1) → (2, 2) if 1 = {} and there is a DB over ℐ such that 2 = state(, 1, , {}) and 2 = channel(, 1, , {})
For ∈ N, the -input bounded semantics is obtained by restricting input DBs containing at most constants.
Definition 14. For ∈ N, the -input-bounded configuration graph of a posIDP = ⟨Λ, , 0⟩ is the directed graph ϒ = ⟨Conf, →⟩ defined as in Def. 13 with the provision that is a DB over ℐ such |Δ()| ≤ .
Note that even under input-bounded semantics, while an infinite amount of data may still flow through the system. 3.3. PosIDP -coverability In this paper, we study the decidability of -coverability of posIDP. Technically, our study will focus on a simple target of the form { is propositional.
}, where Definition 15. Given < (respectively, = ), the -coverability problem for posIDP asks, given a posIDP and a coverability target DB over , whether there is a path in ϒ (ϒ) from the initial configuration to a configuration ⟨, ⟩ such that ⊆ .
These problems are interesting because, while arguably simple and classic, their variants over nonpositive single-node CDPs are undecidable.2 Thus, they are an excellent case study to check the impact of positive programs on the decidability of CDP verification. For example, undecidability of coverability problems for posIDP immediately returns undecidability for any model checking problem over the same or more expressive posIDP or CDP variant (e.g., with arbitrary node networks) based on languages capable of expressing coverability, such as the CDP-CTL fragments from [19]. Moreover, the next example shows that posIDP coverability can be used to check plan existence in some (simple, for the sake of brevity) planning domain.
2This is an immediate consequence of the proofs in [15]. 1 %Making facts persistent. 2 succ(X,Y) if succ(X,Y). 3 block(X) if block(X,Y). 4 5 %Making the posIDP non-terminating. 6 start if start. 7 8 %Alternating phases while updating the
step id. 9 phase(put) if prev{phase(pick), step(X)}. 10 phase(pick) if prev{phase(put), step(X)}. 11 step(X) if prev{step(X), phase(pick)}. 12 step(Y) if prev{step(X), succ(X,Y),
phase(put)}. 13 14 %Using the input to pick blocks. 15 picked(X) if select(X), block(X), prev{free(X), phase(pick)}. 16 free(Y) if picked(X), free(Y), X̸=Y. 17 free(Y) if picked(X), on(X,Y), Y̸=table. 18 on(Y,Z) if picked(X), prev{on(Y,Z),
phase(pick)}, X̸=Y. 19 20 %Using the input to put blocks. 21 picked(X) if prev{picked(X), phase(put)}. 22 putOn(X) if select(X), block(X),
prev{free(X), phase(put)}. 23 putOn(table) if select(table),
phase(put). 24 on(X,Y) if picked(X), putOn(Y). 25 on(X,Y) if prev{on(X,Y), phase(put)}. 26 free(X) if picked(X), phase(put). 27 free(Z) if on(X,Y), free(Z), Y̸=Z,
Z̸=table. 28 %Encode number n and
initialize step id. 29 succ(num0,num1).
. 30 .. 31 succ(num− 1,num). 32 33 %Encode initial block
configuration. 34 block(a). 35 block(b). 36 block(c). 37 on(a,table). 38 on(b,table). 39 on(c,table).
(a) (b) 40 free(a). 41 free(b). 42 free(c). 43 44 %Initialize step and phase. 45 step(num0). 46 phase(pick). Example 1. Consider a Block World problem where a robot has to stack the blocks , , and , so that sits on top of which, turn, sits on top of . The blocks are initially on a table. At each step the following actions can be performed: a block on a table or on top of a stack can be picked; the picked block can be put on the table or stacked on top of another block. At each moment, only one block can be picked.
For each ∈ N, we exhibit an instance of interactive 1-coverability that returns true if and only if a plan of at most actions for the Block World problem above exists. We work with a posIDP which non-deterministically attempts the computation of a plan. The program of is in Fig. 1a while the initial DB is in Fig. 1b. Note that the program makes no use of negation (beyond inequalities) and only rule 6 sends messages, specifically a single start message at each step after the consumption of the previous one. Thus, is posIDP.
The signature of is (Δ, , ℐ, ) where Δ is the set of constants appearing in the program or in the initial state-DB, ℐ = {/1}, = {start }, and is the set of all other relational symbols appearing in the program or initial state-DB. The number is encoded in the initial state DB as a path from the constant 0 to the constant through constants for ∈ N via the binary relation /2 ∈ . This encoding is made persistent by rule 2 in the program. The program alternates two phases: a pick phase and a put phase, signaled respectively by the facts phase(pick ) and phase(put ). A pair of consecutive pick and put phases constitutes a step. During the pick phases, lines 15 − 18 use the single constant, if any, in the input DB to select a free block, i.e., a block with no block on top of it. If the input provides a constant that does not match a block name, then no phase(put ) fact is deduced, stopping the non-deterministic computation of the plan. Similarly, during put phases, the program uses the input to select another free block, on which the previously picked block is stacked on. Again, if the input does not indicate a free block, the next phase does not happen. During these phases, the status of the blocks (whether they are free and where they sit) is encoded in the predicates free/1 and on/2 of . When the put phase of the -th step terminates, since there is no successor of the constant according to the extension of succ, no phase(pick ) fact is deduced, i.e., the next phase does not happen.
A plan exists if covers the target {(, ), (, ), (, )}. Moreover, we could have used the simpler target {} if we have added the rule ‘ if (, ), (, ), (, ).′ If desired, upon coverability, one can also obtain the computed plan by inspecting the extension of the additional relation action/3 ∈ whose dynamics is given by the following extra rules: 47 action(X,Y,Z) if action(X,Y,Z). 48 action(pick, X, Y) if picked(X), prev{step(Y)}. 49 action(put, X, Y) if put(X), prev{step(Y)}.
Note that, since rule 6 makes the posIDP non-terminating, at the cost of losing track of the actions, we can check existence of plans of arbitrary length by modifying the program by dropping the rules 11, 12, 47 − 49 and by removing the step-atoms from the bodies of rules 9 and 10. Alternatively, we can employ a strategy to initialize the encoding of an arbitrary natural number as in Sec. 4.1 below.
We now discuss undecidability of coverability for posIDP. We first consider 1-coverability, then coverability for each finite > 0, and finally -coverability. In each case, we provide a reduction from deterministic 2CM termination, which is undecidable. This is done in two steps. First, we show that the simulation of deterministic 2CM whose counters are known to be bounded by a natural number can be performed (even without using the input DB) by taking advantage of an encoding of natural numbers similar to the one in Ex. 1. Second, we exhibit a posIDP that initializes a non-deterministically chosen number . 4.1. 1-Coverability Definition 16. Given a ≤ , a 2CM is a -2CM if is the minimum ordinal such that, for each configuration ⟨, 1, 2⟩ reachable from the initial configuration of , 1 ≤ and 2 ≤ . Definition 17. Given a 2CM configuration = ⟨, 0, 1⟩ and a ≥ encoding of is the following DB, denoted by []: max{0, 1}, the -relational 1 succ(num0,num1).
. 2 .. 3 succ(num− 1,num). 4 min(num0). 5 q. 6 c0(num0 ).
7 c1(num1 ).
In Def. 17, facts 1− 3 encode the numbers 0, . . . , using constants num0, . . . , num. Fact 4 highlights that num0 behaves as zero. Facts 5 − 7 encode that the current state is and that the value of counter 0 (1) is 0 (1).
In what follows, we work with a fixed 2CM = ⟨, Δ, , ⟩. Given an ∈ N, we deifne a posIDP IDP () = ⟨Λ, 0, ⟩. The signature is Λ = (Δ, , ℐ, ) where Δ = {num0, . . . , num}, = {/0 | ∈ } ∪ {min/1, succ/2, 0/1, 1/1}, ℐ = ∅, and = {start /0}. The initial state DB 0 is the -relational encoding of the initial configuration of . The program contains the following rules: 1 start if start. 2 succ(X,Y) if succ(X,Y). 3 min(X) if min(X).
and, for each increment instruction ⟨, +, , ′⟩:
and, for each decrement instruction ⟨, − , , ′, ′′⟩: 7 c− 1(X) if prev{c1− (X), q}. 8 c(Y) if prev{c(X), succ(Y,X), q}. 9 q’ if prev{c(X), succ(Y,X), q}. 10 c(X) if prev{c(X), min(X), q}.
11 q’’ if prev{c(X), min(X), q}.
Note that does not afect the program, but only the initial state-DB. Rule 1 maintains the channel configuration, while rules 2 and 3 make the extension of succ and min persistent. At each step, the program simulates a 2CM transition . Rules 4 and 7 make sure that the encoding of the counter not involved in does not change. Rules 6 and 8 perform the increment and the decrement, if possible, i.e., if the current value of the updated counter has a successor or predecessor according to succ. Rule 10 makes sure that, if the decrement is not possible, i.e., the counter involved in is set to 0, then it is not changed. Rules 6, 9, and 11 update the state according to . Moreover, IDP () is deterministic, i.e., each configuration has at most a unique successor in the configuration graph. Thus, IDP () exhibits a single maximal computation run. The next lemmas capture the intuition that IDP () simulates along runs where the counters do not exceed . If the counters exceed , then the encoding breaks and the final state cannot be covered. · · · → ⟨ [], {start }⟩.
Lemma 3. Let ∈ N. If exhibits a run ⟨0, 0, 0⟩ = 0 → 1 1 → 2 · · · → where, for each ≤ , = ⟨, 0 , 1 ⟩ and 0 , 1 ≤ , then IDP () exhibits a run ⟨[0], {start }⟩ → ⟨[1], {start }⟩ → Proof. By induction on . If = 0, then the statement holds because the initial state-DB of IDP () is [0]. Let the statement hold for some ∈ N, and let exhibit a run 0 → 1 · · · → +1 +1 as in the statement. By induction, IDP () exhibits a non-maximal run ⟨[0], {start }⟩ → · · · → ⟨[], {start }⟩.
We assume, without loss of generality, that +1 operates on counter 0. If +1 is an increment instruction, then it has to be of the form ⟨, +, 0, ⟩ for some ∈ . Thus ≥ 0+1 = 0 + 1. Hence, succ( , +1) ∈ []. Consequently, There is only one instantiation that satisfies the bodies of the rules of type 4 − 6 for +1: the one binding with num and with +1 . Moreover, for each instruction in Δ, there is no binding that satisfies the bodies of rules 7 − 11. Thus, from ⟨[], {}⟩, the reception of the message start results in the configuration ⟨[+1], {}⟩.
If is a decrement instruction then the proof is analogous.
Lemma 4. If IDP () exhibits a run ⟨0, {}⟩ → · · · → ⟨ , {}⟩ → · · · → ⟨ , {}⟩ for some , ∈ N and ∩ = ∅, then, for each ≥ , ∩ = ∅.3 Proof. Each rule with some ′ ∈ in the head also has a in the body, for some ∈ .
Lemma 5. If is an -2CM, then does not terminate and IDP () does not 1-cover {}. Lemma 6. If is a -2CM for some ∈ N, then, for each < , IDP () does not 1-cover {}. Lemma 7. If is a -2CM for some ∈ N, then, for each ≥ , IDP () 1-covers {} if and only if terminates.
We now show that there is a 1-bounded posIDP IDP () such that, for each ∈ N, there is a ifnite maximal run that computes the initial state-DB of IDP (). If a maximal run does not initialize a IDP (), then it is infinite. Moreover, when we extend the program of IDP () with that of IDP (), we obtain a posIDP IDP () that covers {} if and only if terminates. The initial state-DB of IDP () is {charge, min(0)}. The program unfolds two phases, called charge and generate. the first one charges a unary relation . Each phase finishes when the input DB is {()}. 1 min(X) if min(X). 2 num(X) if prev{num(X), charge}. 3 charge; num(X) if I(X), charge, X̸=next. 4 generate if I(next), charge.
5 start if start, charge.
Rules 1 and 2 make and persistent during the phase. Rule 3 charges and maintains the phase. Rule 4 skips to the next phase. Note that the charge phase may run forever. However, if it ends, it ends with the state DB {(0), (1), . . . , (), }, for some constant 1, . . . , and ∈ N. Rule 5 makes the system reactive during this phase by sending a message on the channel at each step.
The second phase uses the input to pick and remove, one per step, constants from . The picked constant is used as the next successor, starting from num0. This ensures that the chain of successors does not contain repetitions. Again, the phase ends upon reception of {()}. In that case, the initial state of is deduced. 1 last(num0) if generate, charge. 2 succ(Y,X); last(X) if I(X), num(X),
last(Y), generate, X̸=next. 3 succ(X,Y) if succ(X,Y). 4 num(X) if I(Y), prev{generate, num(X)},
X̸=Y. 5 q0 if I(next), generate.
6 start if start, last(X), generate.
Rule 1 applies only when the phase shifts from charge to generate and marks 0 as the last constant in the (currently empty) chain of successors. Rule 2 applies only when the input is not triggering another phase shift: if the input provides a constant currently in , then the constant is added to the chain of successors and marked as the last one. Rule 3 makes persistent. Rule 4 makes a part of the extension of persistent. Specifically, only the constants not mentioned in the input are retained in . This way, when rule 2 adds a constant to the extension of , rule 4 implicitly removes it from . Rule 5 performs the phase shift. Rule 6 makes the system reactive up to the phase shift, as long as there is a fact involving . In fact, because of () in rule 6, if the input does not provide a constant in , then rule 2 gets inhibited, the extension of remains empty, rule 6 gets inhibited, and the computation stops.
Note that, at each step of the generate phase, either IDP () terminates or it removes a constant from . Since the extension of is finite and no rule puts back constants in , IDP () always terminates. Summarising, the generate phase has the following two behaviors, where a configuration ⟨, {}⟩ of IDP () is valid if is isomorphic to the initial state DB of a IDP (), for some ∈ N: 1. If, during the computation, the input DB is always of the form () for some constant currently in the extension of , except for the last step, where the input DB is {()}, then IDP () terminates in a valid configuration. 2. If the empty input DB or an input DB providing a constant not currently in is eventually received, then IDP () terminates in a non-valid configuration.
Moreover, for each ∈ N there is at least one run of IDP () that terminates in a valid configuration.
Let IDP () be the posIDP obtained by extending the program of the IDP () posIDP. If is a -2CM, IDP () exhibits the following maximal runs: 1. Infinite runs never leaving the charge phase of IDP (). Theorem 2. For each deterministic 2CM , terminates if and only if IDP () 1-covers {}.
Since deterministic 2CM termination is undecidable and IDP () is a posIDP, we obtain the following result.
Corollary 1. 1-coverability of posIDP is undecidable. 4.2. -Coverability for Finite If ∈ N and > 1, the above construction does not immediately work for -coverability. In fact, the reception of input DBs containing more than one constant may interfere with the generation of the chain of successors, resulting in constants with more than one immediate successor. However, as long as is finite, we can fix the above construction so that: 1. If an input DB does not provide the constants ℎ1, . . . , ℎ− 1 plus another arbitrary constant, then no rule body is satisfied, resulting in an empty DB and terminating the computation. 2. Otherwise, all the ℎ constants are ignored.
This can be achieved by: 1. adding an atom to all the rules in the program of IDP (), 2. for each rule using variables 1, . . . , , adding the inequalities ̸= ℎ , for ≤ and ≤ − 1, 3. adding the rule ‘ if (ℎ1), . . . , (ℎ− 1), (), ̸= ℎ1, . . . , ̸= ℎ− 1.’.
The resulting posIDP, interpreted under the -input bounded semantics, behaves as a IDP () interpreted under the 1-input bounded semantics, with the provision that the reception of the empty input DB results in termination with configuration ⟨∅, ∅⟩. Thus, all the previous lemmas and theorems apply also for -coverability, yielding the next generalization of Cor. 1 Corollary 2. For each ∈ N, -coverability of posIDP is undecidable. 4.3. -Coverability When we consider unbounded inputs, the solution in the previous section does not work. However, we can still show undecidability by modifying the way we encode numbers. Specifically, instead of using the relation to induce a chain of successors, we use it to capture a less demanding partial order, as depicted in Fig. 2, and defined next.
Definition 18. For each ∈ N, a relational encoding [] of is any DB defined inductively as follows: 1. if = 0, then [] = {(00)}. 2. if > 0, then [] extends [ − 1] with the following set of facts, for some ∈ N and for each ∈ N such that − 1 is in a constant in [ − 1]: 1 succ(num− 1,num0).
. 2 ..
3 succ(num− 1,num).
We can now update the encodings for 2CM configurations.
0
0 1
1 3 (a) 2 00
0 01 11 21 (b) 02 12
1 03 13
Definition 19. Given ∈ N, a relational encoding [] of , and a configuration = ⟨, 0, 1⟩ where 0, 1 ≤ , the []-relational encoding of is the DB [] ∪ {} ∪ {( ) | ∈ {0, 1} and ∈ Δ([])}, where Δ([]) is the active domain of [].
We now define IDP []() as IDP (), with the provision that the initial state DB is the []relational encoding of the initial configuration of . Note that Lemma 3 still applies with an analogous proof: instead of working with single facts (, +1), we just have to work with several facts (, +1). Lemma 4 immediately applies. Consequently, Lemma 5, Lemma 6, and Lemma 7 hold too. Interestingly, when IDP () is exposed to unbounded input DBs, its behavior remains as in Sec. 4.1, with the provision that instead of initializing -relational encodings, it initializes []-relational encodings. Specifically, during the charge phase, at each step all the constants in the input DB diferent from are internalized as part of ; the phase shift happens again when the input contains the constant ; during the generate phase, at each step, the input DB instructs the node to move several constants from to , resulting in a []-relational encoding for some . As before, only if the input DB does not contain any constant, the empty state DB is reached and the computation stops before initializing some IDP []().
Note that in this construction we did not modify the program or initial state-DB of IDP (). Thus, overall, we can use -coverability of IDP () to check termination of , even if adopting a diferent encoding. Thus, we obtain the following corollary.
Corollary 3. For each ∈ N, -coverability of posIDP is undecidable.
The undecidability of posIDP coverability, despite the monotonicity of posD2C, may appear surprising. However, the result is consistent with the insights provided by WSTS theory. In fact, the quasi-order used to define coverability, i.e., inclusion among DBs, is not a WQO among posIDP configurations. The next example provides a counter-example involving unary relations.
Example 2. The sequence { (1)}, { (2), { (3)}, . . . for pairwise distinct constants 1, 2, . . . shows that inclusion of DBs over unary signatures is not a WQO. In fact, for each , ∈ N, either = or { ()} ̸⊆ { ( )}.
An issue analogous to that in Ex. 2 afects also coverability problems in related models, such as data
Petri Nets [
Example 3. For each > 0, let = {(0, 1), . . . , (− 1, )} be a DB encoding a cyclic graph of length , for some pair-wise distinct constants 1, . . . , . The sequence 1, 2, 3, . . . shows that inclusion up to isomorphisms of DBs over binary signatures is not a WQO. In fact, for each ∈ N, is a cycle of length , each isomorphic copy of is a cycle of length , but does not contain any cycle of length .
Ex. 3 highlights that, in order to apply WSTS theory to posIDP, we have to focus on coverability problems with respect to a quasi-order ⪯ among DBs such that ⪯ is WQO also over relational encodings of directed graphs. Thus, essentially, ⪯ has to capture a WQO among digraphs. Unfortunately, to the best of our knowledge, there are only few known WQOs among families of graphs and essentially only one among graphs in general, i.e., the graph-minor order [24]. Specifically, a graph is a minor of a graph if can be obtained, up to a isomorphisms, from by a sequence of vertex deletions, edge deletions, and edge contractions. The graph-minor relation can be used as a WQO also among directed graphs, when one forgets the direction of the edges, i.e., it works on their underlying graphs: given two directed graph and , is a minor of if the underlying graph of is a minor of the underlying graph of . When interpreting this order in the DB setting, the contraction of paths from vertex to amounts to the weak reachability of a constant from constant via a chain of pairs in a binary relation. Motivated by this insight, we propose the following quasi-order among DBs over at most binary signatures, which combines inclusion for propositions, inclusion up to isomorphisms for unary facts, and a contraction relation for binary facts.
minor relation over , 1 ⪯ ⪯ 2 if and only if: Let be a signature of at most binary symbols and a permutation of Δ. The (, ) is the binary relation among DBs over such that, for each two DBs 1 and 2 1. for each propositional symbol /0 ∈ , if ∈ 1 then ∈ 2. 2. for each unary symbol /1 ∈ and constant , if () ∈ 1, then ( ()) ∈ 2. 3. for each binary symbol /2 ∈ and two constants and , if (, ) ∈ 1, then there is a sequence 0, . . . , of constants such that, 0 = () and = () and, for each < , (, +1) ∈ 2 or (+1, ) ∈ 2.
The -minor ⪯ is the union of all the ⪯ the union of all the ⪯ for all at most binary signatures .
for all the permutations of Δ. The DB-minor relation ⪯ is (1) ̸⪯ (2). respect to ⪯ , as shown in the next example.
In item 3 we require that precedes +1 in 2 or vice-versa. This is because we are capturing a WQO that works on top of the underlying graphs of the directed graphs encoded by the DBs. Because of the above arguments, we conjecture that ⪯ is a WQO among DBs. However, irrespectively of the WQO status of ⪯ , the reductions in Sec. 4 apply also to coverability problems defined in terms of ⪯ . In fact, in those reduction, we considered the coverability of propositional flags, on which ⊆ and ⪯ coincide. Thus, WSTS theory cannot be applied to posIDP even for coverability problems based on ⪯ (otherwise decidability would apply). One reason for that is that posIDP are not compatible with ⪯ . In other words, posIDP (and Datalog with inequalities) is monotone with respect to ⊆ but not with Example 4. Consider the one-rule program = { if (, ), (), ().} and the DBs 1 = {(, ), (), ()} and 2 = {(, ), (, ), (), ()}. While 1 ⊆ 2,
Consequently, we argue that the only way to apply WSTS theory to posIDP requires not only to
consider coverability based on ⪯ , but also to modify the semantics of posD2C, and more precisely of Datalog, so as to avoid counter-examples such as Ex. 4. We call this semantic the DB-minor Datalog semantics. Technically, it coincides with the standard semantics of Datalog with the provision that a fact (, ) is true in a DB if {(, )} ⪯
, instead of the traditional (, ) ∈ or, equivalently, {(, )} ⊆
. We call ⪯ -posIDP the variant of posIDP defined on top of DB-minor Datalog semantics. Conjecture 1. The DB-minor Datalog semantics and ⪯ -posIDP are well defined. Moreover, ⪯ is a WQO compatible with ⪯ -posIDP and with efective pred-basis property, irrespectively of the bounds on the input DBs.
By WSTS theory, a positive answer to the conjecture would immediately return decidability for ⪯ -posIDP coverability problems based on ⪯ .
We have studied the coverability problem for posIDP under bounded and unbounded input semantics. In all cases, we have obtained that coverability is undecidable. When compared to previous results [15, 18], these results indicate that the positivity of programs is irrelevant on the decidability of CDPs. We also investigated, from the perspective of WSTSs, why the monotonicity of Datalog is not enough to yield decidability for the restricted model of posIDP. The obtained insights motivated us to propose a semantics for Datalog and, more in general, posIDP and CDPs, based on the notion of graph-minor. This graph-minor semantics essentially closes each binary relation by reflexivity and transitivity.
As future works, we aim at proving Conjecture 1 and to study the actual expressiveness and practicality of Datalog-like languages and data-aware processes whose semantics is based on graph-minors or on other WQOs among DBs.
Operating Systems Principles 2005, SOSP 2005, Brighton, UK, October 23-26, 2005, ACM, 2005, pp. 75–90. doi:10.1145/1095810.1095818. [11] J. Su, L. Wen, J. Yang, From data-centric business processes to enterprise process frameworks, in: S. Hallé, R. Villemaire, R. Lagerström (Eds.), 21st IEEE International Enterprise Distributed Object Computing Conference, EDOC 2017, Quebec City, QC, Canada, October 10-13, 2017, IEEE Computer Society, 2017, pp. 1–9. doi:10.1109/EDOC.2017.11. [12] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Multi-shot ASP solving with clingo, Theory
Pract. Log. Program. 19 (2019) 27–82. doi:10.1017/S1471068418000054. [13] P. Cabalar, R. Kaminski, P. Morkisch, T. Schaub, telingo = ASP + time, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Logic Programming and Nonmonotonic Reasoning - 15th International Conference, LPNMR 2019, Philadelphia, PA, USA, June 3-7, 2019, Proceedings, volume 11481 of Lecture Notes in Computer Science, Springer, 2019, pp. 256–269. doi:10.1007/978-3-030-20528-7\_19. [14] D. Calvanese, M. Montali, J. Lobo, Verification of fixed-topology declarative distributed systems with external data, in: D. Olteanu, B. Poblete (Eds.), Proceedings of the 12th Alberto Mendelzon International Workshop on Foundations of Data Management, Cali, Colombia, May 21-25, 2018, volume 2100 of CEUR Workshop Proceedings, CEUR-WS.org, 2018. [15] D. Calvanese, F. Di Cosmo, J. Lobo, M. Montali, Convergence verification of declarative distributed systems, in: S. Monica, F. Bergenti (Eds.), Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021, volume 3002 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp. 62–76. [16] B. B. Hariri, D. Calvanese, G. D. Giacomo, A. Deutsch, M. Montali, Verification of relational datacentric dynamic systems with external services, in: R. Hull, W. Fan (Eds.), Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, NY, USA - June 22 - 27, 2013, ACM, 2013, pp. 163–174. doi:10.1145/2463664.2465221. [17] F. Di Cosmo, Verification of prev-free communicating datalog programs, in: A. Dovier, A. Formisano (Eds.), Proceedings of the 38th Italian Conference on Computational Logic, Udine, Italy, June 21-23, 2023, volume 3428 of CEUR Workshop Proceedings, CEUR-WS.org, 2023. [18] F. D. Cosmo, Analyzing termination for prev-aware fragments of communicating datalog programs, in: A. Fensel, A. Ozaki, D. Roman, A. Soylu (Eds.), Rules and Reasoning - 7th International Joint Conference, RuleML+RR 2023, Oslo, Norway, September 18-20, 2023, Proceedings, volume 14244 of Lecture Notes in Computer Science, Springer, 2023, pp. 110–125. doi:10.1007/978-3-031-45072-3\_8. [19] C. Aiswarya, D. Calvanese, F. D. Cosmo, M. Montali, Verification of unary communicating datalog programs, Proc. ACM Manag. Data 2 (2024) 89. doi:10.1145/3651590. [20] A. Finkel, P. Schnoebelen, Well-structured transition systems everywhere!, Theor. Comput. Sci.
256 (2001) 63–92. doi:10.1016/S0304-3975(00)00102-X. [21] G. Higman, Ordering by divisibility in abstract algebras, Proceedings of the London Mathematical
Society 3 (1952) 326–336. [22] M. L. Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, 1967. [23] S. Abiteboul, R. Hull, V. Vianu, Foundations of Databases, Addison-Wesley, 1995. URL: http: //webdam.inria.fr/Alice/. [24] R. Diestel, Graph Minors, Springer Berlin Heidelberg, Berlin, Heidelberg, 2025, pp. 363–416.