++++++++++++++++++ FME2001: - Review reports for paper 24 +++++++++++++++++++++ - 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: 24 CATEGORY: 2 TITLE: Model-Checking Over Multi-Valued Logics AUTHOR(S): Marsha Chechik Steve Easterbrook Victor Petrovykh -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper motivates and proposes the use of multi-valued logics in software engineering. It defines a multi-valued extension of Computational Tree Logic (CTL), and presents a symbolic model-checker Xchek for this logic with an analysis and discussion of its correctness and optimization issues. 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: The use of model-checking in system analysis is of majority interest. This will be of interest even to those who use classical logics. It meets the theme of FME 2001, by `enhancing analysis techniques for validation and verification'. 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: 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: 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 too well qualified to judge, since I am not familiar with developments in multi-valued logics. But it appears to me that the multi-valued extension to CTL is new, and thus the symbolic multi-valued model checking algorithm and tool are also new, and significant. 6. How WORTHWILE is the goal of the authors? Comment: The provision of tools to support multi-valued reasoning is worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: It is well-motivated. The running example is useful for explaining and motivating the work. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: They appear to be 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: The methodology is sound. The authors have essentially established `proof-of-concept' so far, and have yet to develop the tool to be able to handle non-trivial systems (as they acknowledge in their conclusions section). 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is clearly written and easy to understand. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: The main body of the paper is 18 pages, which is acceptable, but there are a further 8 pages of proofs in an appendix. These do contribute to the paper, but the paper could be made self-contained without it (if the proofs were to appear elsewhere, e.g. in a technical report). Are the references correct?: as far as I can tell. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Theorem 8 is reassuring. It would be interesting to know if Xcheck is as efficient as other tools on (2-bool,sqsubseteq)? You have results about complexity. Do you have the results of any actual experiments, e.g. how long it takes to check the thermostat system against how many states there are to check? It may be of interest to include figures here. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 24 CATEGORY: 2 TITLE: Model-Checking Over Multi-Valued Logics AUTHOR(S): Marsha Chechik Steve Easterbrook Victor Petrovykh -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents an extension of CTL to a multi-valued quasi-boolean CTL (called \chi CTL), an extension of a Kripke structure to a multi-valued quasi-boolean Kripke structure (\chi Kripke) and an algorithm to perform model checking of a \chi-Kripke structure with respect to a \chi-CTL 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: 3 Please comment your rating: this elegant extension of model checking to multi-valued quasi-boolean logics offers an automated means to reason about systems with uncertainty and/or inconsistency. Also, since it extends model checking to reason over any n-valued logic (as long as it is quasi-boolean) it may have other applications as well. 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: 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 multi-valued quasi-boolean CTL (\chi-CTL), and the multi-valued quasi-boolean Kripke structure (\chi-Kripke) are new notions. The algorithm to perform model checking of a \chi-Kripke structure with respect to a \chi-CTL formula is of course new as well. I believe this is the first time that the notion of model checking was extended to reason over any n-valued quasi-boolean logic. 6. How WORTHWILE is the goal of the authors? Comment: the ability to reason over system with uncertainty or inconsistency is definitely worthwhile. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: the authors did a fine job in explaining and justifying this goal in the introduction to the paper. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: all definitions are sound. All theorems are followed by a sound proof (in the appendix). The model checking algorithm and its correctness proofs are sound as well (a few minor remarks are specified in item 10). Some of the examples seem incorrect and some of the properties inaccurate (these also will be elaborated in item 10). 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: as mentioned in 6 the applicability justifies the theory. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: the paper is very nicely written. I suggest the following changes: (1) page 4, line 4: Replace IDLE_1 by IDLE_2. (2) To exemplify the logic lattices of Fig. 2, figure 2 does not suffice in itself. I suggest to add the truth tables for the relevant operators (meet,join and complement), as otherwise one cannot fully understand the places there referred to (e.g. after definitions 2 and 5). The truth tables of the operators of lattice (3-QBOOL,\sqsubseteq) is mandatory as it serves as the logic of the ongoing thermostat example. (3) page 7, line 31 replace "to quasi-boolean lattices" by to "n-valued quasi-boolean lattices". (4) page 9, definition of \chi-CTL, replace $a \in I(v)$ by $s\in I(a,v)$ (5) page 11, after the definition of BigOpTable add a comment saying that BigOpTable can be computed only for commutative operators, and thus there is no BigOpTable for the implication operator. (6) The definition of PartitionType (page 11, line 31) is not clear. I suggest to replace it by the following: a PartitionType is an |L|-tuple (S_1,s_2,...,s_{|L|}) such that for all i\in{1,..|L|) S_i \subseteq S and \bigcup _{S_i \in S} = S. (7) In Fig. 5, page 12: there are mixed fonts for the same value 'v', which appears slanted in the "foreach statement" and straight in the "result statement". This is confusing especially in the function doBigOP where capital V is used as well. (8) page 13, lines 1-2: pred([Running],\wedge) should return ({IDLE_1,IDLE_2,HEAT,AC,OFF},{IDLE_2},{IDLE_1,IDLE_2,AC,HEAT,OFF}} (9) page 13, lines 9-11: there is no need to repeat the definition of PartitionType, maybe its best to add this explanation immediately after the definition at page 11, line 31. (10) The computation of BigOpTable_{op,v} in function doBigOp is a bit more complex than the other functions, I suggest to elaborate and explain it better (page 13, line 12). Also, replace "intersection of states" and "union of states" by "intersection of the set of states" and "union of the set of states" respectively. (11) The example in page 13, lines 15-17 is incorrect. {IDLE_1,IDLE_2,HEAT} seems to be the result of [doBigOp(\vee,[pred([Heat],\vee)])]_T. (12) page 13, line 29: replace "EU and AU" by "E[\varphi U \psi] and A[\varphi U \psi]" (13) page 14, line 1: right parenthesis is missing to the left of the equality sign. (14) The \chi-CTL properties does not reflect accurately the (English) properties in Table 1 (page 14). For example a more adequate translation of the English property 4 is AG (Heat <-> \neg AC) (15) Page 14, second line from the bottom: replace "running time is smaller" by "running time in the average case may be smaller". (16) Page 15, Theorem 5, replace "\forall p \in P" by "\forall p in \chi CTL" in both (a) and (b). (17) Page 16, lines 10,11: pleas define "BooleanCheck(p)". (18) Page 19, Theorem 1: the following property is missing from the theorem statement and proof: (4) (a_1,b_1) \sqsubseteq (a_2,b_2) \Leftrightarrow \neg (a_1,b_1) \sqsupseteq \neg(a_2,b_2). (19) Page 19, please reverse the order of the implication (i.e. the order of lines) in the proof. (20) Page 22, proof of Theorem 5, in line 23 replace "\varphi()" by "check(\varphi)", and replace "\neg v is onto" by "\neg is onto" (21) Page 23, proof of Theorem 6, in line 177 replace "s \in [...]_{neg_{v_i}}" by "s \in [...]_{neg_v}" (22) Page 24, proof of Lemma 4: In line 30 replace "(value of InvTable,\vee,T)" by "(the equivalence of v_1 -> v2 to \neg(v_1 \wedge \neg v_2)". In line 31 replace "(s,l) \notin R" by "(s,l) \in R". (23) Page 24, Theorem 8: replace "\forall p\in P" by "\forall p \in CTL" (24) Page 25, line 5: replace "proofs for" by "proofs of (2) for" (25) Page 25, lines 18,26: replace "<\psi>_a" by "<\psi>_b" (26) Page 25, lines 36,45: replace "[pred([varphi],\rightarrow)]" by "[pred([varphi],\wedge)]" (total of 4 occurrences). (27) Page 25, line 48 replace "s \in BooleanCheck(p)" by "s \notin BooleanCheck(p)" 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 the ones 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 ++++++++++++++++++++++ PAPER NUMBER: 24 CATEGORY: 2 TITLE: Model-Checking Over Multi-Valued Logics AUTHOR(S): Marsha Chechik Steve Easterbrook Victor Petrovykh -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes use of multi-valued temporal logic for capturing uncertainities and inconsistencies (as in paraconsistent logics). The set of logical values is required to form a quasi-boolean distributive lattice and user must supply (as tables) interpretations of and (glb) and or (lub) operations. Semantics of CTL is extended to such many-valued logic and the CTL model checking algorithm is reformulated to deal with multiple values. A tool XCTL implementing the algorithm is outlined. There are no serious examples presented and the implementation of the tool is, I believe, incomplete. 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: This paper belongs more to a specialised conference such as TACAS or CAV. However the idea of paraconsistent reasoning may have some bearing on formal methods in general. 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: 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 paper presents a very interesting direction of work. They extend temporal logics classical boolean reasoning to one with multiple truth values forming a quasi-boolean lattice. Conceptually, such a framework can be used to reason about uncertainity, qualitative reasoning and paraconsistency (where inconsistency does not immediately degenate to triviality). Paper is techically 6. How WORTHWILE is the goal of the authors? Comment: While no serious examples of the proposed framework are discussed I found the proposal original and interesting direction for work. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Paper is very well written. The goals are well motivated and the technical part of the paper is nicely developed. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The paper is of high technical quality. 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 paper proposes foundations behind multi-valued CTL model checking. No serious examples are presented and implementation of the model checking tool is also incomplete. Thus paper is purely theoretical at this stage. Unfortunately, the complexity of proposed decision procedure for multivalued CTL is linear is size of the formula but cubic (S**3) in size of the transition system. I am afraid this could be prohibitive in in pratice as usally properties are small but systems are large. Please discuss. One more omission is justification of the proposed fixed point characterisation for AU and EU operators in Figure 3 (page 9). These definitions are at the heart of the paper and MUST be properly motivated. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Very Well written. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Typographic error: page 9 Section 5.2 Definition of s "a in I(v)" should be "s in I(a,v)" 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 ++++++++++++++++++++++