and are the possibility and necessity modal operators.  or example, the modal formula LivingBeing after. LivingBeing corresponds to the abovementioned Mortal concept.

nfortunately, the      logic is shown to be undecidable, at least for most interesting classes of temporal structures One gets decidability only in very restricted cases, such as when the set of temporal models consideral is a finite collection of structures, ach consisting of alpern hoham, a finite set of natural numbers."
propose T-REX, a loose hybrid integration between eida and  itman escription ogics and constraint networks. lans are defined as collections ofsteps together with temporal constraints between their duration. Each step is associated with an action type, represented by a generic concept in K- REP a non-temporal escription ogic. Thus a plan is seen as a plan network, a temporal constraint network whose nodes, corresponding to time intervals, are labeled with action types and are associated with the steps of the plan itself. As an example of plan in T- REX they show the plan of preparing spaghetti marinara (defplan Assemble-Spaghetti-Marinara Boil-Spaghetti Make-Marinara Put-Together-SM
before meets before meets This is a plan composed by three actions, i.e., boiling spaghetti, preparing marinara sauce, and assembling all things at the end. Temporal constraints between the steps establish the temporal order in doing the corresponding actions. A structural plan subsumption algorithm is defined, characterized in terms of graph matching, and based on two separate notions of subsumption  pure terminological subsumption between action types labeling the nodes, and pure temporal subsumption between interval relationships labeling the arcs.

The plan library is used to guide plan recognition eida, in a way similar to that proposed by   autz
. Even if this work has strong motivations, no formal semantics is provided for the language and the reasoning problems.

tarting from the assumption that an action has a duration in time, our proposal considers an interval-based modal temporal logic   in the spirit of   alpern and   hoham and reduces the expressivity of   chmiedel, in the direction of   eida it man, hile chmiedel s work las computational mainery, and alpern and hoham s logic is undecidable, here an expressive decidable logic is obtained, providing sound and complete reasoning algorithms.   i  erently from T-REX which uses two di  erent languages to represent actions and plans a non temporal escription ogic for describing actions and a second language to compose plans by adding temporal information here an extension of a   escription  ogic is chosen in which time operators are available directly as term constructors. This view implies an integration of a temporal domain in the semantic structure where terms themselves are interpreted, giving the formal way both for a well-founded notion of subsumption and for proving soundness and completeness of the corresponding procedure. As an example of the formalism, the plan for preparing spaghetti marinara introduced above is represented as follows