N:o | Question | Answer(s) | Continued discussion |
---|---|---|---|
1a |
17.5 Paolo Liberatore |
24.5 Angelo Montanari |
|
1b |
17.5 Paolo Liberatore |
24.5 Angelo Montanari |
|
1c |
17.5 Paolo Liberatore |
24.5 Angelo Montanari |
|
1d |
17.5 Paolo Liberatore |
24.5 Angelo Montanari |
|
2 |
27.5 Peter Jonsson |
14.6 Angelo Montanari |
|
3 |
17.7 Rob Miller |
5.8 The authors |
Q1a. Paolo Liberatore (17.5):
Questions 1a and 1b are comments on the presentation; questions 1c and 1d are requests for clarification.
Page 2, col 2, second-last para: "We represent an MVI for
A1a. Angelo Montanari (24.5):
In the following, we quote a bigger paper excerpt, including the sentence:
"We represent an MVI for
Given an EC-structure H = (E, P, [.>, <.], ].,.[)
and a knowledge state w, the
Event Calculus (EC for short) permits inferring the maximal validity intervals
(MVIs) over which a property p holds uninterruptedly. We represent an MVI for p
as
|
We believe that reading the sentence in its context should allow one to
conclude that every MVI is 3-tuple
Q1b. Paolo Liberatore (17.5):
The definition of MVI states that between
A1b. Angelo Montanari (24.5):
We discussed this point in some detail in previous publications (cf. reference [4] as well as in [j-ci-12-359]. Your comment indicates that it is probably useful to add a brief explanation immediately after Definition 2.2.
In the following, we report part of the discussion provided in [4].
Definition 2.2 states that an event e interrupts the validity of a property
if it initiates or terminates p itself or a property q which is incompatible
with
Further details about the strong/weak distinction, including formalization and other examples, can be found in [4].
Q1c. Paolo Liberatore (17.5):
Page 9, col 1, para 3: the bound
A1c. Angelo Montanari (24.5):
An instance of the model checking problem we analyzed in the paper is a
triple
Given an EC-structure
The cardinality of
Finally, the size
Q1d. Paolo Liberatore (17.5):
Page 10, col 2, comment after Theorem 5.5: if
A1d. Angelo Montanari (24.5):
This last question is concerned with the following sentence, at the end of the complexity section:
The directness of the implementation allows checking easily that
the complexity of the implemented algorithms coincide with the bounds
proved in this section for the problems they implement."
|
"The directness of the implementation allows checking easily that the complexity of the implemented algorithms coincide, in the worst case, with the bounds proved in this section for the problems they implement."
However, we are convinced that the actual costs of the implemented versions of EC, ECMEC and EQCMEC are NOT close to the theoretical upper bounds, even though we have not empirical evidence of this fact.
Take, for example, the case of EQCMEC. Here, the critical factor is the
level of nesting of quantifiers. The worst case holds when we have an
EQCMEC-formula involving
Furthermore, as mentioned in the paper, practical applications using modal event calculi with quantifiers are expected to model situations involving a large number of events, while the size of the queries, and in particular the nesting of quantifiers, will in general be limited. The hardware fault diagnosis example falls into this category (the nesting level of quantifiers is 2).
Finally, it is possible to show that the upper bound of
From the above elements, it follows that the hardware fault diagnosis problem
can actually be solved in
Q2. Peter Jonsson (27.5):
Comments and questions to the authors:
Page 4, col 1, para 2: Please find a better name than "condition (*)".
Page 6, col 1, para 3: You write "The best approximation of /formula/ we can achieve...". In what sense is it the "best" approximation?
Chapter 4 "Implementation". I agree that the implementation of QCMEC
in
Page 8, before Th. 4.1: You write "We only show the statement of our
soundness and completeness result since a fully worked out proof would
require a very detailed account of the semantics of
Chapter 5 "Complexity Analysis" Why not rearrange the section as follows: Begin the section by proving that QCMEC is in PSPACE. Then there is no need for first showing that CMEC is in PSPACE, extending the result to EQCMEC and finally realize that the proof for EQCMEC also works for QCMEC.
Page 8, col 2, proof of Th. 5.3.: You write "...the algorithm enters in
an AND (resp. OR) state. It nondeterministically choose one among
Page 10, col 1, end of proof of Th. 5.3. Please give the proof of why
Page 11, col 1: You write "In Section 4 we have transliterated the definition
of QCMEC and its subcalculi in the higher-order logic programming
A2. Angelo Montanari (14.6):
Page 4, col 1, para 2: Please find a better name than "condition ()".
|
Page 6, col 1, para 3: You write "The best approximation of /formula/
we can achieve...". In what sense is it the "best" approximation?
|
Chapter 4 "Implementation". I agree that the implementation of QCMEC
in
|
We did not consider efficiency issues. We would ourselves be very surprised if our lambda-Prolog implementation of QCMEC were to do better than even a naive C implementation. However, it is not our goal to compare the efficiency achievable with different programming languages.
Page 8, before Th. 4.1: You write "We only show the statement of our
soundness and completeness result since a fully worked out proof would
require a very detailed account of the semantics of
|
This was the logician's answer. The vast majority of the people who are likely to cast their eyes on our work will be interested in the more intuitive aspect of a correctness proof that we call immediacy: how far apart is the implementation from the formalism it implements? Here, our lambda-Prolog implementation is a direct transliteration of the specification of the semantics of QCMEC. It would not be so had we used C.
Chapter 5 "Complexity Analysis" Why not rearrange the section as follows:
Begin the section by proving that QCMEC is in PSPACE. Then there is
no need for first showing that CMEC is in PSPACE, extending the
result to EQCMEC and finally realize that the proof for EQCMEC also
works for QCMEC.
|
Page 8, col 2, proof of Th. 5.3.: You write "...the algorithm enters in
an AND (resp. OR) state. It nondeterministically choose one among
|
By definition, the alternating machine accepts an AND-state configuration (resp., an OR-state configuration) if and only if all (resp., al least one) of its successor configurations are accepting configurations. Thus, the distinction bewteen AND states and OR states comes into play in the definition of acceptance.
It is worth noting that given a problem, a nondeterministic
algorithm for this problem does not solve it. Given a "yes"
instance of the problem and a succint certificate for it, the
nondeterministic algorithm only checks that the instance is
indeed a "yes" instance of the problem by exploiting the
certificate.
For example, in the case of SAT, given a satisfiable propositional
formula
Notice also that AP is equal to PSPACE, that is, finding an alternating polynomial time algorithm for a given problem allows us to conclude that the problem can be solved in polynomial space. Thus, it is not surprising that the behaviour of the algorithm in an AND and in an OR state is the same, since the space requirements in both states are the same.
See [12] (chapter 16) for further details.
Page 10, col 1, end of proof of Th. 5.3. Please give the proof of why
|
| \Diamond \hat{F} | if k = n | F_k = | \Diamond (\psi_{k+1} \And \Box \hat{F}) | if k = n-1 | | \Diamond (\psi_{k+1} \And | \Box (\psi_{k+2} \Impl F_{k+2})) otherwise
Coming back to your question, we will now provide further details in order to help the reader to understand the proof.
Let G be a QBF with variables in
A knowledge state
If
In the proof, we exploit this correspondence in order to map the
propositional quantifiers of a QBF into the modal operators
of a CMEC-formula. However, there is a technical problem with
this solution: the scope of a quantifier is limited to the
variable that it quantifies, whereas the scope of a modal
operator in the formula
We invite the skeptical reader to make some small examples with two or three nested quantifiers.
Page 11, col 1: You write "In Section 4 we have transliterated the definition
of QCMEC and its subcalculi in the higher-order logic programming
|
Q3. Rob Miller (17.7):
Dear Iliano, Massimo and Angelo,
I've several questions about your paper "The complexity of Model Checking in Modal Event Calculi with Quantifiers" submitted to the ETAI.
Generally, I would like to understand the relationship between the modal logic event calculi you describe and refer to in your paper and the classical logic versions of the event calculus that people such as myself and Murray Shanahan use. So any remarks you have in this respect would be helpful. Here are some more specific questions related to this:
"Pushing causes the door to open if it's not locked" "The door was pushed at 9 o'clock"(In the classical logic variants of the event calculus, you'd write formulas such as
(FORALL t).[Initiates(Push,Open,t) <- NOT Holds(Locked,t)]. Happens(Push,9).
Apologies if answers to these questions are already to be found in the other papers to which you refer. As a proponent of "the event calculus" I regret not knowing more about your previous work.
Rob
C3-1. Iliano Cervesato, Massimo Franceschet, and Angelo Montanari (5.8):
Dear Rob,
Thank you very much for your questions. In the following, we provide you with some remarks about our modal event calculi that hopefully will contribute to clarify the questions you raised.
Generally, I would like to understand the relationship between the modal
logic event calculi you describe and refer to in your paper and the
classical logic versions of the event calculus that people such as myself
and Murray Shanahan use. So any remarks you have in this respect would
be helpful. Here are some more specific questions related to this:
|
Roughly speaking, the original Event Calculus (EC) is a simple temporal formalism designed to model situations characterized by a set of events, whose occurrences have the effect of starting or terminating the validity of determined properties. Given a description of when these events take place and of the properties they affect, EC is able to determine the maximal validity intervals (MVIs) over which a property holds uninterruptedly.
We focused our attention on situations where only partial information about the ordering of event occurrences is at our disposal. More precisely, we limited our investigation to problems consisting of a fixed set of events that are known to have happened, but with incomplete information about the relative order of their occurrences. In these situations, the MVIs derived by EC bear little relevance since the acquisition of additional knowledge about the actual event ordering might both dismiss current MVIs and validate new MVIs. It is instead critical to compute precise variability bounds for the MVIs of the (currently underspecified) actual ordering of events. In [7,8], optimal bounds have been identified in the set of necessary MVIs and in the set of possible MVIs. They are the subset of the currents MVIs that are not invalidated by the acquisition of new ordering information and the set of intervals that are MVIs in at least one extension of the current ordering of events, respectively. In [1], we proposed a Modal Event Calculus (MEC), which, given a possibly incomplete specification of the ordering of event occurrences, extends EC with the possibility of inquiring about MVIs (MVIs computed by the original calculus), necessary MVIs (MVIs which hold in all extensions of the given ordering), and possible MVIs (MVIs which hold in at least one extension). In [3,4,5,6], we generalized such a modal framework to model effectively significant situations (we considered case studies taken from the domain of hardware fault diagnosis). We defined a number of modal event calculi that allow a free mix of modal operators, boolean connectives and preconditions, focusing on the interactions between modal operators and boolean connectives in [3,4], and between modal operators and preconditions in [6]. In [5], the expressiveness and complexity of the resulting hierarchy of modal event calculi are systematically investigated. In the ETAI paper, we further extend our modal event calculi by admitting arbitrary event quantifications.
Other differences between our modal event calculi and the classical logical versions of EC, that are worth mentioning, are the following:
|
As described above, at the beginning of our research work (cf. [7,8]), we restricted our attention to complete actual courses of events, whose temporal ordering, specified by means of a set of ordered pairs of events, is only partially known. The considered scenarios are thus characterized by a set of occurred events, which is fixed once and for all, and does not include concurrent or divisible events, and by incomplete (but consistent) information about an actual total order, given in terms of the relative order of pairs of event occurrences. Modal EC (cf. [1]) allows one to determine the sets of MVIs, necessary MVIs, and possible MVIs, and to constrain their evolution as further (consistent) information about the ordering (that is, further pairs of ordered events) is added.
However, most of the restrictions of the original Modal EC (which, by inertia, we do not explicitly remove from its successive generalizations [3,4,5,6]) can actually be relaxed:
All the proved results, indeed, do not rely on such restrictions.
|
According to the proposed approach, the meta-predicate "br" does not belong to any modal query language (syntax); it comes into play in the definition of the intended models of our modal languages (semantics) as well as in their implementations.
Obviously, nothing prevents us to extend query languages to allow one to retrieve information about, for instance, the initiating and terminating maps. Our original (and current) goal, however, was to support queries about (any combination of) MVIs only.
would help. How roughly might you express information such as: |
"Pushing causes the door to open if it's not locked"
"The door was pushed at 9 o'clock" |
(In the classical logic variants of the event calculus, you'd write
formulas such as
|
Such as example can be easily expressed in the Event Calculus with preconditions (PEC) described in [6]. A structure for PEC (PEC-structure) differs from an EC-structure for the addition of a context argument to the initiating and terminating maps (that specifies the set of preconditions that must hold in order that an event actually initiates or terminates a given property) and the removal of the exclusive relation (the presence of preconditions in PEC permits an easy emulation of the exclusivity relation).
We express the condition that
"pushing causes the door to open if it's not locked" |
Let OPEN and UNLOCK be two properties, and PUSH, SHUT, KEY_L, and KEY_R be four events. The event PUSH initiates the property OPEN with precondition UNLOCK, that is, a push event opens the door if it is unlocked. Moreover, the event SHUT terminates the property OPEN with no preconditions. Finally, the event KEY_L initiates the property UNLOCK, while the event KEY_R terminates it.
It is worth noting that, for simplicity (as in the original Kowalski and Sergot's EC paper), we usually define the initiating and terminating maps in terms of event occurrences and property types. In such a case, the initiating map only includes information stating that the occurred PUSH event initiates the property OPEN if the property UNLOCK holds at its occurrence time, while the terminating map provides no information.
However, it is not difficult to redefine the initiating and terminating maps in terms of event and property types, and to properly instantiate them when an event of the given type occurs (we detailed such an approach in some of our early papers on EC). In such a case, the initiating and terminating maps can be used to model all the above described event and property relationships; moreover, the relationship between the event PUSH, the property OPEN, and the precondition UNLOCK is instantiated for the given occurrence of an event of type PUSH.
Furthermore, we express the fact that
"the door was pushed at 9 o'clock" |
We do not associate explicit times with event occurrences (we model temporal information by a strict partial order over the set of occurred events), but we exploit temporal knowledge provided by explicit timestamps to obtain information about the relative ordering of event occurrences.
Aside. We only consider positive preconditions. For this reason, we introduce the condition UNLOCK. However, as long as we restricted ourselves to acyclic dependencies among properties (as we did in [6]), it is not difficult to generalize our notion of PEC-structure in order to support both positive and negative preconditions.
Additional questions and comments, as well as the answers from
the author(s), will be added into this
structure. They will also circulated by email to the area subscribers.
To contribute, please click Msg to moderator in the column
to the right, send your question or comment as an E-mail message.
For additional details, please click Debate procedure
there.
This debate is moderated by Erik Sandewall.
The present protocol page was generated automatically from
components containing the successive debate contributions.