14.1 Fluent Propositions


14.1 Fluent Propositions

The primitive propositions used to construct assertions in Java are concerned with the values of variables, for example, i==0. They are propositions concerning the state of a program as represented by the values of the program’s variables. However, our models are focused on interaction and as such they describe sequences of actions and do not explicitly describe state. What should be the primitive propositions that we use in the logical description of properties? One possibility would be to make the occurrence of an action a proposition such that for an action a, the synonymous proposition a would be true when the action occurred and false at every other time. The problem here is that, as we saw in Chapter 3, we model concurrent execution as an interleaved sequence of actions which we call a trace. Consequently it would always be the case that only one action proposition could be true at any one instant. This makes it difficult to describe quite simple properties. As a result, we have taken an approach which allows us to map an action trace into a sequence of abstract states described by fluents.

14.1.1 Fluents

fluent FL = <{s1,...sn},{e1..en}> initially B defines a fluent FL that is initially true if the expression B is true and initially false if the expression B is false. FL becomes true when any of the initiating actions {s1,...sn} occur and false when any of the terminating actions {e1..en} occur. If the term initially B is omitted then FL is initially false. The same action may not be used as both an initiating and terminating action.

In other words, a fluent holds at a time instant if and only if it holds initially or some initiating action has occurred, and, in both cases, no terminating action has yet occurred. The following fragment defines a fluent LIGHT which becomes true when the action on occurs and false when the action off or power_cut occurs.

 const False = 0 const True  = 1 fluent LIGHT = <{on}, {off, power_cut}> initially False

We can think of the above fluent as capturing the state of a light such that when the light is on, the fluent LIGHT is true and when the light is off, the fluent LIGHT is false. We can define indexed families of fluents in the same way that we define indexed families of processes:

 fluent LIGHT[i:1..2] = <{on[i]}, {off[i], power_cut}>

This is equivalent to defining two fluents:

 fluent LIGHT_1 = <{on[1]}, {off[1], power_cut}> fluent LIGHT_2 = <{on[2]}, {off[2], power_cut}>

Action Fluents

Fluents are defined by a set of initiating actions and a set of terminating actions. Consequently, given the alphabet α of a system, we can define a fluent for each action a in that alphabet such that the initiating set of actions for the fluent a is {a} and the terminating set of actions is α {τ} – {a}. In other words, the fluent for an action becomes true immediately that action occurs and false immediately the next action occurs. The next action may be the silent action τ. We can also use a set of actions in a fluent expression. The logical value of this is the disjunction (or) of each of the actions in the set. We can freely mix action fluents and explicitly defined fluents in fluent expressions. An example is given in the next section.

14.1.2 Fluent Expressions

We can combine fluents with the normal logical operators. If we wished to characterize the state in which two lights are on, this would be the expression LIGHT[1] && LIGHT[2]. The state in which either light is on would be LIGHT[1] || LIGHT[2]. This latter would also be true if both lights were on. Fluent expressions can be formed using the following logical operators:

&&

conjunction (and)

||

disjunction (or)

!

negation (not)

->

implication ((A->B) (!A||B))

<->

equivalence ((A<->B) (A->B)&&(B->A))

For example, given the fluents:

 fluent POWER = <power_on, power_off> fluent LIGHT = <on, off>

the expression LIGHT->POWER states our expectation that, for the light to be on, the power must also be on. We do not expect that if the power is on the light need necessarily be on as well.

If we wish to express the proposition that all lights are on, we can use the expression:

 forall[i:1..2] LIGHT[i]

This is exactly the same as LIGHT[1] && LIGHT[2]. In a similar way, if we wish to express the proposition that at least one light is on, we can state:

 exists[i:1..2] LIGHT[i]

This is exactly the same as LIGHT[1] | | LIGHT[2].

An expression that combines an action fluent and an explicitly defined fluent is (getkey && LIGHT[1]) which is true when the getkey action occurs when the LIGHT fluent is true – i.e., the light has previously been turned on.




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net