The Logic of Dynamic Systems

1 Introduction

A common assumption underlying most formal theories of actions, such as [Gelfand and Lifschitz , 1993; Sande­ wall, 1994], is that state transitions in dynamic sys­ tems only occur when some agent executes an action­ otherwise the state of the system is assumed to be stable. As pointed out for instance in [Pollack, 1992], this view is often too restrictive if one intends to model more re­ alistic scenarios where one or more autonomous agents act in a complex world. In this paper, we present an alternative theory of dynamic systems that is based on a different paradigm: State transitions naturally occur while time passes by. A reasoning agent might influence and direct the development of the system by initiating actions but the system is not assumed to pause in case there are no explicit actions. 1

The aim of this paper is to develop a logic-oriented, formal theory of dynamically changing worlds and the process of acting in them. We will show that our view provides naturally two main characteristic features. First, the notion of parallelism is an intrinsic element of our theory. This notion includes the concurrent ex­ ecution of actions as well as the simultaneous occur­ rence of events. Second, we can easily model delayed effects of actions by initiating additional independent events which eventually trigger a particular effect . This is the case since parallelism normally means that the var­ ious changes during a state transition are simultaneously caused by several reasons.

1 A similar principle was recently introduced in [Grofie, 1994] in the context of a modal logic approach to reasoning about actions .

When specifying a dynamic system, a major challenge is to find a compact description of the underlying causal model, which defines the space of possible state changes in the course of time. Our theory includes these two fundamental concepts: First, the persistence assump­ tion2, which enables one to state explicitly only what changes during a single state transition while everything else is implicitly assumed to remain unchanged. Sec­ ond, atomic causal laws are used to state relationships between single cause-effect-pairs. Since usually several of these atomic laws apply to the current state of a dy­ namic system, a combination of such laws determines the complete transition step. The use of atomic causal rela­ tionships is especially necessary in theories which involve concurrency of actions and events.

The major application of formal specifications of dy­ namic systems is to address one of the following three problem categories:

• In a temporal projection problem, one is interested in the result of executing a particular sequence of actions starting in a particular state of the system.
• In a planning problem, the question is whether a sequence of actions, taken as a plan, can be found whose execution in the system results in the sat­ isfaction of a given goal. Below, we will illustrate that our theory enables us to formulate more general planning problems compared to the classical AI de­ finition of planning. We are able to specify that the properties we strive for might be distributed over several states of the system and need not necessar­ ily be satisfied in a single final state, until otherwise required.
• In a postdiction problem 3 , one is faced with a nar­ rative which is represented by a number of obser­ vations regarding a system's development during a specific period. These observations are used to de­ rive more information about what has happened. Our theory generalizes former work such as [Gelfand

2 also called frame a88umption or inertia principle

3 called chronicle completion in [Sandewall, 1994]

and Lifschitz, 1993; Sandewall, 1994] in so far as the sequence of actions performed during the period in question is not necessarily completely known.

In the course ofthis paper, we will give precise definitions of all these three problem categories in terms of our the­ ory. We will illustrate that this results in a model-based semantics for formal specifications of dynamic systems along with particular problem instances, which enables us to define solutions to such problems in terms oflogical entailment.

The paper is organized as follows. In Section 2, we define deterministic dynamic systems, where a unique successor state can always be determined provided the current state is completely known. For sake of simplic­ ity, we focus on so-called propositional dynamic systems, where states are described by means of a finite number of propositional constants. We introduce the notion of a logical formula to describe properties of system states. Such a formula can be used, for instance, to specify which combinations of truth values for the underlying proposi­ tional constants denote impossible (inconsistent) states. In Section 3, we define the notions of persistence as­ sumption and atomic causal laws; they both are funda­ mental for a compact and intuitive specification of the behavior of a dynamic system. We introduce a certain specificity criterion in order to resolve conflicts which occur whenever the concurrent execution of actions or the simultaneous occurrence of events, respectively, has different effects than the serial execution. In Section 4, we develop a model-based semantics for specifications of dynamic systems and define the process of influenc­ ing the development of a system by means of executing actions. This allows for a precise formalization of the three aforementioned problem categories. In Section 5, we extend the basic version of our theory to nondeter­ ministic dynamic systems, where uncertainty about the successor state may exist even if the system's current state is completely known. In particular, we argue that the concept of nondeterminism provides an interesting and reasonable solution to the problem of concurrently executed actions whose causal laws propose mutually ex­ clusive effects: Instead of declaring such situations im­ possible, which is the standard proposal in literature (e.g., [Lin and Shoham, 1992; Baral and Gelfond, 1993; GroBe, 1994]), we take only the disputed effects as un­ certain (c.f. [Bornscheuer and Thielscher, 1994]).

The reader should be aware of the purpose of this pa­ per, which is unusual in so far as it merely consists of de­ finitions rather than describing concrete results. We pro­ pose a formal framework to specify and to reason about dynamic systems. Thus, our intention is similar to the purpose of the topical systematic approaches [Sandewall, 1994; Gelfond and Lifschitz, 1993], namely, to provide a high-level framework which deserves adequate proof the­ ories or can be used to assess the range of applicability of existing approaches. A brief discussion of this aspect in Section 6 concludes the paper.

2 Specifying Dynamic Systems

A formal specification of a dynamic system consists of two components. First , a collection of fluents [McCarthy and Hayes, 1969], which are used to describe particu­ lar states of the system. For sake of simplicity, we re­ strict attention to a finite set of propositional constants here. Second, the behavior of the system as regards state transitions needs to be described. In this and the next two sections, we focus on deterministic dynamic systems. This is reflected in the following definition, where a tran­ sition function determines unique successor states.

Definition 1 A deterministic, propositional dynamic system is a pair (:F, <I>) consisting of a finite set of sym­ bols :F , called fluents, and a partially defined mapping <I> : C f-+ C , called causal model. The range of the latter is a particular set of subsets of :F, i.e., C ~ 2.:F. ·

Each subset s of :F determines a (not necessarily pos­ sible) state of the dynamic system at hand. Each fluent f E s is then said to be true in s while each fluent f E :F \ s is taken to be false . The set C is intended to contain all so-called consistent states-only for these states s the successor state <I>( s) is defined through the exhaustively given causal model.

Based on the notion of truth wrt single fluents and states, we can construct (propositional) formulae and define entailment following the standard way:

Definition 2 Let :F be a set of fluents. The set of fluent formulae (based on :F ) is the smallest set such that each element f E :F is a fluent formula; and if F and G both are fluent formulae then -.F, (F 1\ G), (F V G), and (F--+ G) are also fluent formulae .

Given a state s ~ :F and a fluent formula F , the no­ tion of F being true in s , written s I= F , is inductively defined as follows:

• s I= f iff f E s , for each f E :F .
• s I= -.F iff s ~ F .
• s I= (F 1\ G) iff both s I= F and s I= G .
• s I= (FvG) iff s I= For s I= G (or both).
• s I= (F--+G) iff s ~ F or s I= G (or both).

·

Fluent formulae can be used, for instance, to specify con­ sistency of states more compactly by means of a partic­ ular formula C such that a state s E :F is defined to be consistent iff s I= C . Then, the set C , which contains all consistent states of a dynamic system (see Defini­ tion 1), is implicitly given by C = { s ~ :F I s I= C} .

In order to integrate the paradigm mentioned in the introduction, we call some distinguished fluents :Fa C :F actions; these are fluents which an agent can make true in the current state in order to influence the system's behavior. Hence, actions are nothing else than elements of a state description . The formal notion of executing actions will be given below, in Section 4.

Example 1 The Yale Shooting domain will be used, in several variants, as the running example throughout the paper. To formalize a first version, consider the set of fluents :F = {alive , loaded, load, shoot} -where alive and loaded are used to describe the state of the turkey and the gun, respectively, while load and shoot are action fluents to describe the events of loading the gun and shooting with it , respectively. The particular state s = {alive, load} ~ :F, for instance, describes the facts that the turkey is alive, that the gun is un­ loaded, and that the agent intends to execute the ac­ tion load. The successor state P( s) might then be de­ fined as {alive, loaded} , stating that the turkey is still alive and that the gun is now loaded. Furthermore, one might wish to specify that the agent cannot simultane­ ously load the gun and shoot. This can be achieved by means of the consistency criterion C = ·( load 1\ shoot) such that, say, s I= C due to {alive, load} ft= shoot . ·

3 Causal Laws

The main challenge when specifying a dynamic system is the problem of finding a compact representation of the corresponding causal model P . The most fundamental concept related to this is the principle of persistence, which enables us to only specify the fluents that change their value during a particular state transition; all other fluents are implicitly taken to keep their value.

In our theory, we make a distinction between so-called static fluents :F, that "tend to persist," i.e., which are assumed to keep their value until the contrary is ex­ plicitly stated (and, hence, to which the persistence as­ sumption should apply), and so-called momentary flu­ ents :Fm that "tend to disappear" [Lifschitz and Ra­ binov, 1989]. For instance, shooting with a previously loaded gun causes a bang which, however, does not per­ sist and abates immediately. As an important subclass of momentary fluents we have the action fluents :Fa . Alto­ gether, the set offluents :F describing a dynamic system consists essentially of three components (:F., :Fm, :Fa) where :Fa ~ :Fm and :F, n :Fm = 0.

Based on this sophistication, the persistence principle is integrated into our framework by defining that, for each state s, the successor state P( s) is specified via an associated triple of sets of fluents (sf-, sf+, mf+). Here, sf- contains the static fluents which change their truth value to false during the state transition, i.e., which are removed from s ; sf+ contains the static fluents which change their truth value to true, i.e., which are added to s ; and mf+ contains all momentary fluents which are true in P( s) . All other static fluents in s continue to be (and no other static fluents become) ele­ ment of P( s) while all momentary fluents except those in mf+ shall not be contained in the resulting state.

Example 2 Consider an extension of the Yale Shoot­ ing domain with static fluents :F, = {alive, loaded} and momentary fluents :Fm = {bang, bullet, load, shoot}, where the additional fluents bang and bullet describe, respectively, the temporary acoustical occurrence of a shot and a flying bullet. We then might specify the fol­ lowing:

In words, shooting with a previously loaded gun causes the gun to become unloaded ( loaded E sf(-;.) ) and the occurrence of two events, bang and bullet ; and the fly­ ing bullet is intended to hit the turkey and, hence, causes it to drop dead ( alive E sf(-;,) ) during the following state transition. This example illustrates how our paradigm allows for a natural formalization of delayed effects (here, the victim's death as a final result of having shot with the gun) . Using this specification, we obtain, for instance, P(P({alive, loaded, shoot}))= P({alive, bang, bullet})= 0 . Note that finally both fluents bang and bullet dis­ appear automatically because they are momentary. ·

Although the persistence assumption allows for a com­ paction of defining a successor state P( s) by providing instructions to computing it, the formalization above still requires an exhaustive description as regards the space of states s . Therefore, the second major principle of specifying the behavior of a dynamic system consists in splitting the definition of a single state transition into separate atomic laws of causality, which then are usually applicable in multiple states. This is especially essential in theories which involve concurrency since it enables one to specify the effects of each single action (or event like bullet) separately:

Definition 3 Let :F = :F,U:Fm be a set of static and momentary fluents. A structure c: (sf-, sf+, mf+) is called a causal law if c ~ :F, called the condition; sf-, sf+ ~ :F, ; and mf+ ~ :Fm. ·

A causal law is applicable in a state whenever its con­ dition is contained in the state description. 4 In what follows, to select the four components of some causal law £ = c: (sf-, sf+, mf+), we use the four functions cond ( £) ~! c , static- ( £) ~ 1 sf- , static+ ( £) ~! sf+ and moment+(£) ~ 1 mf+. For convenience, we furthermore use the following abbreviation to describe the result of applying a set of causal laws £ to some state s :

where :Fm denotes the set of momentary fluents con­ sidered in the dynamic system at hand. Hence, we first remove from s all static fluents that are supposed to become false by some causal law in £ ; afterwards, all momentary fluents are removed; and finally, all static and all momentary fluents are added that are supposed to become true by some law in £ .

Example 3 Consider the two causal laws

whose conditions both are contained, hence satisfied, in the state s = {alive, loaded, bullet, shoot} (where bullet might result from a previous shot). We obtain Trans( { £11 £2}, s) = {bang, bullet} . ·

4 1t is for the sake of simplicity why we have restricted the condition of a causal law to a set of fluents and defined ap­ plicability as validity of the conjunction of these fluents in the state at hand. It is however natural and straightforward to consider arbitrary fluent formulae (c.£. Definition 2) instead.

It is of course important to take into account the pos­ sibility that the simultaneous occurrence of two or more actions (or events) might have different effects than their separate occurrence. As an example, consider a table with a glass of water on it. Lifting the table on any side causes the water to be spilled whereas nothing similar happens if it is lifted simultaneously on opposite sides. In terms of our theory, we can specify this situation by three causal laws, viz

where lift-left and lift-right both are action fluents and water-spills too is a momentary fluent. Unfor­ tunately, however, each law is applicable in the state s = {lift-left, lift-right} , thus determining the unin­ tended result Trans( { £1, £2, £3}, s) = {water-spills}.

In order to avoid this kind of counterintuitive behav­ ior, we employ an additional criterion to suppress the ap­ plication of some causal law as soon as, roughly spoken, more specific information is available (see also [Baral and Gelfond, 1993; Holldobler and Thielscher, 1995]). For in­ stance, Law £3 in (2) should override £1 and £2 when­ ever it is applicable. Formally, we introduce the following partial ordering on causal laws:

Definition 4 Let £1, £2 be two causal laws then £1 is called more specific than £2 , written i\ -< £2 , iff cond(£1) :J cond(£2). ·

E.g., £3 -< £1 and £3 -< £2 but neither £1 -< £2 nor £2 -< £1 in (2). 5

Based on the specificity criterion, the causal model of a dynamic system is obtained from a set of causal laws as follows :

Definition 5 Let :F be a set offluents and .C a set of causal laws. For each (consistent) state s ~ :F let .C( s) denote the set

In words, .C( s) contains each causal law £ E .C which is applicable in s (i.e., cond(£) ~ s) unless there is a more specific law £' E .C that is also applicable (i.e., £' -< £ and cond(£') ~ s ).

For instance, since the first two causal laws in (2) are less specific than the third one, we now obtain-due to .C( {lift-left, lift-right}) = { £3 } -the successor state ~( {lift-left, lift-right}) = 0 as intended. On the other hand, we still obtain, say, ~( {lift-left}) = {water-spills} because Law £3 , though more specific than £1 , is not applicable in this case.

5 1f we allow arbitrary fluent formulae as conditions of causal laws (c.f. Footnote 4), then a law with condition c1 is said to be more specific than a law with condition c2 iff V s. s f= Ct --+ c2 imd 3s. s f= ...,( c2 --+ c1) . In the propositional case, this is obviously still decidable and a corresponding de­ pendence graph could be computed in a pre-processing step.

One should be aware of the fact that nonetheless it might well happen that two most specific applicable laws have mutually exclusive effects. A reasonable way to handle this problem will be proposed and formalized be­ low, in Section 5. For the moment we assume that the combination of most specific causal laws never leads to contradictory fluent values, i.e., more formally, that

for each (consistent) state s (where .C( s) is as in Defi­ nition 5).

4 A Model-Based Semantics

Based on the specification of state transition in a dy­ namic system, we can define its behavior over a longer period and under the influence of one or more agents. To direct the development of a system, these agents are able to (simultaneously) execute actions. The execution of one or more actions in a particular state is modeled by adding the corresponding set of action fluents to the state descriptions before applying the transition func­ tion. Since we take action fluents as momentary, these are usually removed during a state transition. The fol­ lowing definition formalizes this concept and extends it to the application of sequences of action sets:

Definition 6 Let ( :F, ~) be a dynamic system with action fluents :Fa C :F and p = [a1, ... , an] ( n 2:: 0) be a sequence of sets of action fluents (i.e., ai ~ :Fa). Furthermore, let s0 be a consistent state, then the ap­ plication of p to s0 yields an infinite sequence of system states (s1, ... ,sn,sn+1 1 ··· ) where

• s1 = so U a1;
• Si+l = ~(si) U ai+1 , for each 1 ~ i < n; and
• Si+1 = ~(si) for each i 2:: n

provided each state s1 , ... , sn is consistent-otherwise the application of p to s0 is undefined. If it is de­ fined then the triple (p, s0 , (s1 , ... ) ) is a development in (:F, ~). ·

Note that some sets of actions ai might be empty, i.e., an agent has the possibility to pause for a moment and let the system act autonomously. Note further that, af­ ter having executed the entire sequence of actions, the resulting state is not necessarily stable, i.e., the system might run into a limit cycle by oscillating among a num­ ber of states. Although a transition function ~ should be designed such that no inconsistent state results from a consistent one ( c.f. Definition 1), the process of adding action fluents may cause inconsistency of some state Si . This is the reason for the additional consistency require­ ment above.

Example 4 Consider the Yale Shooting domain in the formalization of Example 2 along with the causal model determined by the two causal laws in (1). The appli­ cation of the sequence [0, {shoot}] to the initial state s0 = {bang , alive, loaded} yields

In the course of the development of a system, we can make observations concerning its various states. An ob­ servation can be formulated as a fluent formula associ­ ated with a particular time point. We then call a formal development in the sense of Definition 6 a model of an observation iff the corresponding fluent formula is true in the corresponding state of the development:

·

Definition 7 Let (F, <P) be a dynamic system. An expression [i]'¢' is called an observation if i E IN0 and '¢' is a fluent formula. Such an observation holds in a devel­ opment (p, s0 , (s1 , ... ) ) iff Si f= '¢'. A model of a set \]! of observations is a development in (F, <P) where each element of \]! holds. ·

For instance, [O]alive 1\ -.bullet and [3]-.alive are two observations that can be formulated in our Yale Shoot­ ing domain. Then, this development is a model wrt the causal laws in (1):

since we have s0 = {alive, loaded} f= alive 1\ -.bullet and s3 = 0 f= -.alive. The reader is invited to verify that not only in this development but in every model of the two observations above the additional observation [1] shoot 1\ loaded holds-hence, we are allowed to con­ clude that a shoot action must have taken place and that the gun was necessarily loaded at the beginning. 6

In general, we define the following notion of entailment on the space of observations:

Definition 8 Let ( F, <P) be a dynamic system and \]! a set of observations. \]! entails an additional obser­ vation [i]'¢', written \]! F<t [i]'¢', iff [i]'¢' holds in each model of \]! . ·

Based on this model-theoretic formalization of dy­ namic systems, we can classify some important and well­ known problem categories as instances given a system (F, <P), depending on what information is provided:

6 0ne referee raised the question whether one should in general assume minimality of actions being performed when trying to find models for a given set of observations. Al­ though this assumption might be helpful (if taken as prefer­ ence ordering) e.g. in case of planning problems, we definitely do not want to employ this criterion as a global restriction on the notion of a model. If, for instance, we observe the gun being unloaded at the beginning and being loaded after a while, we can conclude safely only that at least one load action has eventually taken place; we ought not to disregard the possibility that the gun has been loaded and shot with several times before, because there is nothing illogical about this. Besides, our definition guarantees the property of re­ stricted monotonicity [Lifschitz, 1993), which means that ad­ ditional observations can never force the revision of previous conclusions.

• A temporal projection problem consists of an ini­ tial state s0 along with a sequence of sets of ac­ tions p = [ a1, ... , an] . The question is to compute the resulting state after having applied p to s0 ·

In terms of our theory, the problem is essentially to find a model for the particular set of observa­ tions that describes the given initial state and ex­ actly those occurrences of action fluents which are determined by p, i.e.,

where Fa denotes the underlying action fluents.

• A classical planning problem consists of an initial state so and a fluent formula g , called the goal. The question is to find a sequence of sets of ac­ tions p whose application to s0 yields a sequence of system states containing one particular state Sn which satisfies g .

In terms of our theory, the problem is essentially to find a model for this set of observations:

for some n E IN .

• A postdiction problem consists of a narrative given by a set of observations \]! along with a sequence of sets of actions p = [a1, ... , an]· The question is to decide whether an additional observation is a logical consequence of this scenario.

In terms of our theory, the problem is essentially to decide entailment wrt the particular set of obser­ vations that includes the given ones and describes exactly those occurrences of action fluents which are determined by p, 1.e.,

Due to the fact that our theory generalizes several formal approaches to reasoning about actions, we are able to formulate, for instance, more general planning problems where the initial situation is only partially defined and where the goal specification is not necessarily required to hold in a single state. Or, we can formulate general postdiction problems where the sequence of actions is only incompletely specified, etc.

5 Non determinism

In this section, we extend the concepts developed so far to so-called nondeterministic dynamic systems. Non­ determinism occurs when uncertainty about the succes­ sor state exists even in case the current state is com­ pletely known. This is reflected in the following defin­ ition, where the causal model consists of a relation on pairs of states (see, e.g., [Thielscher, 1994]) instead of a function as in Definition 1:

Definition 9 A nondeterministic, propositional dy­ namic system is a pair ( :F, <I>) consisting of a set of fluents :F and a relation <I> C 2:F x 2:F . ·

Given a state s ~ :F, each s 1 such that ( s, s 1 ) E <I> is called a possible successor state. A state is now said to be inconsistent in case it has no successor at all.

The concept of nondeterminism is reflected in an ex­ tended notion of a causal law where several expressions ( sf i, sft, mft) can be associated with a single condi­ tion; each triple then determines a possible alternative:

Definition 10 Let :F = :F,U:Fm be a set of static and momentary fluents. An extended causal law is a struc­ t ure c : { (sf1, sfi, mfi), ... , (sf;;, sf~, mf~)} where n 2': 1 ; c ~ :F; sfi, sft ~ :F,; and mft ~ :Fm ( 1 :S i :S n ). ·

Example 5 The Russian Turkey scenario (see, e.g., [Sandewall, 1994]} is obtained from the Yale Shooting domain by adding an action fluent spin . The effect of spinning its cylinder is that the firearm becomes ran­ domly loaded or not, regardless of its state before. This nondeterministic effect can be modeled by the following extended causal law:

·

As for the special case of deterministic systems, the combination of all most specific laws shall determine the behavior of the system at hand. Hence, for each state s we define the set .C ( s) as

similar to Definition 5, where .C denotes the underlying set of (extended) causal laws. Now, let .C(s) be the set {cl : A1, ... ,ck : Ak} (k 2': 0) and define Poss(.C(s)) as

containing each possible selection and combination of al­ ternatives. Each element in Poss(.C(s)) determines a possible successor state of s, i.e.,

For instance, consider ( 4) as the only applicable causal law in the state s ={alive, spin}. Then, Poss(.C(s)) is

The concept of nondeterminism provides us with an interesting solution to the problem of concurrently exe­ cuted actions with mutually exclusive effects. Consider, for instance, the two causal laws

where push-door and pull-door denote action fluents while the static fluent open describes the state of the door under consideration here. Now, assume three agents acting concurrently: The first one tries to push the door, the second one tries to pull it, and the third agent intends to lift the left hand side of a table inside the room ( c.f. ( 2)) . Assume further that the door is closed at the moment and no water spills out of the glass sit­ uated on the table, then this situation can be expressed by the state s = {push-door, pull-door, lift-left} . Now, aside from 1\ in (2) both causal laws in (5) are applica­ ble. However, the first one requires the door to be open in the succeeding state ( open E sf+ ) while the second one requires the contrary ( open E sf- ). Hence, our consistency condition, (3), is not satisfied here.

Most classical AI formalizations of concurrent actions, such as [Lin and Shoham, 1992; Baral and Gelfond, 1993; GroBe, 1994], declare situations like s inconsistent and, hence, do not allow any conclusions whatsoever about the successor state. Indeed it is impossible that both ac­ tions push-door and pull-door are successful. However, in [Bornscheuer and Thielscher, 1994] we argue (in the context of a theory developed in [Gelfond and Lifschitz, 1993; Baral and Gelfond, 1993]) that it is reasonable to draw some conclusions at least about uninvolved fluents; e.g., we would like to conclude that the third agent is suc­ cessful in lifting the table, which causes the water to be spilled out. Preventing global inconsistency in case of local conflicts is the basic intention in this idea.

The notion of nondeterminism provides us with the possibility to draw conclusions like the one just men­ tioned. Instead of declaring the successor state of s as completely undefined, we take only the disputed flu­ ent(s) (here: open) as uncertain while any other ef­ fect (here: water-spills, coming from (2)) occurs as in­ tended. In our example, we then obtain two possible successor states of s , namely, {open, water-spills} and {water-spills} -providing us with the conclusion that water-spills is an obligatory effect of s .

This strategy of conflict solving is integrated in the following definition of how to obtain the causal model in case of nondeterministic systems:

Definition 11 Let :F be a set of fluents and .C a set of (extended) causal laws. For each (consistent) state s ~ :F let .C( s) denote the set

Now, if .C(s) = {c1 : A1, ... , ck : Ak} ( k 2': 0) then let Poss(.C(s)) be the set

and define ( s, s 1 ) E <I> iff

where

·

The set Confl(P) is intended to contain all disputed fluents ( c.f. ( 3)), and each possible combination of these fluents determines a possible successor state. 7

Finally, the semantics developed in the previous sec­ tion is extended to nondeterministic dynamic systems in the following way (c.f. Definition 6):

Definition 12 Let (F, ~) be a nondeterministic dy­ namic system with action fluents Fa C F, and let p = [a1 , ... , an] ( n ~ 0) be a sequence of sets of action fluents (i.e., ai ~ Fa). Furthermore, let so be a consis­ tent state, then a triple (p, so, (s1, ... , sn, Sn+l> ... ) ) is a development iff

• Si +l = s~ U a i +l , where (si , s:) E ~ , for each 1::::; i < n ;
• (si , si+I) E ~ for each i ~ n

and each state s1 , . . . , sn is consistent .

·

6 Summary and Outlook

We have presented a formal theory of dynamic systems that is based on a different paradigm compared to stan­ dard approaches such as [Gelfond and Lifschitz, 1993; Sandewall, 1994] : State transitions naturally occur while time passes by-the system does not necessarily keep stable until agents perform actions. We have illustrated that our framework allows for a natural treatment of concurrent actions and simultaneous events as well as delayed effects. Based on the underlying specification of a dynamic system, we have developed a semantics for observations, i.e., fluent formulae associated with time points. We have investigated both deterministic and nondeterministic systems, and we have integrated a rea­ sonable way to handle the problem of concurrent actions with mutually exclusive effects.

The purpose of this paper was to propose a general and uniform specification language for dynamic systems in conjunction with an intuitive semantics. We have not yet tackled the question of an adequate proof theory. The problem of finding such a calculus and proving its sound­ ness and completeness constitutes the paramount aspect of future work. Our proposal is meant as a challenge: How can existing approaches be adopted to the kind of dynamic systems being specified on the basis of our the­ ory? For instance, how could a variant of the situa­ tion calculus [McCarthy and Hayes, 1969] be designed­ called, say, state calculus-where the common successor state argument Result( a, s) is replaced by Result ( s) , i.e., which no longer depends on the execution of some action? Other promising directions are the adaption of resource-oriented approaches to reasoning about actions and change [GroBe et al., 1992], dynamic logic [Harel, 1984], or a first-order encoding following [Elkan, 1992]. Last but not least, though in its current state it covers neither the static-momentary distinction nor specificity or nondeterminism, the modal logic approach [GroBe, 1994] should be a candidate worth being considered since it already includes the principle of taking actions as part of state descriptions. Conversely, our semantics provides a tool for a formal assessment of its range of applicabil­ ity, similar to investigations carried out in [Sandewall, 1994].

7 Note that we are supposed to remove the set sf ~ from Trans(P, s) due to the fact that all elements in Confl(P) are first of all added when computing Trans(P, s) .

Acknowledgments

The author thanks Christoph Herrmann for helpful com­ ments on an earlier version of this paper.