******************************************************************** ELECTRONIC NEWSLETTER ON REASONING ABOUT ACTIONS AND CHANGE Issue 98046 Editor: Erik Sandewall 17.5.1998 Back issues available at http://www.ida.liu.se/ext/etai/actions/njl/ ******************************************************************** ********* TODAY ********* Today's issue contains the summary (longer and more concrete than an ordinary abstract) of the article by Cervesato, Franceschet, and Montanari which was recently received by the ETAI. Also, we have an invited comment-and-question contribution by Paolo Liberatore for the same article. We have been using summaries since the beginning of ETAI as a help for readers to orient themselves rapidly in recent results. The use of invited commentary is a more recent idea. One more invited comment for the same paper has been promised. The present Newsletter issue also contains a contribution by Pat Hayes to the discussion about ontologies of time. After a quite long debate, it seems that the dust is beginning to settle there. ********* ETAI PUBLICATIONS ********* --- RECEIVED RESEARCH ARTICLES --- ======================================================== | AUTHOR: Iliano Cervesato, Massimo Franceschet, and Angelo Montanari | TITLE: The Complexity of Model Checking in Modal Event Calculi | with Quantifiers | PAPER: http://www.dimi.uniud.it/~montana/kr98.ps | REVIEW: http://www.ida.liu.se/ext/etai/received/actions/007/aip.html ======================================================== SUMMARY: The Event Calculus The *Event Calculus*, abbreviated *EC*, is a simple temporal formalism designed to model and reason about scenarios characterized by a set of *events*, whose occurrences have the effect of starting or terminating the validity of determined properties. Given a *possibly incomplete* description of when these events take place and of the properties they affect, *EC* is able to determine the *maximal validity intervals*, or *MVIs*, over which a property holds uninterruptedly. State-of-the-art A systematic analysis of *EC* has recently been undertaken in order to gain a better understanding of this calculus and determine ways of augmenting its expressive power. The keystone of this endeavor has been the definition of an extendible formal specification of the functionalities of this formalism. This has had the effects of establishing a semantic reference against which to verify the correctness of implementations, of casting *EC* as a model checking problem, and of setting the ground for studying the complexity of this problem, which was proved polynomial. Extensions of this model have been designed to accommodate constructs intended to enhance the expressiveness of *EC*@. In particular, modal versions of *EC*, the interaction between modalities and connectives, and preconditions have all been investigated in this context. Contributions The main contributions of the present paper are the following: - *The extension of a family of modal event calculi with quantifiers*. We enhance the expressive power of *EC* by considering the possibility of quantifying over events in queries, in conjunction with boolean connectives and modal operators. We also admit requests to check the relative order of two events. We thoroughly analyze the representational and computational features of the resulting formalism, that we call *QCMEC*@. We also consider two proper sublanguages of it, *EQCMEC*, in which modalities are applied to atomic formulas only, and *CMEC*, which is quantifier-free. - *The use of the proposed formalisms to encode diagnosis problems*. We consider a case study taken from the domain of hardware fault diagnosis. We model it using *EC* and use the various extensions of *EC* to draw conclusions about it. - *The use of the higher-order features of modern logic programming languages in temporal reasoning*. We provide an elegant implementation in the higher-order logic programming language $greek(lambda)$*Prolog* and prove its soundness and completeness. - *Analyzing the complexity of model checking in the proposed extensions of EC@*. We prove that model checking in *CMEC*, *EQCMEC*, and *QCMEC* is **PSPACE**-complete. However, while solving an *EQCMEC* problem is exponential in the size of the query, it has only polynomial cost in the number of events, thus making *EQCMEC* a viable formalism for *MVI* verification or computation. Since in most realistic applications the size of databases dominates by several orders of magnitude the size of the query, the former is asymptotically the parameter of interest. --- DISCUSSION ABOUT RECEIVED ARTICLES --- The following debate contributions (questions, answers, or comments) have been received for articles that have been received by the ETAI and which are presently subject of discussion. To see the full context, for example, to see the question that a given answer refers to, or to see the article itself or its summary, please use the web-page version of this Newsletter. ======================================================== | AUTHOR: Iliano Cervesato, Massimo Franceschet, and Angelo Montanari | TITLE: The Complexity of Model Checking in Modal Event Calculi | with Quantifiers | PAPER: http://www.dimi.uniud.it/~montana/kr98.ps | REVIEW: http://www.ida.liu.se/ext/etai/received/actions/007/aip.html ======================================================== -------------------------------------------------------- | FROM: Paolo Liberatore -------------------------------------------------------- Comments on presentation Page 2, col 2, second-last para: "We represent an MVI for p as p(e_i,e_j) ...". I found this sentence a little misleading. Indeed, the notation p(e_i,e_j) refers to *any* 3-tuple . The aim of queries is to decide whether such a 3-tuple is a MVI. From the sentence written in the paper, it seems that p(e_i,e_j) is used to *state* that e_i,e_j is an MVI for p. Perhaps this sentence should be rewritten in some way. The definition of MVI states that between e_1 and e_2 there is no event that initiates p. I would like you to spend a few words for explaining why. Questions to the authors Page 9, col 1, para 3: the bound O(n^2) for reachability is due to the fact that you consider the number of events as the size of the input. Indeed, reachability in a graph is linear in the total size of the graph, that is, is O(n+m), where n is the number of vertices and m is number of edges. This implies for example that the cost of EC is O(s^2), if s is the total size of the input and not only the number of events. Is there any reason for choosing the number of events to represent the size of H? Page 10, col 2, comment after Theorem 5.5: if k is just a bit high (for instance, 4), the cost of solving the problem becomes something in the order of O(n^7), which is usually considered not very useful. In the conclusions, you mention that the cost of the implemented version of QCMEC is very close to the theoretical value. Do you have empirical evidence that the efficiency of EQCMEC is also similar to the upper bound you proved? If so, the problem should be considered not actually feasible. ********* DEBATES ********* --- ONTOLOGIES FOR TIME --- -------------------------------------------------------- | FROM: Pat Hayes -------------------------------------------------------- [S.B.] >>> Suppose $S$ consists of intervals from the real line. Assume >>> $ \in A$ and $ \in B$, intervals in $S$. We say that >>> $ \leq $ iff $t1 \leq s2$. ****The strict order relation >>> $\less$ is an abbreviation for $\leq \logical-and \noteq$.**** [P.H.] >> It follows then that for intervals, $\leq$ implies $\less$ except for >> pointlike intervals (single-point closed intervals) since if $t1 \leq s2$, >> the intervals $$ and $$ cannot be equal unless >> $s1=t1=s2=t2$. [S.B.] > $\leq$ does not necessarily imply $\less$, as in the case of > $<2,5> \leq <5,9>$, which is a valid case with respect to $\leq$. Clearly, $<2,5>$ is not equal to $<5,9>$, ie $\not-eq( <2,5>, <5,9> )$. That is, both $\leq$ and $\not-eq% hold between those intervals. According to Sergio's definition (marked **** above) it follows that the relation $\less$ must hold between them. In general, if p is not equal to q, then the intervals and cannot be equal, so must be \noteq, but are also \leq, and therefore must be \less. The rest of his message in ENRAC 4.5 (98042) makes the same error, and the subsequent confusion has been noted by Jixin in the later discussion. Sergios point seems to be that one can describe the line in terms of conventional open and closed intervals in such a way that no 'gaps' appear, so that the 'interval' between the open intervals (a,b) and (b,c) is the closed interval [b] containing a single point. Yes, of course: that is not at issue. We are not claiming to have found some basic flaw in conventional real analysis. The question is whether this standard mathematical view of the line is the most suitable for capturing linguistic intuition or for action reasoning. For example, we want to be able to assert that a light is off before time t and on after time t without having to committ ourselves to its being either on or off AT that time, but also without sacrificing the assumption that it is always either on or off. Of course we could just decide that periods of off-ness, say, shall be left-open-right-closed, or some other convention: but this is arbitrary, ad-hoc and theoretically unsatisfactory, since the intuition we would like to capture is that the question (of the light being on or off at b) simply doesnt arise: it just *goes* on then, that's all. That is the intuition which Allens interval calculus, where intervals can simply *meet*, is intended to capture. The fact that this calculus violates Sergios pet axiom doesnt seem to be a very important matter for further discussion. In any case, many users of temporal ontologies do not wish to assume continuity or even density, for reasons of their own, and so a general-purpose temporal ontology should therefore not make such unnecessarily strong assumptions as Sergio's 'completeness' axiom. Temporal database technology usually assumes times are discrete, for example. Pat Hayes ******************************************************************** This Newsletter is issued whenever there is new news, and is sent by automatic E-mail and without charge to a list of subscribers. To obtain or change a subscription, please send mail to the editor, erisa@ida.liu.se. Contributions are welcomed to the same address. Instructions for contributors and other additional information is found at: http://www.ida.liu.se/ext/etai/actions/njl/ ********************************************************************