++++++++++++++++++ FME2001: - Review reports for paper 43 +++++++++++++++++++++ - 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: 43 CATEGORY: 2 TITLE: Reachability Analysis of Timed Automata in Polynomial Time AUTHOR(S): Dirk Beyer -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a framework for symbolic reachability analysis of systems modeled using communicating timed automata, bounds on BDD-sizes in special cases, and experimental results on sample case studies that show improvement in performance over existing tools 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: 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: 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: Many of the ideas presented in the paper are known. However, the strength of the paper is in putting together these things, and backing up the results with implementation/experiments. 6. How WORTHWILE is the goal of the authors? Comment: The title is quite misleading. Clearly, there can be no polynomial-time algorithms for reachability even without time. More modest title like "Improvements in reachability analysis" or "Heuristics for reachability analysis" will be more appropriate. The goal suggested by these titles is one of the central themse in formal verification, and continued progress is quite desirable. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Satisfactory. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Satsifactory for a conference submission. 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: Experimental results are only preliminary. More comparison with Kronos/Uppaal is needed. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Satisfactory 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: Satisfactory. 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: 43 CATEGORY: 2 TITLE: Reachability Analysis of Timed Automata in Polynomial Time AUTHOR(S): Dirk Beyer -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper introduce a heuristic for the comparison of variable orderings in BDD based reachability analysis. A case study with a timed automata model (CTA) justifies its usefulness. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 =3D Out of scope 1 =3D Marginal interest 2 =3D Minority interest 3 =3D Majority interest 4 =3D Outstanding interest Numeric Rating: 2 Please comment your rating: Timed reachability is an interesting verification problem, since it captures many interesting properties of actual designs and nevertheless seems to be in the scope of algorithmic treatment. Due to the high computational complexity, the search for efficient or well-behaved techniques is a rather active field. Using BDDs as an efficient data structure for the search is an approach that deserves further exploration. A *new* part in this paper is the upper bound for the BDD size in dependency of the a given variable ordering. Regretfully, the one case-study reflecting this (Fischer Mutex) does not illustrate this very well, since there are only three samples of variable orderings, where the best one seems to be obvious. Thus, the paper is interesting for those who implement BDD based timed reachability and design heuristics to find good variable orderings. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 =3D Strong reject 2 =3D Weak reject 3 =3D Could go either way 4 =3D Weak accept 5 =3D Strong accept Numeric Rating: 2 NB: There should be a correlation between the two rates above. Comment: I consider the material interesting, but presented in a strange and misleading way. After serious revision, this could be a "4: Weak accept". 4. CONFIDENCE LEVEL: Please provide a rating of your expertise in the area addressed by the paper, using the scale: 1 =3D Know virtually nothing about this area 2 =3D Not too knowledgeable, but I know a bit 3 =3D Know a moderate amount, about average I'd say 4 =3D Not my main area of work, but I know a lot about it 5 =3D 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: I see the main contribution of this paper in the developing of a (numerical) qualification, that can used for the search of good variable orderings in a heuristic fashion (i.e. section 5.2). This is not restricted to CTA models, but can be applied whenever BDD bas= ed reachability analysis is performed on modular definitions (though the author does not address this). The other parts seem to be rather standard. 6. How WORTHWILE is the goal of the authors? Comment: Timed reachability analysis is both an interesting and (computationally) challenging problem. Many crucial feature of real-time critical software can be expressed in this logic. Efficient techniques - like finding good variable orderings in BDD based approaches - are very much needed, even if they cannot be proven to perform well in every case. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Timed reachability is motivated, though not to great detail. It took me some time to realize *what exactly* this paper offers. The argumentation for the presented heuristic needs some improvement, in particular a 'guarantee' (proof) to yield polynomial time reachability checks is never given (though title and abstract suggest it). I recommend changing the title and rewriting the abstract (see 12. (ii)). 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Basically yes. They also succeed in capturing the main concepts, with the exception of page11, top: "Comm_A" should be part of a definition, since it is a centr= al concept. Moreover, it should be clear that the *order* of components in A does immediately influence Comm_A. I did not check the proof of theorem 7 in detail, but the statement looks trustworthy to me. I had some trouble understanding the non-standard definition of BDDs, whe= re redundant tests are not eliminated. For some detailed remarks see 12 (iii). 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 given theoretical result (Theorem 7) is used as an estimate, in order to evaluate three different variable orderings. There is a clear 'applicable' relevance. I am concerned about the significance of the given data, mainly because a. the second example ('And4') does not compare different variable orderings b. the variable orderings appear to be chosen and *then* evaluated according to the estimation, and not vice versa. (We would like to be *guided* by the estimate in some way). 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: At various places, the content should be clarified and the writing style improved. In 12 (i)/(ii), I give some general and IMHO important suggestions. Detailed comments are given below. -------------------- page 1, middle: "... tools like Kronos [BDM + 98] and UppAal [LPY97]..." Should be Uppaal -------------------- page 1, middle: "... there is no canonical representation for clock valuatio= ns" This is, strictly speaking, untrue. DBMs *can* be restricted to a canonical form, but usually this does not improve the efficiency -- cf. e.g.: Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction. Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 14-24. San Francisco, California, USA, 3-5 December 1997 -------------------- page 1, middle: "...which often avoids efficient algorithms." Should be hinders the construction of -------------------- page 1, middle: "This means that our task is to find algorithms that solve t= he problem with polynomial space and time complexity." This is a unfortunate task, since we do not know, whether this is *possible* at all. Rather argue for "efficient algorithms / heuristics etc."= =2E "Polynomial space complexity" is usually not good enough in practice. -------------------- page 1, lower: "...modular model of a MOS circuit." You forgot to mention Fischer's protocol. -------------------- page1, lower: "...In Section 5 we explain the impact of the communication...= " You rather give an estimate to evaluate different variable orderings accordi= ng to the communication structure. -------------------- page2, Figure 1: Initially, "out" should be 0. Where do I see this? You do not mention it in the text. -------------------- page2, section 2.1: The typesetting with "'" is confusing, especially since you use primed variables in your drawing. I suggest italics for variables referenced in the =46igure, or, if possible, the same font (Helvetica?). -------------------- page2, middle: "...(as well as location 'Falling') is called unstable..." should be are -------------------- page2, below: "Discrete variables are provided to store discrete values." You seem to need something like read/write distinction. I did not find that = in your formalization. -------------------- page3, top: "...is is used to model systems containing subsystems,..." The semantics of your "subsystems" seems to be parallel composition, as oppo= sed to state-chart/hi-graph formalisms. It would help to clarify this. -------------------- page3, middle: "...the set of non-negative real numbers IR_+" AFAIK, IR^+ is more standard - or even IR^+_0 if you want it explicitly to include "0". Three lines below you choose delta \element IR_+, and here you probably want to exclude 0 (or delay transitions of time 0, in any case). -------------------- page3, middle: "... For a more compact notation discrete variables (which ha= ve a finite subset of the natural numbers as domain) are introduced which change their value only by location switches. Discrete variables are n= ot considered explicitly." You probably want to say that you allow them in your specification language, but translate the description to a discrete variable-free version for verification. Though sound in principle, this is unfortunately not that easy, since you ha= ve them also in invariants (gate =3D 0 in "Off") and guards (gate =3D 1). Thus,= you have to allow reference to *locations* in your grammar, which is missing. What is your system state, if "gate" changes from 0 to 1? I suggest that you give a sound translation of your syntactic sugar in order to resolve these details. You have an implementation, so you apparently know how it works. -------------------- page4, middle: [un]critical section should be region -------------------- page4, middle: "...behaviour of the AND gate con..." should be And4 or logical AND gate with four inputs -------------------- page4, lower: "...Automata are drawn as graph within a circle." should be graphs More importantly, you should explain what your diagrams aims to express. It seems to be a kind of data flow diagram, but this it not mentioned. Has this sort of diagram some standard name? -------------------- page5, top: "...The second part of Fig. 3..." Please give it a name like (i) (ii) and then refer to it. Moreover, you seem to confuse repeatedly "NAND" (the physical logic gate) an= d "Nand" (your model of it) and "nand" (your automaton). Or are they identical= ? I suggest another choice of names like A_{NAND} for the automaton and M_{NAN= D} for the model. -------------------- page5, top "The only difference to pMOS transistors is the inverse output value and that the pMOS transistors have to react at least 4 time units afte= r a change at the gate." This seem to be two differences. "at least" should probably be "at latest". -------------------- page5, top: "... How many transistors switch their state together at..= =2E" Should be can You probably want a worst-case behavior here. -------------------- page7, lower: "...typically the use symbolic representation of the locations= =2E" should be use of state space -------------------- page7, lower "...idespread use and also implemented in our tool." Please give name and reference here. -------------------- page7, lower "In this section we introduce a new technique for efficient verification of some classes of models." As I understand it, you give a new guideline to choose good variable orderin= gs. -------------------- page7, lower: "We prove the polynomial size of the representation of the transition relation." You should mention, that you do that (i) for one case study and (ii) for one specific variable ordering. The formula you develop in theorem 7 does not lo= ok "polynomial" to me. -------------------- page8, the two "characteristics": I suggest to make this more placative like e.g. Rule-Of-Thumb (I): Communicating components have successive... Rule-Of-Thumb (II): Components which communicate with many... (Fig.4) respect (I) =3D> better (Fig.5) both semi-respect (I) [one violation each] respect (II) =3D> better =46or some reason, you do not give variable ordering 2-1-3 in figure 5, whic= h should be the best (since it respects both (I) and (II)). -------------------- page 9, top: "The second characteristic of good variable orderings becomes obvious" Should be something like "We see that of two variable orderings the one respecting (II) is better." -------------------- page 9, middle: "In [ATB94] as well as in this paper it is demonstrated by empirical studies that this assumption is correct for many classes of systems." You have to admit that "many" is an exaggeration. It is good to give the reference to [McM92], but you have to state and motivate your choice more carefully. Moreover, the assumption can only "hold" and not be "correct" since it is no= t true in general [McM92]. -------------------- page9, middle: "...cause the estimation should only reflect the relation between different variable orderings," Apparently, you use the estimate to compare different variable orderings, so if they are all off by the same factor, it is of no consequence. How much does a bad estimate hurt in a heuristic? -------------------- page9, middle: "Last, not least upper..." should be Last, but not least Moreover, please correct the syntax in this sentence. -------------------- page9, middle: "...they correspond to both of the characteristics mentioned = =2E" should be seem to behave according to both ... -------------------- page9, middle: "...and these characteristics reflect the experience and intuition of many experts." If your make a claim like that, give a reference. -------------------- page9, lower: "...exists some v \element Val(V)," should be Val(X) -------------------- page9, lower: "...by renaming x by y;" should be x to y -------------------- page9, lower: "...v(x) =3D w(y) and v(z) =3D w(z) for all z \element X - {x}= " should be X \ {x} -------------------- page9, lower: "...also in the sequel of the paper." should be following. -------------------- page 10, Algorithm in figure 6: "...while R =3D\=3D R_prev..." should be until R =3D R_prev BTW: Your algorithm seems to need a parallel composition of *atomic* automat= a as input. Is this intended? -------------------- page10, top: "...For the proof we need a formal..." =46or what proof? -------------------- page10, middle: "Identify all equal subtrees. We do not ..." should be Fold together / share / ... "Identify" has ambiguous meanings here. -------------------- page10, middle: "...We do not eliminate nodes with two edges to the same..." Honestly, I do not see your motivation to deviate from the standard definiti= on. Do you maintain canonicity? How? Does your BDD package reflect this modification? Is this the "second rule" you do not apply? -------------------- page10, middle: Theorems 4,5 are rather propositions (or possibly lemmas). Theorem 6 should be called lemma. -------------------- page10, middle: "...For an assignment V \subseteq..." should be For a set of assignments V -------------------- page10, middle: "...regarding the variable in M..." After that, there seems to be a problem with the subtyping, which makes it hard to read. Apparently the problem are the primed variables that are typeset differently. Probably you should use a latex hack here like =2E..q_{1}^{\color{white}'}q_{1}^{'}.... to level them out. -------------------- page13, top: "...the size estimation should correspond as good as possible t= o the actual BDD size induced by the variable ordering." This is very vague. What does "as good as possible" express, since we know i= t is an estimate. Can you be more concrete here? -------------------- page13, top: "...do not contain ticked variables..." AFAIK, the term primed is the one in common usage. -------------------- page13, middle: "...The estimation contains the worst case assumption..." should be pessimistic bound (or something similar. It is *not* an "assumption".) -------------------- page 13, middle: "...But we need an algorithm of polynomial time complexity.= " ^^^^^^^ This is not clear at all, especially since the number of components is expected to be relatively small (compared to the number of bits you have to encode). I strongly recommend rewriting this subsection. You want to use your estimat= e, but cannot evaluate all possible permutations in general, right? So what do you do? Does the reference to [LLKS85] suggest that you do something similar= ? I think you should make a proposal here. -------------------- page13, middle: "...the algorithms described above can..." should be mentioned -------------------- page13, bottom: "...The problem of variable ordering is partitioned into smaller sub-problems" Can you devise a divide-and-conquer style algorithm? Is the outcome the same= ? If not, how does it relate? It seems to be a research question, so why not mentioning it under "future work" or "open problems". With "exact algorithms" - do you mean one doing an exhaustive search? You never classified the computational complexity of "finding the permutatio= n with the lowest estimated value." -------------------- page14, middle: "For the BDD B of all reachable configurations we get the estimation 1 for |B|_1 and |B|_{n+2} , and the estimation..." I am not sure what you are doing here. You seem to apply theorem 5, which yo= u did not introduce as an "estimation". At some point, you would like to inser= t in the formula given in theorem 7, right? This part would benefit greatly from a better exposition. -------------------- page 14, middle: "The last experiment shows that the estimation matches the actual size very good." and page 14, bottom: "seems to be polynomial using a good variable ordering (fif= th row)." Though your experiments suggest a slow growth, this does not "show" anything. It might demonstrate that your estimate is "relatively right", but you could as well fit a cubic function in there. Or an exponential one. Please remember that the O-notation does not say anything about finitely man= y values. -------------------- page 15: "...The main result of our paper is that we can compute good variab= le orderings and that the verification of timed... Our experimental results show that for some classes of models the reachability analysis seems to be of polynomial time and space complexity." Please polish your exposition! a. You do not compute "good variable orderings", but give a guideline to compare them. b. You suggested some methods to compute "approximately good" variable orderings without exhaustive search, but do not apply them (in your paper). c. Your experimental results corroborate that your guidelines correspond to low model checking times, but *not* that "reachability analysis seems to be = of polynomial time and space complexity", not even for "some classes of models"= =2E (If I am not mistaken, the *exact* bound you have is for the size of the *transition relation*.) ------------------------------------------------------------ 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: (i) layout page 6: Fig.3. needs a better layout, i.e. sub-captions or make it two figures. -------------------- page 15: Table 2.: Caption is too close to the table. ------------------------------ (ii) references page2, to: "...contain timed automata to describe its behaviour [BR98]." Your reference does not contain a behavioral description/operational semantic. Should that be [BR99] ? -------------------- page2, lower: "...complete semantics of CTA are given in [BR99]." Your reference should mention that there is a revised version available onli= ne (plus www address). -------------------- page 3, sec 2.3 "... timed automata similar to that introduced by Alur [Alu9= 9]" Here, a journal reference is more appropriate: R. Alur and D.L. Dill. A theory of timed automata. Theoretical Compute= r Science 126:183-235, 1994 ------------------------------------------------------------ 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: (i) General a. Taking "polynomial" as a synonym for "feasible" is dangerous. Though it i= s widely accepted as a working definition, it is not to be confused with a fact. You seem to do this at various places. b. Part of this work seems to be published in: Beyer, Dirk; Noack, Andreas: BDD-basierte Verifikation von Realzeit-Systemen. In Jens Grabowski and Stefan Heymer (editors): Tagungsband Formale Beschreibungstechniken f=B8r verteilte Systeme (FBT'00), pages 79-89, Shaker Verlag, Aachen, June 2000 Though this is in German language and thus not accessible to the internation= al community, I strongly believe it has to be mentioned in your paper! The relevant new part seems to be section 5, the upper bound/estimate for BD= D size. Somehow, however, I failed to see how this influences your case studie= s. ------------------------------ (ii) Title and Abstract a. Your title is very misleading. We know that timed reachability (even *without* parallel composition) is PSPACE complete (R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994). Moreover, you do not *prove* that your two examples can be model-checked in polynomial time, and you cannot infer that by case studies(!). The estimate (formula from Theorem 7) you give seems not to be restricted to a timed automat model or CTAs, but applicable whenever doing BDD based reachability analysis and the system is specified in a compositional way. I suggest something like: "A new heuristic to compare variable orderings in BDD based reachability analysis." -------------------- b. Some parts of the abstract need revision: l.2: "... for the representation." should be e.g. ... for the representation of the explored state space. l.3: "... this paper shows..." should be something like ... We use the communication structure to deduce an estimation for the BDD size. In our experiments, this guides the choice of good variable orderings. l.9: "... in the paper." (redundant) l.10: "...justify our assumption: Polynomial reachability analysis seems to = be possible for some classes of models." Strictly speaking, this is *not* an assumption but a fact: E.g. if all guard= s are simply "true", (timed) reachability is trivial. The question is rather: Can we *identify* interesting classes of examples where our technique performs well? Please be aware that the overall complexity prevents this in general (though= , P !=3D PSPACE is still a conjecture). Moreover, there are classes of example= s where *every* variable ordering leads to exponentially sized BDDs (e.g. multiplication). Thus there are known limits for BDD based analysis. -------------------- c. You should mention your tool implementation ("Rabbit"?) in the abstract a= nd give a reference at some point. ------------------------------ (iii) Technical remarks (other than writing style) a. I had trouble following your CTA references and find a formal definition. You refer to [BR99] Dirk Beyer and Heinrich Rust. A formalism for modular modelling of hybrid systems. Technical Report 10/1999, BTU Cottbus, 1999. A revised version is available online, but I did not find a definition of a *semantics* (e.g. in form of traces/runs etc.) there. In particular I am concerned about the encoding of discrete variables as locations. Though soun= d in principle, this makes it necessary to refer to locations of other components in your guards, e.g. "gate =3D 1" would correspond to a set of *locations* in an input automaton. I do not see that reflected in the syntax you define. -------------------- b. You mention to use 'your BDD tool' Rabbit, but I was not able to uncover = a accessible reference to it. It would be interesting to know *what* kind of B= DD package this is or whether it is an interface to well-known packages (like e.g. CMU/CU/CAL, as collected in the glu1.3 tool bundle, ftp://ic.eecs.berkeley.edu/pub/Vis/ ). BDDs behave very sensitive even to low-level implementation details. It is hard to make sense of your data (and the comparison with Kronos) without having access to those. -------------------- c. Your section 4 Discretization seems to be surplus. Do you give a new proof here (Lemma 2)? You do not seem to refer to anything particularly specific to your timed automata model. Why does it not suffice to state the fact that the reachability analysis is sound? -------------------- d. Your estimate does not seem to be limited to timed reachability analysis, but of more general interest. You should elaborate on that. ---------------------------------------- (iv) Related Work a. You mention that the transition relation is *not* encoded monolithically. There should be a reference, since the exact way *how* to decompose it is rather subtle and influences model checking times significantly. b. AFAIK there was a TCTL model checker developed by one of Ed Clarke's students at CMU, http://www.cs.cmu.edu/~modelcheck/verus.html. Though I don't think it is widely used or of practical relevance, it might b= e worthwhile to take a look at; as I take it from your text, it seems to be ve= ry related to "Rabbit". -------------------------------------------------- +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 43 CATEGORY: 2 TITLE: Reachability Analysis of Timed Automata in Polynomial Time AUTHOR(S): Dirk Beyer -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): 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: Verification of real-time systems is still one of the most challenging problems in formal verification. A satisfactory solution of this problem will expand significantly the scope of applicability of formal methods. Since the paper makes a meaningful contribution towards such a solution, its relevance is very high. 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 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: 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 paper does not contain any deep theory or theorems. Its main strength is in the combination of good methods for determining effective BDD variable ordering, as recommended by Aziz et al (reference [ATB] in the bibliographic list of the paper), with the observation that, for many classes of timed automata, the discrete semantics for the time-base is equivalent to the dense-time semantics ([HMP92] [BMPY97]). Previous experimentation with the discretization of dense-time automata produced poor results, which led to the conclusion that this approach is not effective. The current paper completely offsets this conclusion, providing compelling evidence that time discretization symbolically encoded by BDDs can lead to more efficient time analysis than the currently prevailing implementations. 6. How WORTHWHILE is the goal of the authors? Comment: As commented above, the conclusion that good implementations of BDD-based analysis of timed automata exist, is very valuable and may complete change the trend in implementation of time analysis tools. 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: They are. 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 about combining existing ideas in a successful way to obtain a highly efficient implementation. As such, the applicability value is very high. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality is 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: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++