Review Comment:
SUMMARY: This paper develops a logical formalism called ServLog for
modeling- and reasoning about service processes. A service process is
understood as a specification of legal patterns of interaction between
service providers and service consumers (control flow) as well as a
specification of how data flows between the tasks that form the
constituents of this process (data flow). Eligible service processes
are in the general case constrained by the contract requirements of
the consumer and the service policy of the producer.
ServLog is a declarative, logic programming-like language. The basic
idea is to identify tasks in a service process with predicates and to
model data flow by the sharing of arguments and unification. To
account for the cases when data needs to be shared between tasks that
have no control dependencies, ServLog allows data to be shared by
updating a database. This makes the semantics of ServLog rather
different than say, answer set prolog, or other LP languages, in that
it is formalized in terms of paths over database states.
ServLog is made up of three distinguishable linguistic components: 1)
a language for expressing concurrent service processes (Concurrent
Transaction Logic), 2) a (Horn) rule language for defining composite
processes, and 3) a constraint language for expressing contract
requirements and service policies. The Horn rules are used for
rewriting process formulae into primitive tasks, and in particular, to
formulate recursive tasks. Elements of the constraint language act as
auxiliary requirements on the application of inference rules governing
the rewriting of process formulae. The constraint language in fact
constitutes a separate rewriting system, since constraints are rewritten
during contract execution to ensure that the interactive proof
procedure that generates the execution path never has to look back to
previous states in order to decide how to proceed. The proof system thus
assumes the form of a sequent calculus with a plugged-in term rewriting component.
It is proved to be sound and complete wrt. the semantics, although the proof perhaps
leaves a couple of things to be desired (cf. below).
OVERALL ASSESSMENT:
This is a good paper with a clearly defined problematic and a
fitting solution. It is well written and presented, and generous
with the example material---much to the aid of the reader.
The motivating example is rich and in my opinion realistic, and
testifies to extensive experience. The modelling of contract execution
by way of a proof system that is tempered by a separate rewriting system
for constraints is ingenious, and the examples illustrating its workings
are good fun to work through.
All in all I think this paper would make a nice contribution to the field of service science (although I suspect that branding it as a separate science may be a bit of a mouthful), and more generally to the semantic web community (broadly conceived).
I therefore recommend it for publication, subject to minor revisions.
ORIGINALITY: I am not very well-read in the service orientation literature and have
therefore tried to assess the originality of the paper by checking the
list of references and by having a look at some of the previously published titles by either of the authors.
Of the 39 references, 15 are co-authored by one of the authors of this paper, and 3 more by their co-authors again. This makes the degree of self-containment somewhat high, but I am not inclined to regard that as a problem.
The motivating example from the paper currently under review occurs in [1], but is substantially enriched in this new paper by adding constraints, iterative processes and data flow.
References to Concurrent Transaction Logic seem to go back to [2] where a semantics, a proof system and a completeness theorem linking the two are presented. None of the other two of the three above mentioned linguistic components of ServLog are covered by this result.
The notion of a constraint language for service contracts and policies
goes back at least as far as [3], and the idea of using constraints
to control the application of CTL inference rules goes
back at least as far as [4]. In particular, the set of constraints called serial constraints in the paper currently under review, were mostly formulated in [4], although the formalism is rather different.
Data flow in service processes are discussed in [4], but it is there implemented with data flow graphs rather than, as in the paper currently under review, by variable sharing.
Taking stock, the originality of this paper does not reside primarily in the novelty of its basic ideas, but rather in its confident and consistent development of these ideas in a unifying logical framework. The authors give a detailed account of the contributions in the
related work section. In my opinion, it is sufficient to warrant a new
publication---it is a case of conference and workshop material maturing into a journal paper I would say.
SIGNIFICANCE OF RESULTS: ServLog demonstrates the possibility of reasoning about service oriented architectures and service processes in a strictly logical idiom with a sound and complete proof procedure. This is obviously of value for everything from specification to protocol verification and model checking. ServLog claims to have an advantage over its competitors insofar only ServLog stays strictly within these confines (the confines of logic, that is). This is potentially very significant, of course, as the entire service process now becomes a mathematical entity subject to mathematical rigour.
PRESENTATION: The paper is generally well-structured and well-written.
I have a few comments and suggestions:
Paths and multi-paths: When multi-paths are introduced on page 7 they are denoted with indexed \mu. This keeps them distinct from paths, which are denoted by indexed \pi. On page 8, e.g. the first inductive case of the truth definition, both paths and multi-paths are denoted by indexed \pi. The former practice is a better idea I think, and should be adhered to consistently.
Intro to section 2: The last paragraph on page 2 regarding the BPMN, WSMO and such seems a bit out of place and disrupts the flow of the argument. I suggest it be moved to the related work section.
Primitive versus elementary updates: The different uses of the terms 'elemantary updates' and 'primitive updates' had me confused. We are first told on page 9 that an elementary update is one that changes the underlying database state. Then on page 10 we are told what a primitive task is (namely one that is not allowed in rule heads) and that there are three kinds; updates, queries and tests. Next, the last two lines on page 16 tell us that a primitive update is just an elementary CTR update. The footnote 12 on page 17 adds to the confusion, in my opinion, by saying that primitive tasks (generally?) are *represented* by elementary updates. I suggest that the authors either make more of an effort to justify the dual terminology, or preferably that they simply choose one and adhere to it consistently.
Constraints based on primitive update tasks: The discussion following definition 4.13. on page 17 is in my opinion not up to the high level of precision that characterizes the rest of this paper. First of all the definition itself states that a set of constraints is based on primitive update tasks iff all tasks appearing in the set are primitive update tasks. On a first reading one is inclined to understand 'appearing' as membership. On closer inspection that cannot be so, of course, because no primitive update task is an elements in a set of constraints, strictly speaking, only constraints are. The subsequent discussion is also a bit unclear. The authors argue that the restriction to primitive updates does not limit the expressive power of the language since one can insert bounding primitive tasks (and note that it does not say 'bounding primitive update tasks' here) to delimit the start and end of a task, and then reformulate the constraints wrt. these bounds. An example is provided where a constraint 'after(p -> q)' is replaced by 'after(p_start -> q_start)'. Now, if this discussion is to make any sense as an illustration of definition 4.13. then p_start and p_end must be primitive update tasks, not merely primitive tasks. Yet, what kinds of update would they be? A primitive/elementary update is a relation over database states. What is the relation in question here? The matter is additionally blurred by the fact that the term 'primitive update tasks' occurs only in the definition, whereas the subsequent discussion speaks more generally of 'primitive tasks'.
The authors could have been slightly more generous with their citation practices. For instance, the service contract assumption and the independence assumption are formulated in prequels to this paper, making a reference in order.
*** Additional comments ***
SEMANTICS: The semantics of ServLog is, as acknowledged by the authors, presented only informally (or, I would say, semi-formally). It is mostly clear: we are given definitions of paths and multi-path structures along with a set of operations on them, and we are given rules for assigning truth values to CTR formulas over paths.
However, a crucial element is missing, namely the definition of the
semantic property that is appealed to in the soundness proof of appendix A (denoted by the double turnstile |=)--- whether it be satisfaction or entailment that is intended. Indeed it is not obvious which one it is. Ordinarily soundness would be taken to mean that derivability in the calculus corresponds to semantic entailment. However, this does not seem to be what the authors have in mind. A ServLog sequent says (adjusting notation here for a non-latex environment) for a given set of Horn rules P, a database state s, a set of constraints C and a CTR formula A, that A as defined by P can execute along *some* path that starts with s without violating the constraints in C. Now, since the derivability of sequents is the concept that the semantics is intended to correspond to, it would mean that |= is not semantic consequence but satisfaction.
I have no clear opinion about the significance of this observation, but I do know that it means that both the soundness and the completeness proofs are rather unusual. Instead
of linking an existential notion to a universal one (i.e. if there *exists*
a proof of such-and-such a sequent then truth is ensured wrt. *all*
valuations in such-and-such a class) it links an existential notion
to another existential notion (if there *exists* a proof of such-and-such a sequent then there *exists* a non-constraint-violating path on which the CTR formula is true). I should think that this warrants a few words, and that it is sufficient reason for defining the relevant concepts and notation in the semantics section, particularly the |=.
SOUNDNESS AND COMPLETENESS: Given the satisfaction-reading of |=, the soundness proof appears to be correct. As regards the completeness proof, the strategy is sensible, but the execution of it may be a bit too sketchy. Here are a few observations:
The completeness proof delegates the grunt work to a previously established completeness result for CTR. That would be acceptable were it not for the fact that it is difficult to trace the provenance of the completeness proof in question as no specific source is given. The theorem is stated in [2], and it is this paper that seems to be intended whenever there is talk of the original CTR logic. However in [2] the theorem is stated but not proved. To be clear I do *not* doubt that this result has been proved, I am just saying that the authors should either supply us with a proof or with a reference to one.
There is more that turns on this obscurity of origin, because it is only possible to defer to the original completeness result for CTR to begin with if it is the case as the authors claim that 'the new system reduces to the old one when the set C of constraints is empty' (page 9). Again, it is not clear which system 'the old one' is. If it is that of [2], then it is at least not obvious that these two systems are the same in the absence of constraints. Their outward form is rather different, whence ideally the interderivability of the two sets of rules should be demonstrated.
Finally, the wording of the inference rules starting from page 21 is not entirely crisp: Prior to stating the inference rules themselves, C and C' are declared as sets of constraints. Yet, rule 1 refers to the disjunctive normal form of C, and to C' as one of its disjuncts. I am used to thinking of disjunctive normal form as a property that applies to formulae, not sets, and since it is therefore not clear to me what C is, neither is it clear what C' is.
TYPOS AND SUGGESTED REFORMULATIONS:
Page 7, section 3, first line: 'the classical predicate logic' -> 'classical predicate logic'.
Page 7, section 3, fourth line: 'the classical logic' -> 'classical logic'.
Page 13, second paragraph, second line from bottom: 'completely different logical variables' -> 'different logical variables'.
Page 20, section 5.2, second paragraph, first line: 'To simplify the matters' -> 'To simplify matters'.
Page 24, fourth line after example: 'If we did not take these assumptions' -> 'If we did not make these assumptions'.
Page 29, the soundness proof: The font changes for the set of constraints C.
REFERENCES:
[1] D. Roman, J. and M. Kifer: Semantic Web Service Choreography: Contracting and Enactment. In International Semantic Web Conference, 2008.
[2] A. J. Bonner and M. Kifer: Concurrency and Communication in Transaction Logic. In Joint International Conference and Symposium on Logic Programming, 1996.
[3] H. Davulcu, M. Kifer, C. R. Ramakrishnan, and I. V. Ramakrishnan. Logic Based Modeling and Analysis of Workflows. In PODS, pages
25–33, 1998.
[4] D. Roman and M. Kifer. Reasoning about the behavior of semantic web services with concurrent transaction logic. In VLDB, pages
627–638, 2007.
| 
