∗ 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.