******************************************************************** ELECTRONIC NEWSLETTER ON REASONING ABOUT ACTIONS AND CHANGE Issue 98062 Editor: Erik Sandewall 5.8.1998 Back issues available at http://www.ida.liu.se/ext/etai/actions/njl/ ******************************************************************** ********* TODAY ********* Today, responses by authors for two ETAI submitted articles. ********* ETAI PUBLICATIONS ********* --- DISCUSSION ABOUT RECEIVED ARTICLES --- The following debate contributions (questions, answers, or comments) have been received for articles that have been submitted to 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: authors -------------------------------------------------------- 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: Let us briefly run again along the path that led us to develop our set of modal event calculi. 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: - we provided EC with a model-theoretic formalization by means of the notions of EC-structure (which specifies the set of event occurrences, the set of relevant properties, the initiating and terminating maps that respectively associate each property with the events that initiate and terminate it, the exclusivity relation that identifies incompatible properties), knowledge state (a strict partial order over the set of occurred events), EC query language (the set of all property-labeled intervals over the EC-structure), and EC intended model (the set of MVIs computed by EC); - we generalized such a formalization to all modal event calculi we proposed; the generalization actually consists in the extension of the EC-structure to deal with preconditions, of the (modal) query language to encompass modal operators and boolean connectives, and of the intended model to cope with the additional structural and/or linguistic features; - we gave sound and complete implementations of the various modal event calculi in higher-order logic programming languages (hereditary Harrop formulas, lambda-Prolog). > * Do you see your formalisms as what we describe as "narrative" > formalisms - i.e. formalisms in which the flow of time is described > independently of any actions that occur? > > * Is the underlying concept of time linear? By "partial order" of events, do > you mean "incomplete information about a total order", or are your > techniques applicable to genuinely partially ordered time structures > (such as the forward branching time structure employed by many versions > of the Situation Calculus)? 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: - completeness of the set of event occurrences (we can have incomplete knowledge about both the event occurrences and their temporal ordering); - occurred events only (the events can be either actual events or hypothetical ones). All the proved results, indeed, do not rely on such restrictions. > * I'm confused about the syntax of your language(s). Are there any > meta-predicates in your language other than "br"? Perhaps some examples 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 > > (FORALL t).[Initiates(Push,Open,t) <- NOT Holds(Locked,t)]. > Happens(Push,9). > ) 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" by using the initiating and terminating maps of the PEC-structure as follows. 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" by stating that the set of occurred events of the PEC-structure only includes an occurrence of a PUSH event. 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. ======================================================== | AUTHOR: Marc Denecker, Daniele Theseider Dupre, and Kristof | Van Belleghem | TITLE: An Inductive Definition Approach to Ramifications | PAPER: http://www.ida.liu.se/ext/epa/cis/1998/007/tcover.html | [provisional] | REVIEW: http://www.ida.liu.se/ext/etai/received/actions/009/aip.html ======================================================== -------------------------------------------------------- | FROM: authors -------------------------------------------------------- Dear Eugenia, > Thank you for your answers to my questions. These answers clarify an > important difference between our works. > > Using generalized inductive definitions to detect ill-defined literals is > the advantage of your work. > > However, after 2-valuedness is shown, all reasoning involving multiple > models have to be performed on the metamathematical level. In contrast, > first order logic augmented with inductive definitions allows us to work > with all models at once therefore allowing for incomplete information. > Perhaps your approach could be developed in this direction, but you do > not address this problem in the paper. Notice I do not talk about > non-determinism here. I completely agree with your point of view about > non-deterministic actions. > > Therefore it seems that we mostly developed different parts of the problem. To an important extent your work is indeed complementary to ours. Indeed, we must stress the following: our formalism is not a stand-alone temporal reasoning logic. It does not deal with descriptions of initial states, action preconditions, narratives, state constraints. It does not even make an ontological choice on the nature of time. To use our effect language for temporal reasoning, it must be extended with language constructs for describing these other aspects of temporal knowledge. Or it must be embedded in an existing approach which provides this expressivity. Your work provides such an embedding. We don't. Instead, we focus entirely on ramification and (instantaneous) effect propagation. You will admit that there is merit in our approach: it shows that the ramification problem can be investigated independently of all these other issues - at least if one views causal rules as we do, namely as descriptions of effect propagations independent of say, state constraints-. In other words, our work can be used embedded in a number of other approaches (A, situation calculus, event calculus, temporal logics..). On the other hand, we pay a price for singling out the ramification problem; namely we do not show in our paper the interplay between causal rules and the other types of information. For instance, uncertainty on a certain state of affairs may be due to uncertainty on the initial state or on the narrative (the sequence of events that leads to the state). Obviously, in our paper, we cannot show how to model these sorts of uncertainty; however, our language and semantics is compatible with and is embeddable in many temporal logics in which such uncertainty can be described. Such a logic should satisfy only two conditions: in the logic there must be a notion of momentaneous state of the world which can be represented as a set of true fluents, and uncertainty on the state of the world at a particular moment or situation must be modeled by having different models of the theory in which the state at the time or situation is different (but always two-valued). This is precisely how uncertainty is modeled in your integrated approach. We may add that in the past we have also investigated this combination of inductive definitions and first order logic with uncertainty in a global temporal logic and in logic in general. We have deliberately kept the issue of representing uncertainty on the world (except in our study of nondeterministic effects) out of the current paper to keep the different issues separated. However, uncertainty is addressed in the technical report referred to as [38] in the paper, since there an embedding in a general theory of time is discussed. (The report, like several of the papers mentioned below, can be obtained from http://www.cs.kuleuven.ac.be/~kristof/publications.html As a matter of fact, the idea of integrating inductive definitions with first order logic is the main idea behind Open Logic Programming, used by Marc and Kristof in most of their previous related work (e.g. the papers by Van Belleghem, Denecker and De Schreye in ICLP'94, ICTL'94 and ICLP'97, by Denecker in LPNMR93 and LPNMR95) and is related to ideas about Abductive Logic Programming (in the paper by Console, Theseider Dupre' and Torasso in JLC'91). The idea in Open Logic Programming is that some predicates are considered "defined", and therefore a "closure" semantics, i.e. a Logic Programming (or Inductive Definition)-like semantics is applied to them, while the interpretation of other predicates is left open, possibly being constrained by partial knowledge given in the form of integrity constraints. So, OLP is to be seen as a integration of classical logic with inductive definitions and is suitable for representing uncertainty. Representing and reasoning on uncertainty in this logic is not on the metamathemathical level but on the object level. The embedding of our ramification approach in a linear time structure [38] is actually firmly based on Open Logic Programming. >> In your approach, you impose a syntactical restriction (no cycles) >> which guarantees that the effects are unique and well-defined. > The syntactic requirement of acyclicity is by no means inherent to my > approach. It simplifies the presentation in the LNCS paper. Otherwise I > would have to consider the cases where the correct syntactic form of > successor state axioms is not obtained, thus making the paper even longer. Sorry, that remark was by no means intended as a critique of your approach. We were only trying to explain the use of the third truth value. It helps us to avoid imposing a syntactic restriction, by detecting "bad" definitions in the semantics. Bad definitions need to be dealt with somehow, either by restricting the syntax, which we chose not to do, or by detecting them in the semantics, as we have done. We did not mean to say "your approach does not work with cycles", but only that in any approach some restriction or a way around bad definitions needs to be provided (and that introducing the third truth value is the way we chose to do it). >> We can't see in what way we would be applying the Closed World Assumption. > I use this term in a sloppy way here to say that a state is represented by > a set of positive fluent literal, and the literals not in the set are > false in this state. Classical logic has a 2-valued model semantics. Yet it seems to us that even with a sloppy use of the term "Closed World Assumption", one could not say that classical logic "applies the Closed World Assumption". Neither can this be said about our two-valued state semantics. We do not allow any state to contain undefined fluents just because by "state" we mean a real state, not knowledge of an agent on a state. We do not at all intend that there should be complete knowledge on states. If there is partial knowledge on a state, there will be more than one state matching this partial knowledge. It's again an issue of reasoning about different models, and for each of them our transition function gives a resulting state (it gives one as long as there are no bad definitions, and not more than one as long as there is no explicit nondeterminism). >>> It also seems strange that you cannot derive anything >>> about "holds", although I understand your motivation. >>> Would it be difficult to introduce this feature? >> This is not really true. The result of the transition function defines >> the holds predicate in the next state. One can verify that the next >> state is derived from the previous state and the causal literals as >> described by the normal situation calculus persistence axiom. > Perhaps I should have chosen a different wording. I used "derive" > which I understand as "derive in a formal proof system". > I did not mean "makes true in a particular model". Is your remark that we have not formalised a proof system but only the model theory ? Or are you referring to the fact that our language can be used only to describe state transitions and nothing else? With respect to the second interpretation, we have motivated this choice (see above). With respect to the first interpretation, of course we have not defined any formal proof system in the paper, just a declarative and constructive model semantics. To derive anything about $holds$ in a certain state, given a previous state, one can calculate all the $caus$ literals in the state transition using the fixpoint operator. Calculating the new $holds$ literals from the previous $holds$ and the $caus$ literals is then straightforward: holds(l,s') = [holds(l,s) & not caus(-l)] V caus(l). Is your remark that we have not formalised a proof system but only the model theory ? >> Observe moreover that ramifications need not imply state constraints >> even if they restrict Trans. Of course a restriction of Trans rules >> out certain transitions, but that does not need to mean that any states >> are ruled out: a state is ruled out only if all transitions leading >> to it are invalid. The ``counter'' example in our paper gives an example >> where this is not the case: whenever an output changes to true, the >> counter must be augmented. But a resulting state in which the counter >> were not updated (but all other effects applied) need not be invalid >> in itself. This state might well have existed at an earlier time in >> the history of the network. It can only not be reached from the currently >> given state. So ramifications need not imply any state constraints. > I do not understand neither this comment nor the "Counter" example. > The rules imply a state constraint relating any two consecutive states. > This constraint is perfectly valid. It seems there is just a misunderstanding about terminology here. We use the term "state constraint" to mean a relation between fluents within any one state, not between different states (see also the definition in the paper). As such the term corresponds to for example Reiter's and Shanahan's notions of state constraint and Thielscher's and Lifschitz's notions of domain constraint (to name just a few). We were not aware of a different use of these terms in the literature. It is evident that any derived effect rule necessarily implies some relation between fluents in two consecutive states, e.g. for any state s and any successor state s' of s after any action, the rule "initiating F causes G if H" implies that holds(H,s) & not holds(F,s) & holds(F,s') => holds(G,s') for any F, G and H. But that is not a state constraint. Does this clarify the examples and discussions given before ? > Finally, a question about Definition 1. You say "and body B a nonempty > set of positive and negative literals of D". Do you mean "and body B, a > nonempty set of symbols from D, including $\{t\}$ and $\{f\}$"? No, D already includes $\{t\}$ and $\{f\}$ (see just above definition 1). With positive and negative literals from D we mean symbols of D or their negations. As such the definition allows for $t$ or $f$ to occur alongside other literals in a rule body. Observe that $\neg t$ or $\neg f$ can not occur since $t$ and $f$ can never belong to Defined(D) (see just below definition 1). Thanks for your comments, Kristof, Marc and Daniele ******************************************************************** 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/ ********************************************************************