arXiv subjects

Benjamin Engel

Publications and source records attributed to Benjamin Engel.

4 recordsLinked to original sources

arXiv2026

Four negations and the spectral presheaf

Using Vakarelov's theory of lattice logics with negation, we introduce the (co)quasiintuitionistic logic, and prove its soundness and completeness with respect to the class of (co)quasiintuitionistic algebras. Combining these algebras together, we obtain biquasiintuitionistic algebras and the biquasiintuitionistic logic. Their further extension with the Skolem algebra structure defines Akchurin algebras and the respective logic, which is a product of biquasiintuitionistic and biintuitionistic logics, featuring four distinct negations. Next we generalise the framework of spectral presheaves (which is a main object in the Butterfield--Isham--D\"{o}ring topos theoretic approach to quantum mechanics) to arbitrary complete orthocomplemented lattices, and show that the orthocomplementation determines two negation operators on the spectral presheaf (one paraconsistent, another paracomplete), equipping the set of all closed-and-open subpresheaves of a spectral presheaf with the structure of a biquasiintuitionistic algebra. Combined with the generic Skolem (i.e. Heyting and Brouwer) algebra structure of this set, this gives a particular instance of an Akchurin algebra. We also show that the underlying orthocomplemented lattice can be reconstructed as an internal object of the spectral presheaf, resulting as the image of a double coquasiintuitionistic (resp., quasiintuitionistic) negation monad (resp., comonad). Finally, we prove a no-go theorem for the claim that the spectral presheaf is a model of a dialectical (or any other) relevance logic.

math.LO↗

arXiv2024

The Structure of Emulations in Classical Spin Models: Modularity and Universality

The theory of spin models intersects with condensed matter physics, complex systems, graph theory, combinatorial optimization, computational complexity and neural networks. Many ensuing applications rely on the fact that complicated spin models can be transformed to simpler ones. What is the structure of such transformations? Here, we provide a framework to study and construct emulations between spin models. A spin model is a set of spin systems, and emulations are efficiently computable simulations with arbitrary energy cut-off, where a source spin system simulates a target system if, below the cut-off, the target Hamiltonian is encoded in the source Hamiltonian. We prove that emulations preserve important properties, as they induce reductions between computational problems such as computing ground states, approximating partition functions and approximate sampling from Boltzmann distributions. Emulations are modular (they can be added, scaled and composed), and allow for universality, i.e. certain spin models have maximal reach. We prove that a spin model is universal if and only if it is scalable, closed and functional complete. Because the characterization is constructive, it provides a step-by-step guide to construct emulations. We prove that the 2d Ising model with fields is universal, for which we also provide two new crossing gadgets. Finally, we show that simulations can be computed by linear programs. While some ideas of this work are contained in [1], we provide new definitions and theorems. This framework provides a toolbox for applications involving emulations of spin models.

math-ph↗

arXiv2014

Log-concavity of the overpartition function

We prove that the overpartition function is log-concave for all n>1. The proof is based on Sills Rademacher type series for the overpartition function and inspired by Desalvo and Pak's proof for the partition function.

math.NT↗

arXiv2012

Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code

Reliability in terms of functional properties from the safety-liveness spectrum is an indispensable requirement of low-level operating-system (OS) code. However, with evermore complex and thus less predictable hardware, quantitative and probabilistic guarantees become more and more important. Probabilistic model checking is one technique to automatically obtain these guarantees. First experiences with the automated quantitative analysis of low-level operating-system code confirm the expectation that the naive probabilistic model checking approach rapidly reaches its limits when increasing the numbers of processes. This paper reports on our work-in-progress to tackle the state explosion problem for low-level OS-code caused by the exponential blow-up of the model size when the number of processes grows. We studied the symmetry reduction approach and carried out our experiments with a simple test-and-test-and-set lock case study as a representative example for a wide range of protocols with natural inter-process dependencies and long-run properties. We quickly see a state-space explosion for scenarios where inter-process dependencies are insignificant. However, once inter-process dependencies dominate the picture models with hundred and more processes can be constructed and analysed.

cs.LO↗