RIF example UC3: Collaborative Policy Development for Dynamic Spectrum Access

Contents

RIF example UC3: Collaborative Policy Development for Dynamic Spectrum Access

Summary

This is an attempt to encode some rules for the Use case Collaborative Policy Development for_Dynamic Spectrum Access using the RIF core language proposed by Harold Boley et al.

The "deductive" or "declarative" rule examples given in the current use case text are only part of the story. As mentioned in the "Motivates" section, the use case will require ECA type rules. The current core language is not meant to accomodate such rules. However, we do give an example of what such a rule might look like for the application mentioned in this use case.

Also, the rules as stated in the use case text are somewhat simplified. The source rules listed below take into account some of the issues that would be likely to arise in the application.

Source rules

In addition to the EU regulations mentioned in the text, the FCC has also adopted a policy on the issue of wireless access to the 5GHz band. In its policy the FCC distinguishes between "masters" and "clients." For our purposes, masters can be thought of as being wifi access points with certain additional functionality, namely, they can detect the presence of certain radar signals and they can notify clients associated with them that they must vacate a channel. Once a master detects radar it must immediately notify clients and all clients (and the master) must stop using the channel within 10 seconds (of the appearance of radar). A client can only use one of these 5GHz channels if it first associates with a master device. Note that the FCC does not expect 100% compliance, rather it is expected that over a certain set of well-defined test scenarios the devices will perform correctly 80% of the time.

In order to be in compliance with the policy a master does not need to be checking for radar continuously. Clearly if the master checks for radar every 9 seconds (or some other reasonable interval) and it informs clients immediately (if radar is detected) and clients can vacate the channel in question within 1 second, then the system will be in compliance. Here are two rules that captures this:

R1:

If
- ChanInUse(?ch,tnow) & LastRadarCk(?ch,?t) & tnow - ?t ≥ 9

Then

RequireAction(rck,?ch,tnow)

R2:

If
- RadarSensed(?ch,?t1) & tnow ≥ ?t1 & tnow - ?t1 ≤ 9 & ChanInUse(?ch,tnow)

Then

RequireAction(vsignal,?ch,tnow)

In these rules an item preceded by a ‘?’ is a (universally quantified) variable. We may assume that there is a syntax (not shown here) for specifying the allowed types of such variables, e.g. ‘?ch’ ranges only over channels and ‘?t’ ranges only over instances of time. The types of entities that qualify as channels and instances of time in the intended senses will be reflected in the presupposed definitions provided by the associated ontology. The predicates, such as ‘ChanInUse’ are similarly so defined. Items in italics, such as ‘tnow’, ‘vsignal’, ‘rck’ and ‘’ are individual constants with the following interpretations: ‘tnow’ designates the current time, ‘rck’ designates the action of sensing for the presence of radar, and ‘vsignal’ designates the action of broadcasting a vacate signal. R1, therefore, says that if a channel is currently in use and had a last radar check at a time that is at least 9 seconds earlier, then the action of performing a radar check on that channel is currently required. R2 says that if radar has been sensed within the last 9 seconds on a channel currently in use, then the action of sending vacate signal for that channel is currently required. Both of these rules are deductive in nature. They capture inferences that explain what the policy is. In order to use thes rules to cause a cognitive radio (here the master device) to do something we need to employ rules (or some other programming construct) that have imperative semantics. Here is an example of an ECA rule that would do that for this case:

ECA-1:

ON
- Concluded(RequireAction,vsignal,?ch)
IF <> DO
- {
  - BroadcastVacateSignal(?ch);
  }

Where BroadcastVacateSignal does not designate a predicate but instead invokes an action.

RIF Translation

This uses the RIF Core WD1 syntax with the declare and formula roles of Forall skipped.

<Forall>
  <Var>channel</Var>
  <Var>time</Var>
  <Var>difftime</Var>
  <Implies>
    <then>
      <Uniterm>
        <Const>RequireAction</Const>
        <Const>RADAR-CHECK_ACTION</Const>
        <Var>channel</Var>
        <Const>T-NOW</Const>
      </Uniterm>
    </then>
    <if>
      <And>
        <Uniterm>
          <Const>ChannelInUse</Const>
          <Var>channel</Var>
          <Const>T-NOW</Const>
        </Uniterm>
        <Uniterm>
          <Const>LastRadarCheck</Const>
          <Var>channel</Var>
          <Var>time</Var>
        </Uniterm>
        <Uniterm>
          <Const>timediff</Const>
          <Var>difftime</Var>
          <Var>time</Var>
          <Const>T-NOW</Const>
        </Uniterm>
        <Uniterm>
          <Const>greaterThanOrEqualTo</Const>
          <Var>difftime</Var>
          <Const>9</Const>
        </Uniterm>
      </And>
    </if>
  </Implies>
</Forall>

<Forall>
  <Var>channel</Var>
  <Var>time</Var>
  <Var>difftime</Var>
  <Implies>
    <then>
      <Uniterm>
        <Const>RequireAction</Const>
        <Const>BROADCAST-VACATE_SIGNAL</Const>
        <Var>channel</Var>
        <Const>T-NOW</Const>
      </Uniterm>
    </then>
    <if>
      <And>
         <Uniterm>
           <Const>RadarSensed</Const>
           <Var>channel</Var>
           <Const>time</Const>
         </Uniterm>
         <Uniterm>
           <Const>ChannelInUse</Const>
           <Var>channel</Var>
           <Const>T-NOW</Const>
         </Uniterm>
         <Uniterm>
           <Const>greaterThanOrEqualTo</Const>
           <Const>T-NOW</Const>
           <Var>time</Var>
         </Uniterm>
         <Uniterm>
           <Const>timediff</Const>
           <Var>difftime</Var>
           <Const>T-NOW</Const>
           <Var>time</Var>
         </Uniterm>
         <Uniterm>
           <Const>lessThanOrEqualTo</Const>
           <Var>difftime</Var>
           <Const>9</Const>
         </Uniterm>
      </And>
    </if>
  </Implies>
</Forall>