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

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:

• 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  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.

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
   Review protocol: [in this pane]; with links: [frame] [noframe]

Debates

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 < s2 . The strict order relation   <   is an abbreviation for   <  ^  =/  .

[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   (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 commit 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