++++++++++++++++++ FME2001: - Review reports for paper 48 +++++++++++++++++++++ - 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: 48 CATEGORY: 2 TITLE: A Heuristic for Symmetry Reductions with Scalarsets AUTHOR(S): Dragan Boshnachki Dennis Dams Leszek Holenderski -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): A heuristic method for reducing the state space of model checking problem is described. The method is based on finding symmetry equivalence classes over variables ranging over finite, unordered sets ("scalarsets"). 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: Techniques for reducing the state space in model checking problems are important. 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 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: A heuristic to efficiently find (almost) canonical representatives of symmetry equivalence classes. 6. How WORTHWILE is the goal of the authors? Comment: Very. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes, although I did not check everything. 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: Maybe. The experimental data suggest that the applicability of the methods varies very much with the particular problem and that it is not obvious which particular heuristic to choose or if the method helps much when the problem scales up. 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, as far as I could see. 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: 48 CATEGORY: 2 TITLE: A Heuristic for Symmetry Reductions with Scalarsets AUTHOR(S): Dragan Boshnachki Dennis Dams Leszek Holenderski -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes several heuristics for implementing state space abstraction based on symmetry reduction. The key idea revolves around the calculation of a canonical representative of an equivalence class of states by sorting a member of the equivalence class. 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: 4 Please comment your rating: This paper deals with applicability of automated formal methods to the problem of correct software design. 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: 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: Much of the work on symmetry reduction has been done on simplified models of computation. This work applies to a more sophisticated model of computation and shows how to make use of an important technique that may lessen the computational cost of symmetry reduction. 6. How WORTHWILE is the goal of the authors? Comment: Symmetric software protocol descriptions seem to arise frequently, particularly in communications protocols. Automated analysis techniques that take advantage of this symmetry to mediate against the state explosion problem would be very useful. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The goal is certainly well motivated and the experimental results are intriguing. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Technically the paper seems well written aside from one or two missteps. 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: This work is about the applicability of certain methods to a large class of protocols. The experimental results are well motivated. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality is generally high. For changes see the comments in 12 below. 11. Were there any formatting or mechanical problems with this paper?: Yes -- see below Are the figures and length acceptable?: Yes Are the references correct?: Yes -- see below 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: 1. The problem of efficiently generating the symmetry reduced state space and heuristics for generating the symmetry reduced state space has also been dealt with by: reference [4] Clarke, Enders, Filkorn and Jha where their heuristic involved multiple representatives of equivalence classes. reference [10] Emerson and Sistla where they outlined a method for efficient calculation of a canonical representative (by counting the number of processes in a particular local state) in the case of full symmetry. reference [12] Emerson and Trefler where they took the method of [10] and applied this to symmetric programs in a bdd based environment. 2. On page 3 para 2: "...putting the program counters of the individual processed together" `processed' should be `processes'? 3. I was unclear on the definition of the quotient system T/~. The transition relation is defined by [s] => [s'] iff s --> s' But suppose that [s] = {s, t} and [s'] = {s', t'} and that s-->s' and t-->t' but not s-->t'. It is unclear whether or not [s] => [s'] since it is not that case that [s] => [t'] yet [s'] = [t']. 4. On page 8, the expression for the composition of processes runs into the margin. 5. On page 10, there is the comment: "This implies that we can go beyond safety properties, or more precisely, the full class of omega-regular correctness properties can be handled" Firstly, I believe that this was first shown by reference [10] and dealt with explicitly in their paper on symmetry reduction and fairness. Secondly, as both [10] and [4] point out, care needs to be taken so that the symmetry reduction of the state space respects the internal symmetry of the formula to be checked. Since this point seems to be missing from the discussion in the paper, I found the comment surprising. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 48 CATEGORY: 2 TITLE: A Heuristic for Symmetry Reductions with Scalarsets AUTHOR(S): Dragan Boshnachki Dennis Dams Leszek Holenderski -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents four heuristics for implementing symmetry reduction in model checking by enumerative state space exploration. The heuristics are implemented on top of SPIN verifier and experimental results are obtained to compare reduction in state space with each heuristic. 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.5 Please comment your rating: The paper is a techincal paper on using symmetry reduction in enumerative model checking. Experimental results are carried out in context of SPIN model checker. This may have limited audience. 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 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: 2 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 paper proposes some heuristics for symmetry reduction in enumerating the state-transition graph of programs. The paper extends previous work Ip and Dill. Experimental results on effect of heuristics are interesting. One shortcoming is that effect of symmetry reduction on properties (invariant assertions, deadlocks, livelocks and LTL properties) being verified is not discussed. 6. How WORTHWILE is the goal of the authors? Comment: Important. Symmetry reductions can significantly reduce the size of state-transition graph but they are expensive. Good heuristics must be found for practical applicability. This paper proposes and experimentally investigates four such heuristics. However, effect of symmetry reduction on properties must be considered for applicability. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Paper is well written. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Good. 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 experimental results are justified and provide some insight into reduction achieved by each heuristic and also the cost of applying heuristic. 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 ++++++++++++++++++++++