2025-04-18 | | Total: 4
We formalise the notion of an \emph{anonymous public announcement} in the tradition of public announcement logic. Such announcements can be seen as in-between a public announcement from ``the outside" (an announcement of $\phi$) and a public announcement by one of the agents (an announcement of $K_a\phi$): we get more information than just $\phi$, but not (necessarily) about exactly who made it. Even if such an announcement is prima facie anonymous, depending on the background knowledge of the agents it might reveal the identity of the announcer: if I post something on a message board, the information might reveal who I am even if I don't sign my name. Furthermore, like in the Russian Cards puzzle, if we assume that the announcer's intention was to stay anonymous, that in fact might reveal more information. In this paper we first look at the case when no assumption about intentions are made, in which case the logic with an anonymous public announcement operator is reducible to epistemic logic. We then look at the case when we assume common knowledge of the intention to stay anonymous, which is both more complex and more interesting: in several ways it boils down to the notion of a ``safe" announcement (again, similarly to Russian Cards). Main results include formal expressivity results and axiomatic completeness for key logical languages.
We discuss string diagrams for timed process theories -- represented by duoidally-graded symmetric strict monoidal categories -- built upon the string diagrams of pinwheel double categories.
In the original work on the cost-aware logical framework by Niu et al., a dependent variant of the call-by-push-value language for cost analysis, the authors conjectured that the canonicity property of the type theory can be succinctly proved via Sterling's synthetic Tait computability. This work resolves the conjecture affirmatively.
Reachability of vector addition systems with states (VASS) is Ackermann complete~\cite{leroux2021reachability,czerwinski2021reachability}. For $d$-dimensional VASS reachability it is known that the problem is NP-complete~\cite{HaaseKreutzerOuaknineWorrell2009} when $d=1$, PSPACE-complete~\cite{BlondinFinkelGoellerHaaseMcKenzie2015} when $d=2$, and in $\mathbf{F}_d$~\cite{FuYangZheng2024} when $d>2$. A geometrically $d$-dimensional VASS is a $D$-dimensional VASS for some $D\ge d$ such that the space spanned by the displacements of the circular paths admitted in the $D$-dimensional VASS is $d$-dimensional. It is proved that the $\mathbf{F}_d$ upper bounds remain valid for the reachability problem in the geometrically $d$-dimensional VASSes with $d>2$.