Issue 98046 Editor: Erik Sandewall 17.5.1998

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

Iliano Cervesato, Massimo Franceschet, and Angelo Montanari
The Complexity of Model Checking in Modal Event Calculi with Quantifiers.
[summary]
[interactions]

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:

Discussion about received articles

Additional debate contributions have been received for the following article(s). Please click the title of the article to link to the interaction page, containing both new and old contributions to the discussion.

Iliano Cervesato, Massimo Franceschet, and Angelo Montanari
The Complexity of Model Checking in Modal Event Calculi with Quantifiers


Debates

Ontologies for time

Pat Hayes:

[S.B.]

  Suppose  S  consists of intervals from the real line. Assume  <s1,t1> in A  and  <s2,t2> in B , intervals in  S . We say that  <s1,t1> < <s2,t2>  iff $t1 leq s2$. The strict order relation $lt$ is an abbreviation for $leq and neq$.

[P.H.]
  It follows then that for intervals,   <   implies   <   except for pointlike intervals (single-point closed intervals) since if  t1 < s2 , the intervals  <s1,t1>  and  <s2,t2>  cannot be equal unless  s1 = t1 = s2 = t2 .

[S.B.]
    <   does not necessarily imply   <  , as in the case of  <2,5> < <5,9> , which is a valid case with respect to   <  .

Clearly,  <2,5>  is not equal to  <5,9> , ie  <2,5> =/ <5,9> . That is, both   <   and   =/   hold between those intervals. According to Sergio's definition (in italics above) it follows that the relation   <   must hold between them. In general, if  p  is not equal to  q , then the intervals  <p,q>  and  <q,r>  cannot be equal, so must be   =/  , but are also   <  , and therefore must be   <  . 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   (ab)   and   (bc)   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