# Towards Collaborative and Dynamic Spectrum Sharing via Interpretation of Spectrum Access Policies
## 7 Discussion
However, as the authors state, \"A novel mix of reasoning techniques is required to implement such a reasoner.\" Descriptions of two implementations of CoRaL were published: one in Prolog and one in Maude [27]--a language and theorem proving system with a highly desirable expressiveness. The first implementation did not support the inference of transmission opportunities. The second one, to the best of our knowledge, has not been developed as a standalone system that would address the undecidability issues of Maude. Another attempt at a formal approach to DSA has been described in [28], in which Athena--a programming language and an interactive theorem proving environment--was used for experiments. It is based on first-order logic with arithmetic and algebraic data types and is a framework for working with constraint satisfaction problems (CSP) and satisfiability modulo theories (SMT), in which constraint solvers are used. According to the description of Athena available on its website, it is a theorem-proving environment that one can use for representing proofs and then verifying them. The formulation of the proofs is expected to be done by a human, or the human would have to specify some proof tactics that could be then used by the Athena processor. Clearly, Athena is a very good tool for experimenting with formal representations of policies and investigation of strategies for addressing issues of policy execution; however, this is not a standalone policy engine. The authors of [28] demonstrated that they can implement policy reasoning that includes the ability of returning transmission opportunities in case a request for transmission is not allowed. [PERSON] and their colleagues have developed a DSA system [29, 30] that used a modified Pellet reasoner for checking the consistency of ontologies and reasoning about policies and leveraged SWRL as the policy representation language. The focus of their work was on the derivation of opportunity constraints, to which end, they developed four different algorithms. To the best of our understanding, their goal was to address the issue of undecidability of reasoning in SWRL by limiting its expressiveness. The policy reasoner (BRESAP) frames the policy reasoning problem as a graph-based Boolean function manipulation problem and represents policies as Multi-Terminal Binary Decision Diagrams. While this apparently addresses some issues related to the computation complexity, it is also a limitation with regard to the expressiveness; it is limited to policies that can be adequately represented as finite Boolean functions, which it encodes as binary decision diagrams (BDDs). The last work that we selected comes from the Spectrum Sharing Company (SSC), one of the performers on the DARPA XG program. SSC was first developed to provide a proof of feasibility to the policy-based DSA [31]. Their first paper did not provide any details about the reasoner that was used in the implementation (\"the Policy Reasoner itself is implemented using numerous approaches\"). The second paper [32] stated that OWL Lite (a less expressive profile of OWL) was used for representing ontologies, and SWRL was used for representing policies. However, it seems that the reasoner was a proprietary implementation (\"Based on results from our initial Prolog-based implementation, we developed a C++ Policy Conformance Reasoner for meeting processor and main memory requirements\"). Finally, in [33], SSC summarized their experiences with the work on the XG program. Overall, SSC has made great contributions towards greater acceptance of the policy-based DSA, but their products are not easily accessible to a wider community. In summary, various ideas of how to address the trade-offs between the multiple competing criteria have been investigated. The main trade-off is between the expressiveness of the policy language and the computational cost of policy interpretation and execution.