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.
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 in [2]. 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.
We describe a method for the neural decoding of memory from EEG data. Using this method, a concept being recalled can be identified from an EEG trace with an average top-1 accuracy of about 78.4% (chance 4%). The method employs deep representation learning with supervised contrastive loss to map an EEG recording of brain activity to a low-dimensional space. Because representation learning is used, concepts can be identified even if they do not appear in the training data set. However, reference EEG data must exist for each such concept. We also show an application of the method to the problem of information retrieval. In neural information retrieval, EEG data is captured while a user recalls the contents of a document, and a list of links to predicted documents is produced.
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.
Model checking has found a role in the engineering of reactive systems. However, model checkers are still strongly limited by the size of the system description they can check. Here we present a technique in which a system is simplified prior to model checking by the application of abstraction rules. The rules can greatly reduce the state space of a system description and help in understanding why a system satisfies a property. We illustrate the use of the technique on examples, including Dekker's mutual exclusion algorithm.
'%3e%3cpath fill='%23012169' d='M0 0v30h60V0z'/%3e%3cpath stroke='%23fff' stroke-width='6' d='m0 0 60 30m0-30L0 30'/%3e%3cpath stroke='%23C8102E' stroke-width='4' d='m0 0 60 30m0-30L0 30' clip-path='url(%23b)'/%3e%3cpath stroke='%23fff' stroke-width='10' d='M30 0v30M0 15h60'/%3e%3cpath stroke='%23C8102E' stroke-width='6' d='M30 0v30M0 15h60'/%3e%3c/g%3e%3c/svg%3e)
