++++++++++++++++++ FME2001: - Review reports for paper 31 +++++++++++++++++++++ - 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: 31 CATEGORY: 2 TITLE: An Adequate Logic for Full LOTOS AUTHOR(S): Muffy Calder Savi Maharaj Carron Shankland -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper introduces a new logics called FULL (based on CTL) to reason about the behaviour of terms in LOTOS and proves that this logic can distinguish non-bisimular terms. 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 introduced logics is powerful enough to specify properties of systems specified by LOTOS. However, the paper has not provided any proof system for the logic or rules for reasoning about LOTUS specification. The adquacy is rather obvious. So the results are not very deep. 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: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating of 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: See 2 (above) 6. How WORTHWILE is the goal of the authors? Comment: See 2 (above) 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Clear, and easy to understand 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Mostly. There are some typing mistakes: E in Definition 1 is unspecified, In line for the definition of $T\models \Lamda, $z$ should be $x$. 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 justification of implications in terms of applicability is not sufficient. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: 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: 31 CATEGORY: 2 TITLE: An Adequate Logic for Full LOTOS AUTHOR(S): Muffy Calder Savi Maharaj Carron Shankland -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): A first step towards providing a framework which supports the verification of properties of full-LOTOS specifications. The approach is based on a symbolic treatment of data in order to remove the problem of infinite branching of event choices. 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: Not only targetted at the LOTOS community, the paper should also be of interest to researchers in symbolic computation/analysis 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: 4.5 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: Their symbolic transition system and modal logic introduced 6. How WORTHWILE is the goal of the authors? Comment: VERY ... addressing a serious problem 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: YES 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Good, but it is clear that much more theoretical work remains to be done. (They do mentioin this in their conclusions). 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 implications are adequately justified. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: GOOD 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: The conclusions identified many things to be done. In particular, the relationship between your semantics and standard LOTOS semantics must be addressed. Also, the limited practical use of the bisimulation needs looking at. Finally, your approach might be usefull for practical purposes. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++