++++++++++++++++++ FME2001: - Review reports for paper 21 +++++++++++++++++++++ - 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: 21 CATEGORY: 2 TITLE: Real-Time Logic Revisited AUTHOR(S): Stephen Paynter -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper revisits the Real-Time Logic (RTL) of Jahanian and Mok (1986). The author proposes some generalisations to make RTL more suitable for specification of real-time and hybrid systems. 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: Quite relevant to those interested in real-time systems specification. 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: 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 originality is the generalisation of RTL to make it suitable for a wider range of applications, without making much more complex. 6. How WORTHWHILE is the goal of the authors? Comment: The improvements to RTL are well worth considering. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Very well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The technicalities of the paper contain some errors. I'd hazard a guess that they were put together for the deadline for FME. No problems that couldn't be fixed for the conference. p4 sect 3 para 2 Although the rationals are countable the usual enumeration of them doesn't follow the conventional ordering of the rationals. p5 "An infinite occurrence ..." Such a property could be expressed if one allowed quantification over infinite sequences. I am worried by the fact that actions may take no time and occur at the same time but there is no ordering between such actions. p6 exists near bottom of page first line: last t should be t_1 second line: last t should be t_2 p7 top Modelling a variable value as a function of Time seems reasonable. However, this only allows a variable to have a single value a any one time. This is a problem if one wants instantaneous actions that change the value of variables (one can't model the variable value) and is exacerbated if multiple actions are allowed at the same instant of time. The example (\forall t: Time @ v_1(t) = v_2(t) \implies \psi(e,t) is a bit dubious, because it will (almost certainly) be the case that two variables will be equal over a contiguous interval of time. That would lead to an uncountable number of e events. When dealing with predicates the notation would benefit from having some way of refering to intervals of time. In both the rises and falls predicates, in the second part of each the "t = 0" disjunct should be omitted. For example, for rises consider the case when P(V(t)) is false over an interval starting from 0 (inclusive) -- the current definition gives a rise event at time 0. The type of falls should have an Event as well. hold_over I expected t_1 \leq t \leq t_2 (at least that seems more sensible to me). hold_until and hold_since I'm not sure what the purpose of the event e is in the definition of hold_until. It seems that one could define predicates rising or falling without worrying about there being an event associated with it. At the moment it seems one would have to just invent such events. (I suppose one could use an event name that corresponds to the rising of the predicate.) p8, duration The definition of duration seems very complicated when compared to the DC approach. p9 mid For the purposes of this paper it would seem sufficient to give an abstract syntax and not worry about parentheses etc. p10 Table 2 What does the hypothesis "x_0" mean (forall introduction and exists elimination). Perhaps it should be "x_0 \in S" ? One also needs an "x_0 not free in \alpha" for this rule to be valid (consider \alpha being "x = x_0"). The sorting (typing) of variables doesn't seem to be fully treated. For example, for equality (t_1 = t_2) are t_1 and t_2 required to be the same type? For \forall elimination doesn't one require t to be of type S before this can be applied. p12, Th 3 Is "i > 0" redundant? It is unclear whether Occ is N or N+ ? Sect 7 The periodic predicate is rather strict on it requirements of exactly when the event occurs. But worse, it doesn't actually require event e to occur at all, it only constrains when it happens *if* it happens. Sporadic has similar problems. "or miat" -> "(miat)" --- or just omit as it isn't used. p13 window This definition allows multiple occurrences of e to occur in a single window, and it allows *no* occurrences of e in the window. All it requires is that every occurrence of e is in a window. Is this what is intended? If so, improve the text discription to make this clear. jitter This seems to assume the clock is periodic? But it does not require that there is an ith occurrence of an event. COB Does not require events i or i+1 to occur. p14 In PVS does NONEMPTY_TYPE imply the type is countable? (finite?) "th" and "psi" are not very meaningfull names. I know they weren't your choice of Greek letters, but it seems perverse to use the ASCII names of the Greek letters when one could use a more meaningful name. Also the axiom names could be more meaningfull than "RTLax1" ... In RTLax2 "t3" should be "t2" to be consistent with page 4. RTLax5 swaps t1 and t2 wrt page 6. RTLax6 likewise. The presentation of the PVS axioms adds little to the paper as they are virtually identical to those given earlier except for the concrete syntax (which isn't all that important). What would be more interesting is where representation choices are required in the PVS, or non-trivial encodings (i.e., other than change of concrete syntax). p15 para 3 "``the pump may be turned ?? no more..." Do you mean "on" or "off" or both. para 4 What does "predicate P holds for the ith time" mean when time is continuous and P could hold over a contiguous interval. 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 primarily a generalisation of an existing technique. The examples given in the paper illustrate its use reasonably well. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Well written. p3 sect 2 para after @ make it clear that you use N rather than N+ in the paper. Remove indentation here and after theta. p6 after ax 5 "executed by sequentially" -> "executed sequentially" p7 and p15 "secord" -> "second" Sect 5.3 line 6 drop "special" 4. "pairs" -> "pair" 5. "if Eq(I(e_1,e_2)" -> "if Eq(I(e_1),I(e_2))" last paragraph of Sect 7 could be moved to the start of the section. 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: 21 CATEGORY: 2 TITLE: Real-Time Logic Revisited AUTHOR(S): Stephen Paynter -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper represents RTL in classical many-sorted logic with real and integer arithmetic. It allows RTL time to be continuous, and models RTL functions using predicates over timed variables. The paper also shows a shallow embedding of RTL in the PVS logic. 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 treatment of RTL in MSL is useful to support the following extensions: (1) continuous time. (2) quantification over events (3) instantaneous actions The ability in RTL to refer to the number of occurrences of an event also makes it relatively easy to specify properties such as an event can not occur more than x times in any interval of length y. 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: Adding new features into RTL in support of specification of real time systems. A shallow embedding of RTL in PVS 6. How WORTHWHILE is the goal of the authors? Comment: The extension is worthwhile when it is shown in Section 7 that how some common real-time requirements can be described using the RTL notation in a very simple way. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The motivation of the work is well-explained. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: the technical results are sound, and the examples of Section 7 provide some validation of the RTL notations by showing that it is capable of expressing simply and clearly these common requirements. 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 favour of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: for further exploration. 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?: Are the figures and length acceptable?: Are the references correct?: Please add some reference to ITL. 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: 21 CATEGORY: 2 TITLE: Real-Time Logic Revisited AUTHOR(S): Stephen Paynter -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes a new semantics for Real-time Logic (RTL) where time is now treated as dense. The semantics is formulated using many sorted logic with real and (I presume) integer arithmetic. 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: RTL is one of the early logics for specifying properties of real-time systems. 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. 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: Weak paper. The paper attempts to give new semantics to RTL where time is treated as dense. Much of the technical development is routine. Axioms are shallow and in no sense comprehensive. There are hardly new insights as there are many dense-time logics in literature. Monadic theories of time are also well-established and go well beyond what authors formulate. There is no formal analysis of expressive power of proposed logic. 6. How WORTHWILE is the goal of the authors? Comment: It extends RTL to dense time so this may be of interest to RTL community. However, now there are many well established logics with dense time and the reformulated logic, in my opinion, hardly offers anything beyond these. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Moderately well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: POOR. There are techincal mistakes. See comments to author. The paper attempts to reformulate RTL with dense time. Since one of the main concepts in RTL is occurrence number of an event, a Finite Occurrence Density Property has to be imposed. The axiom for finite occurrence property (AX3, page 4) is inadequate. A counter example is given in comments to author. There are also issues on counting beginning and ending of actions. I found the selection of axioms and theorems of RTL very ad hoc and in no way comprehensive (complete). 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 is reformulation of RTL (an old logic for timed systems) for dense time. Thus, it would presumably allow the kind of case studies 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Reasonable. Section 5 can be considerably shortened as Many Valued Logic is well established in literature. There are standard axioms for this logic which are even implemented into theorem provers such as HOL and PVS. Thus section 5.3 can be omitted. Only the section 5.4 is of some value as this defines the primitives used to formulate RTL. This can be expanded. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes (except section 5 which can be shortened) Are the references correct?: yes. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The paper is an attempt to reformulate RTL with dense time. Since the main concept in RTL is occurrence number (count) of an event, a Finite occurrence property has to be imposed on interpretations. (1) Axiom AX3 page 4 is claimed to impose finite occurrence density (FOD). This is not adequate. Consider a behaviour where event e occurs exactly at times 1, 1+1/2, 1+1/2+1/4, ... Note that there is NO e event at time 2 or afterwards. Then, within an interval [0,2] there will be infinitely many e occurrences. However axiom Ax 3 is still satisfied. (2) Page 5 After AX4 "It is noted that all finite occurrence properties could be expressed using psi instead of theta." This is not true. For predicates of the form theta(e,c,t) where c is a constant, this is true but RTL in general allows one to use variables and terms e.g. theta(e,i+1,t) which cannot be formulated using psi. (3) Page 6 Axioms 5, 6 for begin and end of actions. These are confusing. Can several occurrences of an action overlap? Suppose action a occurs in interval [3,5] and also in interval [4,5] How should theta(end(a),i,5) be calculated. Note that two occurrences action a end at same time so occurrence count of end(a) at time 5 is not well defined. MINOR Comments: -------------- Author comments on his distaste for implicit versus explicit time on page 5. Apart from opinion there are no technical arguments here. This debate is as old as modal logics. Most modal logics can be expressed in classical logics with variables ranging over worlds and having a relation symbol for accessibility relation. Still they are virorously being pursued and used with good and well known reasons. Author should consult a good handbook article on modal logic for real import of modal logics (and use of implicit time in temporal logics). +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++