Strategy logic (SL) is a powerful temporal logic that enables first-class reasoning over strategic behavior in multi-agent systems (MAS). In many MASs, the agents (and their strategies) cannot observe the global state of the system, leading to many extensions of SL centered around imperfect information, such as strategy logic with imperfect information (SL$_\mathit{ii}$). Along orthogonal lines, researchers have studied the combination of strategic behavior and hyperproperties. Hyperproperties are system properties that relate multiple executions in a system and commonly arise when specifying security policies. Hyper Strategy Logic (HyperSL) is a temporal logic that combines quantification over strategies with the ability to express hyperproperties on the executions of different strategy profiles. In this paper, we study the relation between SL$_\mathit{ii}$ and HyperSL. Our main result is that both logics (restricted to formulas where no state formulas are nested within path formulas) are equivalent in the sense that we can encode SL$_\mathit{ii}$ instances into HyperSL instances and vice versa. For the former direction, we build on the well-known observation that imperfect information is a hyperproperty. For the latter direction, we construct a self-composition of MASs and show how we can simulate hyperproperties using imperfect information.

Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem. We implement our encoding in a prototype verification tool and report on encouraging experimental results.

A popular artificial intelligence method provides a powerful tool for the survey and classification of biological data. But for the illiterate, technology presents significant difficulties. Four years ago, Google scientists showed up at neuroscientist Steve Finkbeiner's door. The researchers were based at Google Accelerated Science, a research division in Mountain View, Calif., which aims to use Google technologies to speed up the scientific search. They were also interested in applying a'deep-learning' approach to the mountains of imaging data generated by Finkbeiner's team at the Gladstone Institute of Neurological Disease in San Francisco, California.

Susanne Rafelski and her colleagues had a deceptively simple goal. "We wanted to be able to label many different structures in the cell, but do live imaging," says the quantitative cell biologist and deputy director of the Allen Institute for Cell Science in Seattle, Washington. "And we wanted to do it in 3D." That kind of goal normally relies on fluorescence microscopy -- problematic in this case because, with only a handful of colours to use, the scientists would run out of labels well before they ran out of structures. Also problematic is that these reagents are pricey and laborious to use.

Computers may be taught to identify features in nerve cells that have not been stained or undergone other damaging treatments for microscope use, an approach with the potential to revolutionize the way researchers study neurodegenerative diseases such as Parkinson's. "Researchers are now generating extraordinary amounts of data. For neuroscientists, this means that training machines to help analyze this information can help speed up our understanding of how the cells of the brain are put together and in applications related to drug development," Margaret Sutherland, PhD, said in a press release. Sutherland is program director at the National Institute of Neurological Disorders and Stroke (NINDS), which helps fund the research. The study "In silico labeling: Predicting fluorescent labels in unlabeled images" was published in the journal Cell.

It's harder than you might think to look at a microscope image of an untreated cell and identify its features. To make cell characteristics visible to the human eye, scientists normally have to use chemicals that can kill the very cells they want to look at. A groundbreaking study shows that computers can see details in images without using these invasive techniques. They can examine cells that haven't been treated and find a wealth of data that scientists can't detect on their own. In fact, images contain much more information than was ever thought possible.

In 2007, I spent the summer before my junior year of college removing little bits of brain from rats, growing them in tiny plastic dishes, and poring over the neurons in each one. For three months, I spent three or four hours a day, five or six days a week, in a small room, peering through a microscope and snapping photos of the brain cells. The room was pitch black, save for the green glow emitted by the neurons. I was looking to see whether a certain growth factor could protect the neurons from degenerating the way they do in patients with Parkinson's disease. This kind of work, which is common in neuroscience research, requires time and a borderline pathological attention to detail.

The brain's neural network has long inspired artificial-intelligence researchers.Credit: Alfred Pasieka/SPL/Getty Four years ago, scientists from Google showed up on neuroscientist Steve Finkbeiner's doorstep. The researchers were based at Google Accelerated Science, a research division in Mountain View, California, that aims to use Google technologies to speed scientific discovery. They were interested in applying'deep-learning' approaches to the mountains of imaging data generated by Finkbeiner's team at the Gladstone Institute of Neurological Disease in San Francisco, also in California. Deep-learning algorithms take raw features from an extremely large, annotated data set, such as a collection of images or genomes, and use them to create a predictive tool based on patterns buried inside. Once trained, the algorithms can apply that training to analyse other data, sometimes from wildly different sources.