skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Coalgebraic tools for randomness-conserving protocols}
We propose a coalgebraic model for constructing and reasoning about state-based protocols that implement efficient reductions among random processes. We provide basic tools that allow efficient protocols to be constructed in a compositional way and analyzed in terms of the tradeoff between latency and loss of entropy. We show how to use these tools to construct various entropy-conserving reductions between processes.  more » « less
Award ID(s):
1718108 1703846
PAR ID:
10094113
Author(s) / Creator(s):
;
Date Published:
Journal Name:
Relational and Algebraic Methods in Computer Science - 17th International Conference (RAMiCS 2018)
Page Range / eLocation ID:
298-313
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Bouyer, Patricia; Srinivasan, Srikanth (Ed.)
    Many derandomization results for probabilistic decision processes have been ported to the setting of Arthur-Merlin protocols. Whereas the ultimate goal in the first setting consists of efficient simulations on deterministic machines (BPP vs. P problem), in the second setting it is efficient simulations on nondeterministic machines (AM vs. NP problem). Two notable exceptions that have not yet been ported from the first to the second setting are the equivalence between whitebox derandomization and leakage resilience (Liu and Pass, 2023), and the equivalence between whitebox derandomization and targeted pseudorandom generators (Goldreich, 2011). We develop both equivalences for mild derandomizations of Arthur-Merlin protocols, i.e., simulations on Σ₂-machines. Our techniques also apply to natural simulation models that are intermediate between nondeterministic machines and Σ₂-machines. 
    more » « less
  2. null (Ed.)
    Automated reasoning tools for security protocols model protocols as non-deterministic processes that communicate through a Dolev-Yao attacker. There are, however, a large class of protocols whose correctness relies on an explicit ability to model and reason about randomness. Although such protocols lie at the heart of many widely adopted systems for anonymous communication, they have so-far eluded automated verification techniques. We propose an algorithm for reasoning about safety properties for randomized protocols. The algorithm is implemented as an extension of Stochastic Protocol ANalyzer (Span), the mechanized tool that reasons about the indistinguishability properties of randomized protocols. Using Span, we conduct the first automated verification on several randomized security protocols and uncover previously unknown design weaknesses in several of the protocols we analyzed. 
    more » « less
  3. An essential feature of many modern teacher observation protocols is their “global” approach to measuring instruction. Global protocols provide a summary evaluation of multiple domains of instruction from observers’ overall review of classroom processes.  Although these protocols have demonstrated strengths, including their comprehensiveness and advanced state of development, in this analysis we argue that global protocols also have inherent limitations affecting both research use and applied school improvement efforts.  Analyzing the Measures of Effective Teaching study data, we interrogate a set of five potential limitations of global protocols.  We conclude by discussing fine-grained measures of instruction, including tools that rely on automated methods of observation, as an alternative with the potential to overcome many of the fundamental limitations of global protocols. 
    more » « less
  4. Dynamical systems are commonly used to represent real-world processes. Model reduction techniques are among the core tools for studying dynamical systems models, they allow to reduce the study of a model to a simpler one. In this poster, we present an algorithm for computing exact nonlinear reductions, that is, a set of new rational function macro-variables which satisfy a self-consistent ODE system with the dynamics defined by algebraic functions. We report reductions found by the algorithm in models from the literature. 
    more » « less
  5. Quantum error correction (QEC) is believed to be essential for the realization of large-scale quantum computers. However, due to the complexity of operating on the encoded `logical' qubits, understanding the physical principles for building fault-tolerant quantum devices and combining them into efficient architectures is an outstanding scientific challenge. Here we utilize reconfigurable arrays of up to 448 neutral atoms to implement all key elements of a universal, fault-tolerant quantum processing architecture and experimentally explore their underlying working mechanisms. We first employ surface codes to study how repeated QEC suppresses errors, demonstrating 2.14(13)x below-threshold performance in a four-round characterization circuit by leveraging atom loss detection and machine learning decoding. We then investigate logical entanglement using transversal gates and lattice surgery, and extend it to universal logic through transversal teleportation with 3D [[15,1,3]] codes, enabling arbitrary-angle synthesis with logarithmic overhead. Finally, we develop mid-circuit qubit re-use, increasing experimental cycle rates by two orders of magnitude and enabling deep-circuit protocols with dozens of logical qubits and hundreds of logical teleportations with [[7,1,3]] and high-rate [[16,6,4]] codes while maintaining constant internal entropy. Our experiments reveal key principles for efficient architecture design, involving the interplay between quantum logic and entropy removal, judiciously using physical entanglement in logic gates and magic state generation, and leveraging teleportations for universality and physical qubit reset. These results establish foundations for scalable, universal error-corrected processing and its practical implementation with neutral atom systems. 
    more » « less