=Paper=
{{Paper
|id=None
|storemode=property
|title=An Application of Formal Methods to Cognitive Radios
|pdfUrl=https://ceur-ws.org/Vol-832/paper_11.pdf
|volume=Vol-832
|dblpUrl=https://dblp.org/rec/conf/fmcad/ArkoudasCC11
}}
==An Application of Formal Methods to Cognitive Radios==
https://ceur-ws.org/Vol-832/paper_11.pdf
∗
An Application of Formal Methods to Cognitive Radios
Konstantine Arkoudas and Ritu Chadha and Jason Chiang
Telcordia Research
One Telcordia Drive
Piscataway, NJ 08854
{konstantine, chadha, chiang}@research.telcordia.com
ABSTRACT As wireless devices continue to proliferate, demand for
We discuss the design and implementation of a formal policy access to RF spectrum is becoming increasingly pressing,
system regulating dynamic spectrum access (DSA) for cog- and increasingly difficult to achieve. After all, the (usable)
nitive radios. DSA policies are represented and manipulated spectrum is finite, while the demand for it continues to in-
in a proof framework based on first-order logic with arith- crease without bounds. However, it has been recognized [13,
metic and algebraic data types. Various algebraic operations 14] that problems of spectrum scarcity and overuse arise not
combining such policies can be easily implemented in such so much from physical shortage of frequencies, but mostly
a framework. Reasoning about transmission requests is for- as a result of the centralized and rigid way in which spectrum
mulated as a satisfiability-modulo-theories (SMT) problem. allocation has been managed. Spectrum has been allocated
Efficient SMT solvers are used to answer the corresponding in a static way: bands of the RF range are statically assigned
queries and also to analyze the policies themselves. Further, to licenced users on a long-term basis, who then have ex-
we show how to reason about transmission requests in an op- clusive rights to the corresponding region. Examples here
timal way by modeling the problem as an SMT instance of include the 824–849 MHz, 1.85–1.91 GHz, and 1.930–1.99
weighted Max-SAT, and we demonstrate that this problem GHz frequency bands, which are reserved for FCC-licenced
too can be efficiently solved by cutting-edge SMT solvers. cellular and personal communications services (PCS). Other
We also show that additional optimal operations on trans- parts of the RF spectrum, by contrast, are unlicensed, and
mission requests can be cast as classic optimization prob- anyone can transmit in those frequencies as long as their
lems, and to that end we give an algorithm for minimizing power does not exceed the regulatory maximum. Conse-
integer-valued objective functions with a small number of quently, large portions of the RF range remain underutilized
calls to an oracle SMT solver. We present experimental re- for long periods of time, while other parts—such as the ISM
sults on the performance of our system, and compare it to bands—are overutilized.
previous work in the field. Observations like these provided the impetus behind the
NeXt Generation (XG) Communications program, a tech-
nology development program sponsored by DARPA [9], which
1. INTRODUCTION proposed opportunistic spectrum access as a means of cop-
One of the world’s most prized physical resources is the ing with spectrum scarcity. The underlying approach has
electromagnetic spectrum, and particularly its radio frequency come to be known as dynamic spectrum access (DSA), and
(RF) portion, stretching roughly from 10 KHz to 300 GHz. has evolved into a general methodology for dealing with
The RF spectrum is so valuable that its allocation is strictly spectrum scarcity [17]. The main idea is that a DSA net-
regulated by world governments, and these days even small work has two classes of users: primary and secondary. Pri-
parts of it can be sold for billions of dollars in spectrum auc- mary users are licenced to use a particular spectrum band
tions. and always have full access to that band whenever they need
∗The research reported in this paper was performed in connection
it. Secondary users are allowed to use such spectrum por-
tions but only as long as their use does not interfere with the
with contract number W15P7T-08-C-P213 with the U. S. Army
operating needs of the primary users. The secondary users
Communications Electronics Research and Development Engineer-
ing Center (CERDEC). The views and conclusions contained in this are typically cognitive radios [4] that can dynamically adjust
document are those of the authors and should not be interpreted as their operating characteristics (such as waveform, power, etc.).
presenting the official policies or position, either expressed or im- Secondary users sense the spectrum for available transmis-
plied, of the U. S. Army CERDEC, or the U. S. Government unless sion opportunities, determine the presence of primary users,
so designated by other authorized documents. Citation of manufac-
turers or trade names does not constitute an official endorsement
and attempt to use the spectrum in a way that interferes as
or approval of the use thereof. The U. S. Government is autho- little as possible with the activities of the primary users.
rized to reproduce and distribute reprints for Government purposes Policies are used for specifying how secondary radio nodes
notwithstanding any copyright notation herein.
are allowed to behave. Policies consist of declarative state- gramming language [3]. Athena’s rich logic, sort system,
ments that dictate what secondary radios may or may not and programming language significantly facilitated the rep-
do, without prescribing how they might do it [18]. Different resentation and manipulation of policies. Another innova-
policies may be applicable in different regions of the world. tion of our paper is the use of SMT solvers [15] for rea-
Even in one and the same region there may be multiple poli- soning with and about policies. The problem of determin-
cies in place, reflecting different constraints imposed by dif- ing whether a transmission request is permissible by a given
ferent regulatory bodies. Policy systems for cognitive radios policy can be couched as a satisfiability problem, namely,
should be able to load new policies on the fly. the problem of determining whether the request is consistent
There are two key questions in designing such a policy with the policy. So SAT solving would seem to be a natu-
system, one representational and the other computational: ral fit for this domain. However, policy rules in this domain
How should we represent policies, and how can we make ef- also make heavy use of equality and numeric relations, not to
ficient use of them? Policies regulating DSA must be able to mention symbolic values such as transmission modes. Thus,
express rules such as the following: “Allow a transmission if viewed as an abstract syntax tree, the body of a policy rule
its frequency is in a certain range and the power does not ex- has an arbitrarily complicated boolean structure internally,
ceed a certain limit, or if the transmission is an emergency.” with relational atoms at the leaves, whose semantics come
Thus, for representation purposes, we need at least the full from standard theories such as those of arithmetic, equal-
power of propositional logic, as well as numbers (both inte- ity, and so on. That is what makes SMT solving an ideal
gers and reals), and numeric comparison relations. It would paradigm for this problem. We will show that the problem
also be helpful to have algebraic datatypes at our disposal, of making optimal adjustments to transmission parameters
so that we could, for example, represent the mode of a trans- can also be formulated quite naturally in this setting as a
mission as one of a finite number of distinct symbolic val- weighted Max-SAT problem, many instances of which can
ues, such as everyDay or emergency. A certain amount of be efficiently solved despite the problem’s high theoretical
quantification would also be convenient, so that we could, complexity. Indeed, competitive SMT solvers such as CVC3
e.g., quantify over all possible transmissions. We must also [7] and Yices [6] are highly optimized programs that can
be able to introduce arbitrary transmission parameters, so a readily decide extremely large formulas. As a quick com-
strong type system, preferrably with subtyping, should be parison, another recently built policy system for spectrum
available. Hence, first-order logic with arithmetic, and per- access, Bresap, which uses BDDs as its underlying technol-
haps additional features such as algebraic datatypes and sub- ogy, cannot handle policies with more than 20 atomic ex-
sorting, would appear to be a natural representation choice, pressions [1, p. 83]. By contrast, our system can easily han-
provided that we can make efficient use of it, a point that we dle policies with many thousands of atomic expressions.
will address shortly. The remainder of this paper is structured as follows. The
So much for representation. What are the main computa- next section describes the representation of spectrum-access
tional problems that a policy system must solve? The main policies in Athena.1 Section 3 discusses the integration of
problem is this: determine whether an arbitrary transmission SMT solvers with Athena, and shows how to reduce the
request should be allowed or denied, given the current set of problem of reasoning with spectrum-access policies to SMT
policies. In fact, if this were all there was to using policies solving. In section 4 we model the problem of making opti-
for spectrum access, things would be relatively simple. But mal changes to transmission requests as a Max-SAT prob-
we usually want the policy engine to do more. For example, lem, and we describe how our system models and solves
when a transmission request is not permissible, a simple “de- such problems. We also present an optimizing algorithm
nied” answer is not very useful. The policy system should that uses a version of binary search in order to minimize
also tell the requesting radio why the request was denied, integer-valued objective functions with very few calls to an
and more importantly, what it would take for its request to oracle SMT solver (at most log(n) such calls, where n is
be allowed. As a simple example, the system might tell the the maximum value that can be attained by the objective
radio: “Your request cannot be allowed in its present form, function). This algorithm can be used to further optimize
but it will be allowed if you only change your transmission transmissions, e.g., by minimizing the distance between the
power to such-and-such level.” Further, in such cases the values desired by the cognitive radio and the values allowed
policy system will usually have many choices as to which by the policy. Section 5 presents results evaluating the per-
parts of the transmission request to modify in order to make formance of our policy engine. Finally, section 6 discusses
it permissible. We then want it to make an optimal choice, related work and concludes.
i.e., a choice that satisfies the original request to the greatest
possible extent. 2. POLICY REPRESENTATION
In this paper we present an implementation of a policy
system in Athena, an interactive proof system for polymor- 1
While some Athena code is presented, knowledge of the language
phic multi-sorted first-order logic with equality, algebraic is not necessary. Any reader familiar with formal methods and
data types, subsorting, and a higher-order functional pro- functional programming languages should be able to follow the
code.
The set of radio transmissions is treated as an abstract data normally be where the ellipses now appear in (1) (or in (2)).
type with fields such as frequency, power, mode, etc. The Then the result of the said application is the sentence ob-
abstract domain of transmissions is introduced in Athena as tained from body by replacing every free occurrence of the
follows: quantified variable ?x:Transmission by the term t. In
Athena code, this procedure is defined as follows:
domain Transmission
d e f i n e apply :=
A transmission field (or “parameter”) can then be introduced lambda (C t)
as a function from transmissions to values of some appro- match C {
(forall x ((_ x) <==> body)) =>
priate sort. For illustration purposes, we demonstrate the (replace-var x t body) }
declaration of the following parameters: frequency, power,
mode, and time. Additional parameters can be introduced as The built-in ternary Athena procedure replace-var is
needed. such that (replace-var x t p) produces the result ob-
tained from the sentence p by replacing every free occur-
declare frequency: [Transmission] -> Int rence of variable x by the term p. As a concrete example,
declare power: [Transmission] -> Real here is a sample AC:
declare mode: [Transmission] -> Mode
declare hours, minutes: [Transmission] -> Int d e f i n e AC1 :=
(forall ?x .
Here Int and Real are built-in Athena sorts represent- allow ?x <==>
frequency ?x in [5000 5700] &
ing the sets of integers and real numbers, respectively, with power ?x < 30.0 &
Int a subsort of Real. The sort Mode is a finite algebraic mode ?x = everyDay & hours ?x <= 11)
datatype:
It says that a transmission is (provisionally) permissible iff
d a t a t y p e Mode := emergency | everyDay | ...
its frequency is in the 5000 . . . 5700 MHz range; its power is
There are two distinguished unary predicates on the set of less than 30.0 dBm; its mode is everyDay; and the trans-
all possible transmissions: allow and deny. These predi- mission’s time is no later than 11 in the morning. Here in is
cates are used by policies to specify which transmissions are a binary procedure defined as follows:
considered permissible and which are not. More concretely,
a policy is represented as a pair of sentences: an allow con- d e f i n e in :=
dition and a deny condition. An allow condition (or AC for lambda (x range)
short) is of the form: 2 match range {
[a b] => (a <= x & x <= b)}
(forall ?x:Transmission. allow ?x <==> · · · ) (1)
while a deny condition (DC) is of the form: (Note that variables do not need to be explicitly annotated
with their sorts. Athena has polymorphic sort inference, so
(forall ?x:Transmission. deny ?x <==> · · · ) (2) a Hindley-Milner algorithm will recover the most general
Either condition may be absent, i.e., a policy may specify possible sorts of all variable occurrences.) We can now con-
only an allow condition but no deny condition, or only a struct a policy with the above AC and with no DC as follows:
deny condition but no allow condition. An absent condition d e f i n e policy-1 := (make-policy AC1 ())
is represented by the unit value, (). The constructor for
policies is therefore a procedure that takes two conditions Our second policy example has both an AC and a DC:
and simply puts them together in a two-element list: d e f i n e policy-2 :=
d e f i n e make-policy := (make-policy
lambda (AC DC) [AC DC] (forall ?x .
allow ?x <==> mode ?x = emergency)
(forall ?x .
There are two destructor or selector procedures, one for re- deny ?x <==> power ?x > 25.0))
trieving each component of the policy:
d e f i n e [get-AC get-DC] := [first second]
A key operation on policies is that of merging. New policies
may be downloaded into the policy database at any given
An important operation is the application of a given pol- time. A newly acquired policy must be integrated with the
icy condition C of the form (1) or (2) to a term t of sort existing policy that is in place in order to produce a single
Transmission. Let body be whatever sentence would merged policy with a new AC and a new DC. Merging is
2
therefore a binary operation. The current definition of merg-
A more accurate term instead of allow would be “allow provi- ing two policies p1 and p2 is simple: it is disjunction on
sionally,” because, as we will see, for a transmission request to be
granted, the allow condition must hold and the deny condition must both the AC and DC. Specifically, the AC of the merged pol-
not hold. With this caveat in mind, we will continue to use the term icy allows a transmission t iff p1 allows t or p2 allows it;
allow in the interest of simplicity. and it denies t iff p1 denies it or p2 denies it. Merging is
implemented as an Athena procedure. Other alternative def- a yes/no answer from the policy system. But in general the
initions of merging are possible, and these could be straight- policy system needs to solve more interesting versions of this
forwardly implemented in the same way. As an example, problem, namely: If the transmission request is granted, find
here is the result of merging policy-1 and policy-2, appropriate values for any missing parameters, in case the
as these were defined above: request was incomplete; if the request is not granted, find ap-
d e f i n e merged-policy := propriate values for the transmission parameters that would
(merge-policies policy-1 policy-2) render the transmission permissible. Moreover, in the sec-
ond case, we often want to compute values in a way that is
>(get-AC merged-policy) optimal w.r.t. to the given request, e.g., so that the original
transmission request is disrupted as little as possible. We
Sentence:
(forall ?v4:Transmission discuss such optimality issues in section 4.
(iff (allow ?v4) The above problems are naturally formulated as satisfia-
(or (and (and (<= 5000 bility problems. However, the most appropriate satisfiability
(frequency ?v4)) framework here is not that of straight propositional logic, but
(<= (frequency ?v4) rather that of satisfiability modulo theories, or SMT for short
5700))
(and (< (power ?v4) [15]. In the SMT paradigm, the solver is given an arbitrary
30.0) formula of first-order logic with equality and its task is to de-
(and (= (mode ?v4) termine whether or not the formula is satisfiable with respect
everyDay) to certain background theories. Typical background theories
(<= (hours ?v4) of interest are integer and/or real arithmetic (typically linear,
11))))
(= (mode ?v4) but not necessarily), inductive data types (free algebras), the
emergency)))) theory of uninterpreted functions, as well as theories of lists,
arrays, bit vectors, etc. Hence, most of the function symbols
>(get-DC merged-policy) and predicates that appear in the input formula have fixed in-
terpretations, given by these background theories. An SMT
Sentence: (forall ?v5:Transmission
(iff (deny ?v5) solver will not only determine whether a sentence p is satisfi-
(> (power ?v5) able; if it is, it will also provide appropriate satisfying values
25.0))) for the free variables and/or constants that occur in p.
Athena is integrated with a number of SMT solvers, such
(Note that while Athena accepts input in either infix or pre- as CVC3 and Yices; the one used for this project is Yices [6],
fix form, sentences are output in prefix for indentation pur- mostly because it can solve Max-SAT problems. The main
poses.) interface is given by a unary Athena procedure smt-solve,
We define a transmission request as a set of constraints which takes an arbitrary first-order sentence p and attempts
over some object of sort Transmission, typically just to determine its satisfiability with respect to the appropri-
a free variable ranging over Transmission. These con- ate theories. If successful, smt-solve will return a list of
straints, which are usually desired values for some—or all— values for all free variables and/or constants that occur in p.
of the transmission parameters, can be expressed simply as Some examples:
a sentence. A sample transmission request:
d a t a t y p e Day :=
d e f i n e request-1 := (frequency ?t = 150 &
Mon | Tue | Wed | Thu | Fri | Sat | Sun
mode ?t = everyDay &
hours ?t = 16)
>(smt-solve ?x = 2 & ?y = 3.4 |
?x = 5 & ?d = Mon)
This is a conjunction specifying that the frequency of the
desired transmission (represented by the free variable ?t) List: [(= ?y 3.4) (= ?x 2) (= ?d Mon)]
should be 150, its mode should be everyDay, and its time
should be between 4:00 and 4:59 (inclusive) in the evening. The input to smt-solve here was a disjunction of two
A transmission request may be incomplete, i.e., it may not conjunctions. The free variable ?d ranges over the datatype
specify desired values for every transmission parameter. The Day; while ?x and ?y range over Int and Real, respec-
preceding request was incomplete, since it did not specify tively. The output is a list of identities providing values for
values for the power and minutes parameters. each free variable that render the input satisfiable. Because
the argument to smt-solve is a sentence, i.e., a native
3. POLICY REASONING Athena data value, this provides a very flexible and high-
The main task of the policy system is this: determine bandwidth programmable interface to SMT solvers. This in-
whether the policies currently in place allow or deny a given terface proved extremely useful for our system.
transmission request. This is in fact the simplest formula- The policy reasoning problems described earlier have a
tion of the core reasoning problem, in that it only requires natural formulation in SMT. Specifically, consider an arbi-
trary transmission request tr, i.e., a first-order sentence with with the desired value vi of each transmission parameter pi .
a free variable x ranging over Transmission (there may The weight wi reflects the importance that the radio attaches
be other free variables as well). To determine whether tr to pi taking the value vi . The SMT solver will then try to
is allowed by the current policy: (1) We construct a longer find a satisfying assignment for the request that has maxi-
request, tr0 , which is the conjunction of (a) tr; (b) the appli- mal total weight. In that case, the request is not just a list
cation of the current policy’s AC to x; and (c) the application of constraints [c1 · · · cn ] but a list of pairs of constraints
of the negation of the current policy’s DC to x: and weights [[c1 w1 ] · · · [cn wn ]]. A sample trans-
tr & (apply (get-total-AC) x) & mission request might then be:
˜ (apply (get-total-DC) x) d e f i n e weighted-request :=
[[(frequency ?t = 8000) 10]
The procedure get-total-AC returns the AC of the cur- [(power ?t = 35.0) 15]
rent (“total”) policy; likewise for get-total-DC. So tr0 [(hours ?t = 13) 30]]
represents all the constraints imposed on the requested trans-
mission, both by the original transmission request, tr, and indicating that the relative importance of the frequency being
by the policy itself, whose AC must hold for the transmis- 8000 is 10, that of the power being 35.0 is 15, and that of
sion variable x while its DC must not. (2) We then run hours being 13 is 30. Suppose further that the policy in
smt-solve on tr’. If the result is a satisfying assignment, place has no DC and a disjunctive AC:
then the request is granted, and all we need to do is report
d e f i n e AC1 :=
values for any missing parameters (parameters that did not (forall ?t . allow ?t <==>
figure in the given request). If, by contrast, smt-solve (frequency ?t in [5000 7000] &
determines that tr’ is unsatisfiable, then tr in its given form power ?t <= 30.0 & hours ?t > 12) |
must be rejected. In that case we make a blank request con- (frequency ?t in [6000 9000] &
power ?t <= 40.0 & hours ?t <= 8))
sisting of the application of the policy’s AC to x conjoined
with the application of the negation of the policy’s DC to d e f i n e policy := (make-policy AC1 ())
x, and run smt-solve on it. This blank request therefore
imposes no constraints at all on the transmission apart from Now consider evaluating weighted-request with re-
those imposed by the policy. If the result is a satisfying as- spect to this policy. Clearly, the request cannot be allowed
signment, we provide it to the user, otherwise we report that as is. We can make it permissible in more than one way:
the current policy is unsatisfiable. (a) we could demand a change of frequency and power in
The Athena code for this algorithm is expressed in a pro- accordance with the values prescribed by the first branch of
cedure evaluate-request, which accepts an arbitrary AC1, while keeping the hours parameter to the requested
request and processes it as described above. Here is the out- value of 13; or (b) we could demand a change of the hours
put for the example of the previous section: parameter only, in accordance with the second disjunctive
>(evaluate-request request-1) branch of AC, while keeping the desired frequency and power
values; or (c) we could demand that all three parameter val-
Transmission allowed. Appropriate values ues change. From these possibilities, only (a) is optimal, in
for missing parameters: that it honors the original request to the greatest extent pos-
[(= (power ?t1) 20.0)]
sible (as determined by the given weights). Running this
example in our system results in the following output:
4. COMPUTING OPTIMAL ADJUSTMENTS >(evaluate-request weighted-request)
TO TRANSMISSION PARAMETERS
The following parts of the request
When a transmission request is denied, there are usually
could not be satisfied:
many different ways of modifying it so as to make it per-
missible. For instance, the solver could change the desired (= (power ?t) 35.0) (= (frequency ?t) 8000)
transmission’s time; or it could change its frequency; or it
could change its power and mode; or it could change all of Here is a maximally satisfying assignment:
the above. Some of these actions may be preferable to oth-
[(= (mode ?t) everyDay)
ers. For instance, the radio might be less willing to change (= (frequency ?t) 5999)
the time of the transmission, or its power level, rather than (= (power ?t) 30) (= (hours ?t) 13)]
the frequency. In such cases we want the policy system to
return a satisfying assignment that is optimal in the sense of By contrast, if we had changed the weight of the hours
respecting as many such preferences of the radio as possible. parameter from 30 to 20, the result would then change the
Our system achieves this in a flexible way by formulating hours parameter instead of the frequency and power, since
the problem as an (SMT) instance of Max-SAT. In its trans- retaining the values of the two latter parameters would result
mission request, the radio can provide a weight wi along in a maximum weight of 25.
Note that weights can be arbitrary integers or a special z in [720 800]) |
“infinite” token, indicating a hard constraint that must be (x in [500 600] & y in [30 40] &
satisfied. In fact this infinite weight is the one that Athena z in [920 925])
attaches to the constraints obtained from the AC (and the
negation of the DC) of the current policy. But radios can Suppose also that the desired values are x = 13, y = 15,
also use infinite weights in their requests. z = 922. The task is to find values for these variables that
Occasionally there may be additional requirements on the satisfy c while diverging from the desired values as little as
assignments returned by the policy system, beyond honor- possible. We can readily model this problem in a form that
ing the original request to the greatest extent possible. For is amenable to smt-solve-and-minimize as follows.
example, if a parameter value must change, we may want First we define the objective-function term t, as the sum of
the new value to be as close as possible to the original re- the three differences:
quested value. If we are not allowed to transmit at the exact d e f i n e t := (?d-x:Int + ?d-y:Int + ?d-z:Int)
desired time, for instance, we may want to transmit as close
to it as possible (as can be allowed by the currently installed with the difference terms defined as follows:
policies). To meet such requirements we generally need the
d e f i n e d-x-def :=
ability to perform optimization by minimizing some objec- (ite (x > 13) (?d-x = x - 13)
tive function, in this case the absolute difference between de- (?d-x = 13 - x))
sired and permissible parameter values. Most SMT solvers d e f i n e d-y-def :=
do not perform optimization (apart from Max-SAT, in the (ite (y > 15) (?d-y = y - 15)
case of Yices, though see below), but we can efficiently im- (?d-y = 15 - y))
d e f i n e d-z-def :=
plement an integer optimizer in terms of SMT solving. The (ite (z > 922) (?d-z = z - 922)
idea is to use binary search in order to discover the opti- (?d-z = 922 - z))
mal cost with as few calls to the SMT solver as possible: at
most O(log n) calls, where n is the maximum value that the Here ite is a simple if-then-else procedure:
objective function can attain. Specifically, let c be an arbi-
trary constraint that we wish to satisfy in such a way that d e f i n e ite :=
lambda (c x y) ((c ==> x) & (˜ c ==> y))
the value of some “cost” term t is minimized, where max is
the maximum value that can be attained by the cost function Assume that we do not know the exact maximum value that
(represented by t). (Tf this value is not known a priori, it t can attain, but we know that it cannot be more than 106 .
can be taken to be the greatest positive integer that can be We can then solve the problem with the following call:
represented on the computer.) The algorithm is the follow-
ing: We first try to satisfy c conjoined with the constraint d e f i n e diff-clauses :=
that the cost term t is between 0 and half of the maximum (d-x-def & d-y-def & d-z-def)
d e f i n e query := (c & diff-clauses)
possible value: 0 ≤ t ≤ (max div 2). If we fail, we recur-
sively call the algorithm and try to satisfy c augmented with >(smt-solve-and-minimize query t 1000000)
the constraint (max div 2) + 1 ≤ t ≤ max. Whereas, if
we succeed, we recursively call the algorithm and try to sat- List: [(= ?x 13) (= ?y 15) (= ?z 800)
isfy c augmented with the constraint 0 ≤ t ≤ (max div 4). (= ?d-x 0) (= ?d-y 0) (= ?d-z 122)]
Some care must be taken to get the bounds right on each
call, but this algorithm is guaranteed to converge to the min- This solution was found by a total of 8 calls to the SMT
imum value of t for which c is satisfied, provided of course solver (for a total time of about 100 milliseconds). Why
that the original constraint c is satisfiable for some value of were only 8 calls required when we started the binary search
t. This algorithm is implemented by a ternary Athena proce- with a maximum of 106 ? One would expect about log 106
dure smt-solve-and-minimize, such that calls to the smt solver, i.e., roughly 20 such calls. However,
our implementation uses the information returned by each
(smt-solve-and-minimize c t max) call to the SMT solver to speed up the search. That often
returns a satisfying assignment for c that minimizes t (whose results in drastic shortcuts, cutting down the total number of
maximum value is max). iterations by more than a factor of 2.
For example, suppose that x, y, and z are integer variables This procedure enables our system to optimize any quan-
to be solved for: tity that can be given an integer metric. Moreover, unlike
independent branch-and-bound algorithms for integer pro-
d e f i n e [x y z] := [?x:Int ?y:Int ?z:Int] gramming, it has the advantage that it allows not just for nu-
meric constraints, but for arbitrary boolean structure as well,
subject to the following disjunctive constraint: along with constraints from other theories such as reals, lists,
d e f i n e c := arrays, bit vectors, inductive datatypes, etc. While more so-
(x in [10 20] & y in [1 20] & phisticated approaches to optimization in the SMT paradigm
are beginning to emerge (e.g., [2]), the implementation de-
scribed here has been quite adequate for our purposes.
5. PERFORMANCE
In order to test our system we wrote an Athena program
that generates test instances, with two independently con-
trollable variables: parameter number and policy number.
In particular, we defined a procedure make-policy-set with
two parameters, param-num and policy-num. The output is
a list of policy-num policies, where each policy involves
param-num transmission parameters. The latter came from
Figure 1: SMT solving times for processing regular
a pre-declared pool of 100 transmission parameters, half of
transmission requests.
them integer-valued and the other half real-valued. We dis-
tinguished the following types of policies:
• permissive policies, which have only an AC; among all the preceding types. Specifically, 20% of the
policies in L are ordering/N policies. About 1/3 of these
• prohibitive policies, which have only a DC and no AC; ordering/N policies are permissive, 1/3 are prohibitive, and
1/3 mixed. The next 20% of L consists of equational/N poli-
• mixed policies, which have both.
cies, and these are again evenly split between permissive-,
• Ordering/N policies. These policies are parameter- prohibitive-, and mixed-policy subsets. The third 20% con-
ized over N > 0. Specifically, an ordering/N policy is tains inequational/N policies, and so forth. Once a list L of
one whose AC and/or DC is of the following form: policies is thereby obtained, we combine them all into a sin-
gle policy by folding the merge-policies operator over
(forall ?t:Transmission . D ?t <==> L, with the empty-policy as the identity element. It is
(f i1 ?t R1 ci1 ) & ... & (f ik ?t Rk cik )) with respect to this merged policy that we tested transmis-
sion requests. The requests were generated randomly.
where D is either allow or deny, and ∀ j ∈ {1, . . . , k}: Figure 1 shows the SMT-solving times for processing plain
f ij is a transmission parameter; Rj ∈ {<, >, <=, >=}; transmission requests (i.e., without weights attached to the
and cij is a constant number of the appropriate sort. We various transmission parameters), for various combinations
refer to the ordering constraints (f ij ?t Rj cij ) as of policy-set sizes and transmission parameter numbers, where
the atoms of the AC (or DC). An ordering/N policy the policy sets are evenly mixed as described above. Fig-
may be permissive, prohibitive, or mixed, but its total ure 2 shows the corresponding times for optimal processing
number of atoms (i.e., the number of the AC’s atoms of transmission requests, i.e., requests that attach weights to
plus the number of the DC’s atoms) must equal N . each of the transmission parameters and are solved as Max-
SAT problems. In order to stress-test the implementation
• Equational/N policies. The AC and/or DC of such a
further, we repeated the experiments with sets of policies
policy is of the same form as shown above, except that
that were more structurally complex, doing away with sim-
each Ri is the identity relation. These identities are the
ple ordering, equational, and inequational policies, and us-
atoms of the condition. The total number of atoms (of
ing instead only range and disjunctive-conjunctive policies.
the AC and DC together) must be N .
The corresponding results are shown in Figure 3 and in Fig-
• Inequational/N policies. Same as above, except that
the relation in question here is inequality.
• Range/N policies. The AC and/or DC of such a policy
is of the same form as that of an ordering/N policy, ex-
cept that each Ri is the relation in, and each constant
ci is a range [a b].
• Disjunctive-Conjunctive/N policies. The AC and/or
DC of such a policy is a disjunction of conjunctions,
where each atom is of the form (f x ?t in [· · · ]).
The number of atoms are required to add up to N .
A call of the form (make-policy-set N P) returns
a list L containing P policies, each of which involves N trans- Figure 2: Max-SAT SMT solving times for optimized
mission parameters. This list is roughly equally partitioned processing of transmission requests.
to get the timing data. In most cases, the reported system
time (the sys entry of time’s output) was 0.000, i.e., too
small to be reliably measured, and hence the time reported
here is real (wall clock) time, which includes time seg-
ments spent by other processes and times during which the
SMT solver was blocked (e.g., waiting for I/O to complete).
Therefore, the times reported here are overly conservative;
the actual times spent on SMT solving are smaller.
6. RELATED WORK & CONCLUSIONS
Figure 3: Solving times for processing of transmission We have presented an implementation of a policy system
requests with structurally complex policies. for dynamic spectrum access. Policies are represented and
manipulated in Athena, a formal proof system for first-order
logic with polymorphism, subsorting, inductive datatypes,
ure 4. With these sort of structurally complex policies in arbitrary computation, and definitional extension. Most of
place, the highest increase occurs in optimal processing of these features have proven useful in the engine’s implemen-
transmission requests with more than 50 policies and param- tation; others would become useful if the engine were to be
eters. extended so that it used, e.g., structured ontologies instead
The graphs show only the time spent on SMT solving, of flat data types.
which is the bulk of the work that needs to be done when pro- Previous work in this area includes BBN’s XGPLF [8] and
cessing transmission requests. We do not include the time SRI’s Coral [10, 11]. XGPLF does not have a formal se-
spent on translating from Athena to SMT notation and back. mantics and is limited in what it can express (it is based on
This translation is a straightforward linear-time algorithm OWL [19]). Moreover, XGPLF cannot model inheritance.
(linear in the size of the formula to be translated, on average, To the best of our knowledge, the only implementation of
since it uses hash tables for the necessary mappings between a policy reasoning engine based on XGPLF is the one built
Athena and SMT namespaces), and the time spent on it in by the Shared Spectrum Company [12]. They used SWI-
most cases is neglibible. For huge policies containing hun- Prolog as the underlying reasoning engine. In field tests us-
dreds of thousands of nodes, the translation does take longer, ing resource-limited radio devices, SSC replaced the Prolog
though still typically a fraction of a second. Virtually all of reasoner with “a simplified reasoner developed in C/C++”
the translation cost is incurred when translating the policy, [12, p. 504]; no details are provided regarding the design,
since the transmission requests are tiny by comparison. Ob- implementation, or correctness of this simplified reasoner.
serve, however, that there is no reason to be translating the SSC’s engine can only return yes/no answers to transmission
entire policy anew each time the engine needs to process a requests.
new request. Instead, the (merged) policy can be translated Coral (Cognitive Radio Policy Language) is a new lan-
off-line, once, and subsequently cached in SMT notation in guage specifically designed for expressing policies govern-
some file. Thus, the translation time is an one-time, off-line ing the behavior of cognitive radios. Like Athena, Coral of-
cost. fers a rich and extensible first-order logical language that
All experiments were performed on a 2.4 GHz Intel Core includes arithmetic and allows for the introduction and def-
i3-370M dual-core processor with 4GB RAM, running Win- inition of new function symbols. It also features subtyping
dows 7. The time command of the Cygwin shell was used and can therefore express inheritance and ontologies. Some
notable differences from Athena include: (a) Unlike Coral,
Athena has polymorphism. Thus, e.g., it is not necessary
to introduce lists for integers and lists for booleans sepa-
rately; a generic parameterized definition is sufficient. (b)
Athena has automatic sort inference based on the Hindley-
Milner algorithm, which is convenient in practice because
it allows for shorter—and usually cleaner—specifications.
(c) Athena has a general-purpose formally defined program-
ming language that can seamlessly interact with its logical
layer, and which can be used to dynamically construct and
manipulate logical formulas very succinctly. This program-
ming language offers procedural abstraction, as well as side
effects through mutation, including reference cells and vec-
Figure 4: Max-SAT SMT solving times for transmission tors, features which are often important for efficiency. The
requests with structurally complex policies. ability to compute with terms and sentences as primitive data
values was very useful. While Coral can express some com- system that was recently implemented at Virginia Tech [1,
putations via universally quantified identities which can then 5]. Unlike the other systems discussed above, Bresap is lim-
be interpreted as executable rewrite rules by a tool such as ited to policies that can be adequately represented as finite
Maude [16], it does not offer procedural abstraction, i.e., it Boolean functions, which it encodes as binary decision di-
is not possible to define arbitrary procedures. agrams (BDDs). Therefore, unlike Coral and our system,
Two policy engines based on Coral have been implemented Bresap is not suitable as an expressive language for specify-
[10, 11]. The initial implementation used Prolog as the un- ing policies. For instance, it has no facilities for introducing
derlying reasoning engine, and was only able to return yes/no new policy concepts and/or rules. Indeed, Bresap is not a
answers to transmission requests. The second (and current) language. It is a system that reads certain types of policies
implementation uses a custom-made proof system to rea- expressed in XML and converts them to BDDs. This is done
son about transmission requests. The system has four kinds by assigning a distinct Boolean variable to each atomic ex-
of proof rules: forward chaining, backward chaining, par- pression that appears in the policy. For instance, a policy
tial evaluation based on conditional rewriting, and constraint such as “allow transmission in the frequency range a . . . b
propagation and simplification. The proof system is im- if the power does not exceed m” would result in the intro-
plemented in the rewriting engine Maude. One issue with duction of two distinct Boolean variables x1 and x2 , with
this implementation is that a positive answer is given only x1 corresponding to the atom a ≤ f ≤ b (where f stands
if the transmission request is an exact match of the opera- for the transmission’s frequency); and with x2 correspond-
tive policy conditions. But that is not likely to be the case ing to the atomic expression p ≤ m (where p stands for the
in practice. Most transmission requests are likely to be in- transmission’s power). The accepting condition could then
complete or to diverge from the policy, at least in some small be represented by the boolean function x1 ∧ x2 . Graph al-
degree. In such cases, the Coral implementation does not re- gorithms are used to merge different policy BDDs. With a
turn values for the relevant transmission parameters. Rather, single BDD in place representing the result of merging all
it returns an arbitrarily complicated first-order formula rep- active policies, Bresap can then accept an incoming trans-
resenting all the possible “opportunity constraints” that the mission request and evaluate it. A transmission request must
radio could use to modify its request so as to make it per- be an attribute-value list of the form a1 = v1 , . . . , an = vn ,
missible. But that is not likely to be of much use to the where ai is a transmission parameter (such as mode or fre-
requesting party. It is not realistic to require that whoever quency) and vi is the corresponding desired value. Notably,
made the transmission request should be able to understand Bresap is capable of handling underspecified (incomplete)
and reason about arbitrarily complicated logical formulas in requests. It is also capable of attaching costs to transmission
order to understand the policy system’s output. parameters (where a given cost indicates the penalty paid for
A second issue with this implementation is efficiency. The changing the value of that parameter), and then modifying
Coral team has not published precise benchmarks describing the parameter values of a transmission request in a way that
their engine’s performance for variable numbers and types of minimizes the overall cost.
policies (and for variable numbers of transmission parame- A drawback of Bresap is that the underlying policy repre-
ters), but they have released a demo of their implementation sentation framework, that of BDDs (or propositional logic,
that can be used to evaluate transmission requests with re- more generally), lacks semantics for the numeric constraints
spect to policies that have a fixed set of transmission param- that pervade spectrum access policies. To put it simply, BDDs
eters, namely: location (latitude and longitude); time (hours, do not know arithmetic, and thus do not have the where-
minutes, and seconds); sensed power; emissions; network withal to “understand” that < is transitive, that 1 + x is
id; and role (slave/master). Even with this fairly small set of greater than x, that 10 and 14 − 4 are the same object, and
transmission parameters, and with only 11 active policies in so on. Whereas an SMT solver immediately realizes that
place, it has been reported [1, p. 18] that evaluating a sin- f < 10 conjoined with f ≥ 30 is contradictory, because
gle transmission request took the Coral engine 58 seconds, it uses a dedicated reasoning procedure for arithmetic, in
and resulted in an output formula comprising 75 constraints. the approach of Bresap these two atoms would result in the
In the preceding section we saw that our implementation can introduction of two Boolean variables, x1 and x2 , the for-
evaluate transmission requests with several dozens of param- mer representing f < 10 and the latter representing f ≥
eters and with over 50 complex policies in place in a fraction 30. Thus, the conjunction of x1 and x2 is represented by
of a second; this is so even when the requests are processed the innocuous-looking Boolean function x1 ∧ x2 , a perfectly
optimally. Moreover, the Coral engine has no notion of opti- consistent condition. To represent the fact that in the present
mality. It does not allow the requesting party to specify that context this is actually inconsistent, one has to append to it
some parameters are more important than others, or to ask ad hoc clauses such as C = (¬x1 ∨ ¬x2 ) ∧ (x1 ∨ x2 ). This
that the request should be satisfied to the greatest extent pos- extra information, C, conjoined with x1 ∧ x2 , would then al-
sible, or with as little divergence from the requested values low us to conclude that the condition is unsatisfiable. That is,
as possible. in fact, what Bresap does: It “semantically analyzes” the var-
Another policy engine for spectrum access is Bresap, a ious atomic expressions in the policy in order to generate ad-
ditional constraints—so-called “auxiliary rules” [1, section Verification (CAV ’07), volume 4590 of Lecture Notes
3.5]—that prevent the engine from taking “illogical” paths in Computer Science, pages 298–302.
in the BDD. This approach has some disadvantages.3 First, Springer-Verlag, 2007. Berlin, Germany.
it is an essentially ad hoc encoding of arithmetic facts, the [8] BBN Technologies. XG Working Group, XG Policy
generation of which should not be part of the policy engine’s Language Framework, Request for Comments, version
trusted computing base. Second, the additional encoded in- 1.0. www.ir.bbn.com/projects/xmac/pollang.html,
formation, even if it is polynomial in size, can significantly 2004.
blow up the resulting BDD. Other efficiency issues in Bre- [9] Darpa. News Release for Next Generation (XG)
sap include the conversion algorithm that produces the BDD Communications Program Request for Comments.
from the atomic Boolean expressions of the policy. This al- www.darpa.mil/news/2004/xg_jun_04.pdf.
gorithm has exponential time complexity in the number of [10] G. Denker, D. Elenius, R. Senanayake, M.-O. Stehr,
expression variables. As a result, Bresap is not currently and D. Wilkins. A Policy Engine for Spectrum
able to handle policies with more than 20 atomic Boolean Sharing. In New Frontiers in Dynamic Spectrum
expressions [1, p. 83]. Access Networks, 2007. DySPAN 2007. 2nd IEEE
In conclusion, we believe that the combination of a pro- International Symposium on, pages 55 –65, April
grammable and expressive formal framework such as Athena 2007.
with an efficient SMT solver is a highly suitable implemen- [11] D. Elenius, G. Denker, M. O. Stehr, R. Senanayake,
tation vehicle for spectrum access policy engines. It com- C. Talcott, and D. Wilkins. CoRaL–Policy Language
bines rich expressivity with efficient performance, a consid- and Reasoning Techniques for Spectrum Policies.
eration that is likely to be crucial for cognitive radios. To Policies for Distributed Systems and Networks, IEEE
the best of our knowledge, SMT solvers have not been used International Workshop on, pages 261–265, 2007.
before for reasoning about policies, although we believe that [12] F. Perich. Policy-Based Network Management for
they are ideal for this task. Indeed, we believe that there NeXt Generation Spectrum Access Control. In New
is not much that is special about spectrum access, and that Frontiers in Dynamic Spectrum Access Networks,
the same approach we have introduced here could be used to 2007. DySPAN 2007. 2nd IEEE International
represent and reason about policies in other domains. Symposium on, pages 496 –506, April 2007.
[13] FCC Spectrum Policy Task Force. Report of the
7. REFERENCES spectrum efficiency working group. Available from
www.fcc.gov/sptf/files/SEWGFinalReport_1.pdf.
[1] A. A. Deshpande.
[14] I. F. Akyildiz and W.-Y. Lee and M. C. Vuran and S.
Policy Reasoning for Spectrum Agile Radios. Masters
Mohanty. NeXt Generation / Dynamic Spectrum
thesis, Electrical and Computer Engineering
Access / Cognitive Radio Wireless Networks: A
Department, Virginia Tech, 2010.
Survey. Computer Networks Journal (Elsevier),
[2] A. Cimatti and A. Franzn and A. Griggio and R.
50:2127–2159, September 2006.
Sebastiani and C. Stenico. Satisfiability Modulo the
[15] L. de Moura and B. Dutertre and N. Shankar. A
Theory of Costs: Foundations and Applications. In
Tutorial on Satisfiability Modulo Theories. In
TACAS 2010, pages 99–113, 2010.
Computer Aided Verification, volume 4590 of LNCS,
[3] K. Arkoudas. Athena.
pages 20–36. Springer, 2007.
http://www.pac.csail.mit.edu/athena.
[16] M. Clavel and F. Durán and S. Eker and P. Lincoln and
[4] B. A. Fette. Cognitive Radio Technology. Academic
N. Martı́-Oliet and J. Meseguer and C. Talcott. The
Press, 2nd edition, 2009.
Maude 2.0 System. In R. Nieuwenhuis, editor,
[5] B. Bahrak and A. A. Deshpande and M. Whitaker and
Rewriting Techniques and Applications (RTA 2003),
J. M. Park. BRESAP: A Policy Reasoner for
number 2706 in LNCS, pages 76–87. Springer, 2003.
Processing Spectrum Access Policies Represented by
[17] Q. Zhao. A Survey of Dynamic Spectrum Access.
Binary Decision Diagrams. In New Frontiers in
IEEE Signal Processing Magazine, 24(3):79–89,
Dynamic Spectrum, 2010 IEEE Symposium on, pages
2007.
1 –12, April 2010.
[18] R. Chadha and L. Kant. Policy-Driven Mobile Ad hoc
[6] B. Dutertre and L. de Moura. The Yices SMT Solver.
Network Management. Wiley-IEEE Press, 2007.
Tool paper, available online from
[19] World Wide Web Consortium. OWL 2 Web Ontology
yices.csl.sri.com/tool-paper.pdf.
Language Document Overview. Available from
[7] C. Barrett and C. Tinelli. CVC3. In W. Damm and
www.w3.org/TR/owl2-overview/, 2009.
H. Hermanns, editors, Proceedings of the 19th
International Conference on Computer Aided
3
Note that this criticism is not peculiar to Bresap. It applies to all
policy engines that represent semantically rich policies (requiring
at least linear arithmetic) as Boolean functions.