++++++++++++++++++ FME2001: - Review reports for paper 68 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 68 CATEGORY: 2 TITLE: The Temporal Logic of Distributed Actions AUTHOR(S): Wolfgang Reisig Adrianna Foremniak -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper reformulates Lamport's TLA to cope with Distributed Actions. In fact, it is an attempt to show what TLA can not specify and what TLDA can do, especially with models based on concurrent runs. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 Please comment your rating: Distributed systems are probably a very important issue for FME's community but the paper is very technical and people who are not aware of what are the differences between true concurrency and non determinism may be lost. However, we decide to choose 2. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 2 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 5 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The reformulation of TLA using concurrent runs and another point of view with respect to Lamport's one. 6. How WORTHWILE is the goal of the authors? Comment: OK 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: It is a very polemical paper; I think that the authors have not well understood the objectives of TLA and the famous stuttering. The goal is not really well explained since it seems that there are confusions over notations especailly the leadsto operator which means possibly in this framework. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The level of technicality and quality is not equal. There are some parts which are very technical and tough but it is mainly because the approach is very complex. The essence of TLA is the stuttering and the refinement as implication and TLDA extends the expressivity of TLA by not really useful properties. Hence, technical statements are sound but the leadsto operator has not the same meaning than Lamport*s one: this is a very bad point, since it states the eventuality. Leadsto of TLDA states possibility which is not really useful. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The work is mainly theoretical and there is no realistic case study; this detail is a very bad point and does not help the authors to convince the reader. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: too technical and too boring notations. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: OK the paper of lamport on the possibility properties if missing. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: A convincing example is missing; you use simple examples because your approach is too concrete and hence is very close to what you are modelling. The stuttering helps in defining step by step a complex model. The leadsto operator is in fact defined as a double negation of the box operator which leads me to a branching semantics and then to an interpretaion as a possibility property. Moreover, Lamport has developed a way to state possibility proprties but are they really usefull??? We need to state thing that will happen and I don't care to prove that something may happen. If so, I can reformulate using TLA. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 68 CATEGORY: 2 TITLE: The Temporal Logic of Distributed Actions AUTHOR(S): Wolfgang Reisig Adrianna Foremniak -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The authors define a temporal logic over concurrent runs and compare it with Lamport's TLA. They argue that concurrent runs are more adequate to represent system specifications, and in particular progress and fairness. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 Please comment your rating: This is a paper on the theoretical foundations. No attempt is made to argue the usefulness of the proposed formalism for the theme of FME2001, "Formal Methods for Increasing Software Productivity". 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 2 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 4 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: In my opinion, the paper is mainly a revival of known arguments about interleaving vs. true-concurrency approaches to the semantics of concurrent programs. It is well known that properties can be expressed more faithfully using concurrent runs, but this has (perhaps disappointingly) not deterred practitioners from basing most of their work on sequential runs. I do not believe that this paper is going to help convince them. Moreover, as explained below, I have doubts about the consistency and correctness of the authors' approach. 6. How WORTHWILE is the goal of the authors? Comment: It would be good to convincingly demonstrate that true-concurrency semantics actually solve real-world problems. (So-called partial-order methods for model checking were for some time thought to be such an application, but have turned out not to.) Unfortunately, the paper does not advance current knowledge in this respect. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The authors give a number of examples for the superiority of true concurrency over interleaving semantics in section 5, but these concern boundary cases where some variable participates in some action, although this is not externally observable (i.e., the variable is unchanged). 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Rather untypically for true-concurrency approaches, the authors define a step in such a way that enabled actions are taken as early as possible (cf. the definition of a step in 2.26). Apparently this decision has been taken to simplify the semantics of the logic (in particular, 3.9), but it is in contrast with the informal presentation (cf. the last sentence in section 2.2). It appears that even the authors have overlooked the consequences of this simplification, as exemplified by specification (5.2). Assuming that conjunction distributes over [] as usual (and although the authors do not discuss proofs, I do not see from the semantics why it shouldn't), the specification implies [](x=1 \land z=6 \implies x'=2 \land z'=7 \land \neg Y \land \neg Z \land \neg X) (where I have written X instead of \tilde{x} etc.). Together with formula init, this means that the system is immediately deadlocked, contrary to what the authors intend. It seems that the specification would become much more complicated in order to avoid this problem. Even if it were rewritten, I would still not understand how the tight synchronization is compatible with the desired reachability property (5.1). 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: Not in my opinion. In particular, the clock example of section 3.5 can be easily (and arguably more perspicuously) specified in TLA along the same lines: HR_1 == hr \in {0,...,23} \land [][hr' = suc_1(hr)]_hr MIN_1 == min \in {0,...,59} \land [][min' = suc_2(min)]_min SYNC == [][min=59 \land min' \neq min]_hr HR-MIN_1 == HR_1 \land MIN_1 \land SYNC 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The overall exposition is nicely structured and easy to follow, perhaps with the exception of section 5 which implicitly presupposes concepts from Petri nets. However, there are many awkward formulations and grammatical mistakes. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Please do not use as many numbered equations. The formatting of basic concepts on page 6 should be improved. Fonts are sometimes used inconsistently, and the spacing is sometimes wrong. The figures on pages 16 and 18 should be more consistent in size (esp. fig. 6). Besides references to Lamport's papers there should be pointers to other logics interpreted over concurrent runs. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Some minor comments, in order of appearance: p.3,l.10: Please motivate the restriction that each variable is engaged in at most one transition of a step. p.3,l.-11: "disjunct" -> "disjoint" p.3,l.-10: "s" and "s'" should be "S" and "S'" p.7,l.-9: Please say that pr_1 denotes projection. p.10, l.-14: "step" should be in italic font. At the end of the line, I believe that (3.7) is not necessary. p.10, l.-1: What are "reached variables"? p.11, l.8: misprint "tha" p.11, eq. (3.14): The two representations for Involved(A,X) are not equivalent because the variable \tilde{x} which appears free in the lower representation would be existentially quantified by the Enabled predicate, and therefore does not appear free in the upper representation. As minor remarks, "Enabled" should be italic in (3.14), and the parentheses of the formula at the bottom of the page are not obvious: you want \forall ... : ((A \implies \bigvee \tilde{x}) \land ...)(...) not \forall ... : (A \implies (\bigvee \tilde{x} \land ...))(...) which would be the usual reading. p.12, l.9: (3.6) should be (3.16). p.12: (3.21) and (3.22) are identical. Section 5.3 should be better explained. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 68 CATEGORY: 2 TITLE: The Temporal Logic of Distributed Actions AUTHOR(S): Wolfgang Reisig Adrianna Foremniak -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper defines TLDA - Temporal Logic of Distributed Actions, which is a reformulation of Lamport's TLA. The authors show that TLDA can express properties which are not expressible in formalisms based on sequences of states (such as TLA). The authors introduced the notion of "progress" which resides in this gap of expressiveness and claim that this notion captures the demand that a system proceeds better than the "weak fairness" notion. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: It provides a partial-order version of the logic TLA used to specify systems an their properties. This version, by combining the notions of concurrent runs and TLA, enable to distinguish between non-determinism associated with choice and independent progress of concurrent components. It leads to a natural way of reasoning about abstraction and composition of distributed systems. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The proposed reformulation of TLA, TLDA is new. Its significance stems from the fact that it can express properties inexpressible in TLA yet it retains many valuable properties of TLA. The notion of "progress" that can be expressed in TLDA and cannot be expressed in TLA, is new and seems to lie in between TLA (and LTL) diamond and CTL EF operator. Unfortunately, the paper does not adequately explain the contexts under which this notion is more useful than the TLA "eventually". It is also a serious drawback that the examples used to demonstrate the ideas are too trivial and do not represent interesting cases. Obviously, it is false to state that TLDA is "more expressive than TLA", and the correct statement should be that the two are incomparable. Certainly TLDA can express propeties which TLA cannot, but TLA can express propeties which are inexpressible in TLDA (for example the TLA <>). Also, it is clear that TLDA diamond is "weaker" than the TLA/LTL diamond. However, it is not as weak as CTL's EF, but lies somewhere in between. For example, if we examine the example of Fig. 3, then <>(x=3 | z=8) is true for both the TLA and TLDA interpretations of <>, but while EF(x=3) holds for this system, <>(x=3) is false in both the TLA and TLDA interpretation of <>. The reference list is scandalous. There has been a lot of work on various versions of temporal logics intended to deal with partial-order semantics. The paper completely ignores all of them. I feel that it was a design mistake to associate a unique step with each global state (cut, anti-chain) in a run. The temporal operators are based on the notion of suffix which proceeds from one cut to a later one. Why evaluate state formulas on the maximal step possible at every cut? 6. How WORTHWILE is the goal of the authors? Comment: it introduces a new logic which is a variation of TLA that uses concurrent runs instead of stuttering sequences. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: the goal is not explained so well. There is no introduction to the paper, a place one usually hopes to find an explanation of the goal. Nor is the goal explained in other parts of the paper. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: there are no theorems algorithms and proofs in the paper. The definitions are not as formal as they should be, but the idea is understood. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: the work is primarily theoretical. The authors show that TLDA can distinguish between two systems that TLA and any other formalism based on states sequences cannot. However in the example they give, it is not clear why one would like to distinguish these two systems. Specifically I don't understand why a variable that is in the scope of a transition but is not engaged (not changed by the transition) should be regarded as being used when it was just observed. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The definitions in the paper are not as formal as they should be. Some definitions are missing. Some notations are confusing. Suggestion for changes (including typos): (1) Add an introduction explaining the goal of the paper. (2) The letter immediately following a colon should not be capital. (3) In page 4, first line, replace "steps do with" by "steps dill with" (4) In page 7, lines 30-31, you claim |F^{-1}(t)| =|F(t)|. This cannot be inferred from the definition of a concurrent run (although it is understood from what you say (not define) about transitions. Please correct the definition of concurrent run accordingly. (5) In page 9, second line, you use '/' (in s[[v]]/v), please define it. (6) In page 9, lines 2,26: you use different type of quotes, in both places I suggest to replace it by quote and unquote. I also recommend to change the confusing notation of writing the quantifiers within the parameter lists. (7) In page 9, line 19, replace "variables are involved" by "variables in \tilde(Y) are involved". (8) In page 10, line 1: replace "U_1 \models \neg..." by "U_1 \models A \wedge \neg..." (9) The notion of "unique step" (page 10, line 8) although understood is not defined. Please define it. (10) In page 10, line 28, you define "Enabled A", I suggest to replace it by "Enabled (A)" - same notation you use for other predicates. (11) In page 11, line 8, replace "tha" by "the" (12) In page 11, line 11-12, the operands of \supseteq should be without 'tilde'. (13) I think that the discussion preceding the definition of "Involved(A,X)" is not helping the understanding. I think it can be explained more intuitively and in one line by "Involved(A,X) = \neg Enabled (A \wedge \bigwedge_{x \in X} \neg \tilde(x))". (14) In subsection 3.5. please add a formal definition of a system. (15) In page 12, line 8, replace "(3.6)" by "(3.16)". (16) In page 12, there is no difference between (3.21) and (3.22). (17) In page 13, I suggest to reorganize the paragraphs in the introduction of section 4, such that the second and the forth which both discuss interleavings will come together after the third paragraph which explains fairness. (18) It seems to me that the notion of progress is better explained in its negative form. I.e, explain that a progress of an action is not respected if the action is not taken although it is enabled and all the variables, x, participating in it (the ~-ed variables) are eventually always free (free means do not participate in other actions). (19) In page 14, line 3 you say that \cal(T) may have infinitely many valuations, this is true when using an infinite set of variables (like in TLA). I assume that this is what you mean, but you never state it. (20) In page 14, line 17, replace "progress of A" by "progresss of an action A". (21) In page 15, line 2, replace "and U is never" by "and it may be the case that U is never". (22) In page 15, lines 19-22: you confuse the terms of state and step by saying "a state is taken" instead of "a state is reached" or "a step is taken". (23) In page 17, line 10, replace "For a TLDA formula p define" by "For a TLDA formula p and a system Sigma define" 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: yes. Are the references correct?: as far as I am familiar with, yes. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++