In neural memory decoding, a concept being mentally recalled is identified using brain data. Recently, the feasibility of neural memory decoding with EEG data has been demonstrated. Here we propose a new application – neural information retrieval – that uses neural memory decoding to allow a document to be retrieved merely by thinking about it. In this paper we describe neural memory decoding, define the application of neural information retrieval, present experimental results related to the practicality of the application, and discuss issues of deployment and data privacy.

The California Public Utilities Commission collects and publishes data on mobile broadband service from major wireless service providers. The data is collected twice yearly at over 1900 measurement locations across California. The data can be used to assess the "digital divide", to track improvements in wireless service over time, and to help consumers select a service provider. For example, a consumer might want to know which provider offers the best service quality at important locations, like home and work. Here we apply machine learning and geospatial estimation methods to estimate each provider's wireless service quality at arbitrary locations across the state. We focus on TCP download performance. We find that Kriging, which takes into account the spatial correlation of service quality across measurement locations, yields better predictions than k-nearest neighbor and inverse distance weighting. We observe similar results when we rank providers rather than estimate the quality of service they provide. Finally, because average service performance across the state can be used to rank service providers, we estimate the minimum number of measurement locations that could be used to reliable rank service provider performance.

In designing new service plans, network service providers need to understand how consumption of voice or data service will change in response to pricing signals. It is difficult to acquire such information from customer usage data because voice minutes and data bandwidth are typically sold in the form of large quotas. We address this issue by studying how end-users consume their quotas, both in a prepaid setting (where users pay in advance and refill as needed) and a postpaid setting (where users pay each month for a fixed amount of quota). Our presentation has three main parts. In the first we present data on quota usage for prepaid voice/text services and show that users reduce their voice usage when their balances become low. Moreover, when balances are low there is a tendency to shift from voice to SMS. In the second part, we provide descriptive models of both prepaid and postpaid services. The main feature of these models is that there is a background level of potential demand and the rate at which this potential demand is realized depends on the amount of quota balance available. In the third part, we propose utility maximizing models that can account for this type of behavior. In the prepaid case the main feature of the model is a discount function that represents the perceived cost to the user of a quota refill that will occur sometime in the future. In the postpaid case, where the end-user is attempting to get the maximum amount of utility from his monthly quota, we present a dynamic programming formulation in which utility functions are time varying and not known to the user in advance.

Access control policy is typically defined in terms of attributes, but in many applications it is more natural to define permissions in terms of relationships that resources, systems, and contexts may enjoy. The paradigm of relationship-based access control has been proposed to address this issue, and modal logic has been used as a technical foundation.

Service negotiation allows a service client to negotiate with a service provider on the terms of service. Much existing work on service negotiation assumes that a provider will define its negotiation strategy in terms of the state of its resources. This approach can lead to complex strategy and assumes, unrealistically, that providers have full knowledge and control of their resources. We propose a hierarchical model of service negotiation in which negotiation strategy is defined in terms of sub-negotiations with internal or external agents. This model helps to manage the complexity of negotiation strategy by allowing it to be decomposed, with each component having well-defined scope. In this paper we present our hierarchical negotiation model, and a negotiation protocol and negotiation policy language based on it.

In “administrative ” access control, policy controls permis-sions not just on application actions, but also on actions to modify permissions, on actions to modify permissions on those actions, and so on. One context of work in admin-istrative policy is “administrative RBAC”, in which policy controls the permissions of roles, the membership of roles, and other elements of RBAC access-control state. Here we study and extend the UARBAC model for admin-istrative RBAC from the perspective of usability and expres-siveness. Using tools from logic and program verification, we formulate UARBAC logically and develop an algorithm that produces “administrative plans ” that achieve specified per-missions through permitted actions. This work is closely related to work on the safety problem in administrative ac-cess control, but is intended to aid legitimate users in under-standing how to achieve a desired access-control state. We then show how this machinery can be used so that admin-istrative actions at any desired depth, and so plans as well, can be uniformly simulated in the existing UARBAC model. 1.

Access control to IT systems increasingly relies on the ability to compose policies. Hence there is benefit in any framework for policy composition that is intuitive, formal (and so “analyzable” and “implementable”), expressive, independent of specific application domains, and yet able to be extended to create domain-specific instances. Here we develop such a framework based on Belnap logic. An access-control policy is interpreted as a four-valued predicate that maps access requests to either grant , deny , conflict , or unspecified -- the four values of the Belnap bilattice. We define an expressive access-control policy language PBel, having composition operators based on the operators of Belnap logic. Natural orderings on policies are obtained by lifting the truth and information orderings of the Belnap bilattice. These orderings lead to a query language in which policy analyses, for example, conflict freedom, can be specified. Policy analysis is supported through a reduction of the validity of policy queries to the validity of propositional formulas on predicates over access requests. We evaluate our approach through firewall policy and RBAC policy examples, and discuss domain-specific and generic extensions of our policy language.

It is difficult to develop and manage large, multi-author access control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for all desired policy compositions. In \cite{BH07}, a policy language was presented having policy combinators based on Belnap logic, a four-valued logic in which truth values correspond to policy results of "grant", "deny", "conflict", and "undefined". We show here how policies in this language can be analyzed, and study the expressiveness of the language. To support policy analysis, we define a query language in which policy analysis questions can be phrased. Queries can be translated into a fragment of first-order logic for which satisfiability and validity checks are computable by SAT solvers or BDDs. We show how policy analysis can then be carried out through model checking, validity checking, and assume-guarantee reasoning over such translated queries. We also present static analysis methods for the particular questions of whether policies contain gaps or conflicts. Finally, we establish expressiveness results showing that all {\em data independent} policies can be expressed in our policy language.

The points-to analysis problem is to find the pointer relationships that could arise during program execution. Many points-to analysis algorithms exist, each making a particular trade off between cost of the analysis and precision of the results. In this paper, we show how points-to analysis algorithms can be defined as transformed versions of an exact algorithm. We present a set of program transformations over a general program model and use them to define some existing points-to analysis algorithms. Doing so makes explicit the approximations involved in these algorithms. We also show how the transformations can be used to define new points-to analysis algorithms. Our transformations are generic and may be useful in the design of other program analysis algorithms.

The complexity of points-to analysis is well understood, but the approximations used to carry out points-to analysis efficiently are less well understood. In this paper we characterize points-to analysis as a reachability problem on a program's state space. Reachability analysis can be performed approximately but more efficiently for a program to which certain basic program transformations have been applied. We show the source of approximation and efficiency in several existing points-to analysis algorithms in terms of these generic program transformations.

A temporal logic query checker takes as input a Kripke structure and a temporal logic formula with a hole, and returns the set of propositional formulas that, when put in the hole, are satisfied by the Kripke structure. By allowing the temporal properties of a system to be discovered, query checking is useful in the study and reverse engineering of systems. Temporal logic query checking was first proposed by W. Chan (2000). In this paper, we generalize and simplify Chan's work by showing how a new class of alternating automata can be used for query checking with a wide range of temporal logics.

A form-based service is one in which the flow of data between service and user is described by a sequence of query/response interactions, or forms. Mawl is a domain-specific language for programming form-based services in a device-independent manner. We focus on Mawl's form abstraction, which is the means for separating service logic from user interface description, and show how this simple abstraction addresses seven issues in service creation, analysis, and maintenance: compile-time guarantees, implementation flexibility, rapid prototyping, testing and validation, support for multiple devices, composition of services, and usage analysis.

Abstract The MSMIE protocol [SBC89] allows processors in a distributed system to communicate via shared memory. It was designed to meet the reliability and efficiency needs of applications such as nuclear safety systems. We present a formal model of the MSMIE protocol expressed in the notation CCS. Desirable properties of the protocol are expressed in the modal mu-calculus, an expressive modal logic. We show that the protocol lacks an important liveness property. In actual operation, additional operating constraints are checked to avoid potential problems. We present a modified protocol and show that it possesses the liveness property even without checking operating constraints. We also show how parts of the analysis were automated with the Concurrency Workbench.