++++++++++++++++++ FME2001: - Review reports for paper 10 +++++++++++++++++++++ - 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: 10 CATEGORY: 2 TITLE: An abstract semantics of temporal logic specifications AUTHOR(S): Anatol Ursu -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper is concerned with approximating temporal logic properties by means of deterministic (abstract) Buchi automata. The paper provides the technical justification for a fixpoint characterisation of the abstract semantics, and an abstract interpretation which supports the approximation. 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 paper focuses on the technical details of the work, and is concerned with some quite technical results. Although the benefits of the work is discussed in the conclusions, the paper does not really address the application of these results. The paper is suggesting the basis of a formal analysis technique for reasoning about temporal logic specifications, but it does not show how this could happen. 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. Although the paper does provide some technical results, it appears to be quite theoretical for FME, and might be better at a conference such as LICS or CONCUR. 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: I am not up to date on developments in Buchi automata and temporal logic. I am semi-confident that the fixpoint characterisation of the abstract semantics is new, and the abstract interpretation work. This would be the significant aspect of the paper. 6. How WORTHWILE is the goal of the authors? Comment: The aim of producing an abstract semantics which is more amenable to analysis techniques and which approximates the `real' semantics is always worthwhile. The goal of the author is to provide this abstract semantics. But FME will be more concerned with the application of this theoretical foundation to the analysis of systems. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal of developing the semantics is well-explained. But its usefulness, and the benefit of the work, is not very well explained or justified, and is only considered briefly in the conclusions. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: broadly yes, as far as I can tell. 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 theoretical. I do not believe that the author has explicitly justified the implications in terms of applicability adequately. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The writing is satisfactory. The author's style can be terse, and perhaps some further explanations around the technical material would be beneficial. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: A brief review of Buchi automata would be useful. You can't assume that all the FME audience will be familiar with them. On page 4, should C contain Succ(s0) ? In the example on page 5, there is a state s1 which is not followed by s0. Some further justification and motivation for the work in terms of its applicability would be appropriate for the FME audience. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 10 CATEGORY: 2 TITLE: An abstract semantics of temporal logic specifications AUTHOR(S): Anatol Ursu -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes a new semantics of temporal logic specifications, which is an approximation of the standard specification. The new (so called abstract semantics) are accepted by deterministic Buchi automaton, and hence easier to check for satisfiability etc. (as opposed to non deterministic Buchi automaton). However, no applications of such an approximate semantics are given. The referee doesn't find the approximate semantics to be of any use. 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: 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: 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: New semantics definition, and showing that it is what is accepted by a deterministic Buchi automaton. Also, a standard form is introduced. 6. How WORTHWILE is the goal of the authors? Comment: The goal of the author is not worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Not justified at all. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Sound. 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:Methodology is sound. But even the theoretical results are not applicable and are not justified. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Fair 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 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 ++++++++++++++++++++++ PAPER NUMBER: 10 CATEGORY: 2 TITLE: An abstract semantics of temporal logic specifications AUTHOR(S): Anatol Ursu -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper proposes to approximate a temporal logic formula by a deterministic buchi automaton. Covenversely, such an automaton can also be considered as a formula. These to functions form a Galois connection. The purpose of the proposed approximation is NOT stated or justified. The only property of the approximation is that it is weaker than original formula. 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: The paper is technical work on approximating Temporal logic formulae. The purpose of approximating the formula is not stated or justfied. I found the approximated formula to make no intuitive or practical sense. While a lot of technical set up is used, goals are not clear at all. 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: 1 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: Poor 6. How WORTHWILE is the goal of the authors? Comment: This is a confusing paper. The goal is not clearly stated and I find the proposed approximation of Temporal Logic formulae pointless. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Not justified at all. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Poor. There are problems with some basic definitions. See comments to author. 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: It is not clear what is the purpose of this work. Approximation proposed makes no intuitive or practical sense to this referee. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: OK 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Page 3 Fixed point semantics of Until is INCOMPATIBLE with standard interpretation of Until operator. According to your definition A U B <=> A /\ O(B \/ (A U B)) whereas standard unfolding of Until is A U B <=> B \/ (A /\ O(A U B)) Please justify your approximation of TL to Deterministic Buchi automaton. Why is this approximated Buchi automaton interesting? +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++