Japan Advanced Institute of Science and Technology developed DCA2MC, a divide-and-conquer approach for model checking linear temporal properties. The method splits large verification problems into smaller, independently checkable tasks to address state-space explosion and improve performance through parallelization. A supporting tool is implemented in Maude and provides an environment integrating with external model checkers such as Spin, while a semi-automated method helps select effective layer configurations. Case studies demonstrated improved verification of larger state spaces.

The U.S. National Science Foundation has renewed the Quantum Leap Challenge Institute for Quantum Sensing for Biophysics and Bioengineering (NSF QuBBE) with a $37.5 million, five-year investment to advance quantum sensing technologies that can reveal biological processes difficult or impossible to observe with conventional tools.

Researchers from the University of Osaka have developed a fast computational framework that predicts the optical performance of quantum color centers without being restricted to a specific host material. By replacing computationally intensive calculations with simple theoretical formulas and procedures, the method enables rapid screening of promising quantum materials spanning ultraviolet to telecommunication wavelengths.

A modelling study finds that banks form interbank networks by balancing the benefits of sharing liquidity risk against incentives to rely on other banks' reserves. As networks grow, risk-sharing can initially improve expected profits, but free-riding can later reduce them. The findings suggest that relatively small networks may be most efficient and offer insights into “too-big-to-fail” and “too-interconnected-to-fail” risks.