External Transaction Logic: reasoning and executing transactions involving external domains

Tracking #: 655-1865

Ana Sofia Gomes
José Júlio Alferes

Responsible editor: 
Guest Editors RR2013 Special Issue

Submission type: 
Full Paper
In this work we present External Transaction Logic, a logic that extends Transaction logic with the ability to model and execute transactions requiring interactions with external entities, as e.g. external web-source, web-services or agents. Transactions are defined in a logic programming style by the composition of internal and external primitives. These primitives are incorporated in a quite general manner, as a parameter of the External Transaction Logic theory, allowing the specification of transactions integrating knowledge and actions from multiple sources and semantics. Since one has different control over internal and external domains, different transaction properties are ensured depending on where actions are executed. Namely, internal actions executed in a knowledge base that we fully control, follow the standard model of transactions, where the failure of the transaction leaves the knowledge unaffected. On the other hand, transactional properties over actions executed externally need to be relaxed, as it is impossible to roll back actions executed in a domain that is external. To deal with this, external actions can be defined along with compensating operations. If a transaction fails after executing some external action, then these compensations are executed in a backward order to achieve a relaxed model of atomicity. We provide a model theory for External Transaction Logic, that can be used to reason about the conditions of execution of transactions that require the issuing of both internal and external actions on abstract knowledge bases with potentially different state semantics. We also present here a corresponding proof theory (sound and complete w.r.t. the model theory) that provides means to execute such transactions in a top-down manner.
Full PDF Version: 


Solicited Reviews:
Click to Expand/Collapse
Review #1
Anonymous submitted on 21/May/2014
Review Comment:

Referee report on resubmission of paper entitled:

"External Transaction Logic: reasoning and executing transactions involving external domains"

by Ana Sofia Gomes and Jose Julio Alferes

The present submission reports on the definition of a logical framework called External Transaction Logic (ETR), an extension of Transaction Logic dealing with the presence of external actions. The authors motivate and point out the limitations of standard Transaction Logic and propose ETR as a conservative extension thereof with which one can represent and reason with external actions, i.e., actions that take place on external domains and resources, a challenging problem for existing frameworks.

The main feature of ETR is that it allows for both reasoning about and executing actions that are performed in both internal and external knowledge bases. In particular, ETR allows for a simple yet elegant formalization and execution of rolling back actions performed in external knowledge bases (external actions that have failed and therefore have to be rolled back as though nothing had happened).

The main contributions of the paper can be summarized as follows: (i) the definition of a proper extension of the logic TR with an intuitive semantics; (ii) the provision of a proof procedure for ETR that is shown to be sound and complete with respect to the given semantics, and (iii) an assessment of several action formalisms as the component for specifying action effects. In particular, the authors show that in the absence of external transactions, both logics ETR and TR coincide.

The paper addresses a topic that is interesting on its own right, but that is also relevant to a class of different yet interrelated communities such as knowledge representation and reasoning, business processes modeling, semantic web and logic programming, to mention but a few. Overall the paper looks good, the contributions interesting, the results are significant and the examples insightful. As far as I could check, all authors' claims and technical results are correct.

I had several remarks on the original submission, which have been satisfactorily handled in both the re-submitted version and in the accompanying cover letter. I therefore recommend acceptance of this manuscript for publication in the Semantic Web Journal in its current format.

Review #2
By Leopoldo Bertossi submitted on 29/May/2014
Review Comment:

I already reviewed this paper before. There are some improvements after the resubmission, but the presentation still leaves much to be desired. First of all the authors did not fully address the issues raised by the reviewers. Secondly, the paper is too unclear at many places.
More comments follow below, but at some point I stopped since I gave up.

The authors made considerable improvements on the paper,
specially on the writing. Unfortunately, the cover letter that
supposedly explains/describes the changes is not detailed
enough. It is customary (and desirable) that the authors
address the issues raised by the reviewers one by one. Instead,
they made only general remarks about the changes.

Among other problems with this approach (to cover letter
writing), we find that the authors overlook changes required by
the reviewers. This is the case with my review, which makes me
unhappy, to say the least. I have to incur in extra time and
effort to indicate desirable and the same changes once more.

My main problem is (still) the introduction. It does not
properly convey the results obtained in this paper. Nor the
idea behind the approach. A main problem addressed in this
paper is that the external data sources may make a transaction
fail. This requires rollback or execution of compensation
actions. Transaction logic as known so far does not include
these elements. So, I would expect something to be said already
in the introduction, and also about how these problems are
going to be solved in the rest of the paper. I would imagine
that the rollback need a fixed, special semantics, but not
necessarily compensation. So, how are compensating transactions
or actions captured (formalized) and forced to be executed?

It is also desirable and common that at least a minimum amount
of related work is mentioned and described in the introduction.
This does not preclude having a later section on related work
where technical comments and comparisons are made. In
particular (and as already said in my previous review), Kifer
has applied TL to web service composition. Web services by
their very nature are beyond the control of the issuer of a
transaction (in transaction logic). So, he must have confronted
a similar problem. How do he handle it? What are the
shortcomings of his approach? How are them addressed here? Etc.

The authors ignored my pointing out the work by Eiter et al. on
answer of giving a semantics to them is not far from the
problem treated here.

The authors keep talking in the introduction about consistency
(in the sense of ACID). What does it mean in this context?
Consistency wrt what?

I think the introduction does not need so many examples. It
would be better to include something around my comments above.

Specific comments: (some of them made in the previous review)

- page 2, col. 1, top: explain the idea of "independence of the
state or update semantics ..."

A few lines below: "w.r.t. the semantics ..." semantics of

- Page 3, col. 1, bottom: at that stage talking about "London
and Paris not being *entailed* ..." does not make any sense

A few lines next, top of col. 2: you mention the rollback. A
good place to elaborate on rollback.

- Page 4, col. 2, top: The consistency issue ...

Further down in this column: the description of results is very
poor ... and the description of the problems improved wrt the
previous version, but still leaves much to be desired.

- Page 4, col. 1, beginning last paragraph: why is that a
*result*? Actually what does the whole sentence mean?

- Page 4, col. 2, "Relational oracles": what if the external
relational database has integrity constraints? It may not be
just a matter of deleting one tuple, there may be internal
ramifications, which could have an effect on a later
interaction with the same transaction. Something should be said
(and done) about this issue and others. How does really the
oracle behaves and what does the external transaction know
about it? Going beyond: what kind of frame axioms or
commonsense knowledge is available/used by the external
transaction (in TL)?

- Page 6, col 1: Poorly done ...

In line 15, what does it mean? What's that? What kind of
formula? What are the language's signature? A same kind of
formula cannot be used both with the data and the transition
oracle. For the latter, predicates with "del", "ins" are
required, but are not understood by the former. Def. 1 below
does not make the difference.

By the way, what is the notion of satisfaction in relation to
the oracles? In particular, with the transition oracle and
pairs of structures? Too much is being left implicit and/or

- Page 7, col. 1: The authors freely talk about "transactions"
(they are entailed, they succeed, etc.). What exactly is a
transaction? There is no definition.

- Defs. 4 and 6: I do not understand how they combine. The
former requires satisfaction *for every path* for the M part
(for being a model of the program). So, what is the role of
in the latter?

- Page 8, Col. 2, and next column: It is never made clear that
the contents here is colloquial, and that precise definitions
will come later. So, at this point all this is highly confusing
and misleading.

It should also be said where the rollback and compensations are
captured in the logic. At this stage I have no clue about how
the authors plan to handle that, and this is the main point of
this paper.

- I do not understand why in sec. 3 (and 3.1_ the authors start
talking about actions (for the fist time). If there are actions
in this language, they should have naturally appeared before
even confronting the external domains.

- Sec. 3.1 is not for human consumption ...

I give up!

Review #3
By Michael Kifer submitted on 27/Jul/2014
Major Revision
Review Comment:

This revision is an improvement over the previous version, but it still requires much work. First, the paper is very hard to read because of its very poor English and cumbersome formalization/notation. For instance, the notation includes no less than 6 logical entailments (the different |='s and the squiggly arrow) and at least two proof-theoretic entailments (the |-'s). All these account for some 8 definitions not all of which are sufficiently lucid.

Because of the large number of lapses, typos, and other problems, I just marked them by hand on a hard copy, scanned it, and put in my dropbox; it can be found at https://www.dropbox.com/s/bq05tpui0ohqqvb/2014_07_28_00_31_45.pdf (17MB).
Too bad that SWJ does not provide a convenient way to upload PDFs.

I must say that I had the patience to correct perhaps only 1/3 of the lapses and other language problems. The quality of writing is simply not up to par. It makes the hard-to-read paper even harder to understand (and certainly hard to review).

Although rather awkward, the formalization seems sound (modulo a problem with Definition 14, case 5), but I am not quite convinced about the proofs. On pages 39 (twice) and 42, it is assumed that the goals are fully unfolded, but this is not possible if a goal has a recursive predicate. So, I am not sure whether there are unstated assumptions, restrictions, or what.

There also are some issues with Definitions 30 and 31.

In conclusion, the paper has certain novelty and could be published, but the above issues must be addressed.