Vectors addition systems with states (VASS), a model equivalent to Petri nets, are finite-state machines with finitely many counters ranging over the natural numbers. The decidable reachability problem for VASS has many applications in logic, automata, and verification. In this paper we study the reachability problem for BVASS, a branching generalization of VASS. We show that BVASS reachability sets are very similar to VASS reachability sets, namely that they are sections of VASS. Our proof relies on a new well-quasi-order (wqo) on BVASS runs that generalizes the well-known wqo on VASS runs. By leveraging an amalgamation property, we prove that every BVASS run can be transformed into an equivalent one of bounded branching complexity. This allows us to derive several results on the geometry of BVASS reachability sets. As an application we obtain that reachability sets of 5-dimensional BVAS are effectively semilinear, as is the case for 5-dimensional VAS.
Varieties of quantitative algebras, studied by Mardare, Panangaden and Plotkin, can be presented as categories of algebras for enriched monads on the categories Met (of metric spaces) or CMet (of complete metric spaces). We solve the open problem of whether the resulting monads are precisely the strongly finitary ones. The solution is negative: the monad corresponding to two ε -close binary operations is not strongly finitary. We characterize the monads representing varieties of quantitative algebras as precisely the 1-basic monads which are the weighted colimits of strongly finitary monads. We conclude that strongly finitary endofunctors on Met are not closed under composition.
We describe a categorical model of MALL (Multiplicative Additive Linear Logic) inspired by the Heisenberg-Schrödinger duality of finite-dimensional quantum theory. Proofs of formulas with positive logical polarity correspond to CPTP (completely positive trace-preserving) maps in our model, i.e. the quantum operations in the Schrödinger picture, whereas proofs of formulas with negative logical polarity correspond to CPU (completely positive unital) maps, i.e. the quantum operations in the Heisenberg picture. The mathematical development is based on noncommutative geometry and finite-dimensional von Neumann (co)algebras, which can be defined as special kinds of (co)monoid objects internal to the category of finite-dimensional operator spaces.
f-differential privacy (f-DP) is a recent definition for privacy which can offer improved predictions of “privacy loss”. It has been used to analyse specific privacy mechanisms, such as the popular Gaussian mechanism. In this paper we show how f-DP’s foundation in statistical hypothesis testing implies equivalence to the channel model of Quantitative Information Flow (QIF). We demonstrate this equivalence as a Galois connection between two partially-ordered sets, namely f-DP’s trade-off functions, and a class of information channels. This equivalence enables novel general composition theorems for f-DP, supporting improved analysis for complex privacy designs. We apply our results to the popular privacy amplification mechanisms of sub-sampling and purification, to produce novel f-DP profiles for these general privacy-enhancing algorithms.
Relational presheaves generalize traditional presheaves by going to the category of sets and relations (as opposed to sets and functions) and by allowing functors which are lax. This added generality is useful because it intuitively allows one to encode situations where we have representables without boundaries or with multiple boundaries at once. In particular, the relational generalization of precubical sets has natural application to modeling concurrency. In this article, we study categories of relational presheaves, and construct realization functors for those. We begin by observing that they form the category of set-based models of a cartesian theory, which implies in particular that they are locally finitely presentable categories. By using general results from categorical logic, we then show that the realization of such presheaves in a cocomplete category is a model of the theory in the opposite category, which allows characterizing situations in which we have a realization functor. Finally, we explain that our work has applications in the semantics of concurrency theory. The realization namely allows one to compare syntactic constructions on relational presheaves and geometric ones. Thanks to it, we are able to provide a syntactic counterpart of the blowup operation, which was recently introduced by Haucourt on directed geometric semantics, as way of turning a directed space into a manifold.
