Searcharxiv⌕ Search

arXiv subjects

Alexander Kurz

Publications and source records attributed to Alexander Kurz.

At least 37 records · Page 2Linked to original sources
arXiv2018

Multi-type Display Calculus for Dynamic Epistemic Logic

In the present paper, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display-approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination.

math.LO↗
arXiv2017

Features of Agent-based Models

The design of agent-based models (ABMs) is often ad-hoc when it comes to defining their scope. In order for the inclusion of features such as network structure, location, or dynamic change to be justified, their role in a model should be systematically analysed. We propose a mechanism to compare and assess the impact of such features. In particular we are using techniques from software engineering and semantics to support the development and assessment of ABMs, such as graph transformations as semantic representations for agent-based models, feature diagrams to identify ingredients under consideration, and extension relations between graph transformation systems to represent model fragments expressing features.

cs.MA↗
arXiv2016

Multi-type Sequent Calculi

Display calculi are generalized sequent calculi which enjoy a `canonical' cut elimination strategy. That is, their cut elimination is uniformly obtained by verifying the assumptions of a meta-theorem, and is preserved by adding or removing structural rules. In the present paper, we discuss a proof-theoretic setting, inspired both to Belnap's Display Logic and to Sambin's Basic Logic, which generalises these calculi in two directions: by explicitly allowing different types, and by weakening the so-called display and visibility properties. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals, or logics that are not closed under uniform substitution. In the present paper, we give a general overview of the calculi which we refer to as multi-type calculi, and we discuss their canonical cut elimination meta-theorem.

math.LO↗
arXiv2016

Electron contribution to the muon anomalous magnetic moment at four loops

We present results for the QED contributions to the anomalous magnetic moment of the muon containing closed electron loops. The main focus is on perturbative corrections at four-loop order where the external photon couples to the external muon. Furthermore, all four-loop contributions involving simultaneously a closed electron and tau loop are computed. In combination with our recent results on the light-by-light-type corrections (see Ref. \cite{Kurz:2015bia}) the complete four-loop electron-loop contribution to the anomalous magnetic moment of the muon has been obtained with an independent calculation. Our calculation is based on an asymptotic expansion in the ratio of the electron and the muon mass and shows the importance of higher order terms in this ratio. We perform a detailed comparison with results available in the literature and find good numerical agreement. As a by-product we present analytic results for the on-shell muon mass and wave function renormalization constants at three-loop order including massive closed electron and tau loops, which we also calculated using the method of asymptotic expansion.

hep-ph↗
arXiv2016

Tool support for reasoning in display calculi

We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, that allows us to adapt the tool for a wide variety of user defined calculi.

cs.LO↗
arXiv2015

Positive fragments of coalgebraic logics

Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weak-pullback preserving functors. To facilitate this analysis we prove a number of category theoretic results on functors on the categories $\mathsf{Set}$ of sets and $\mathsf{Pos}$ of posets: Every functor $\mathsf{Set} \to \mathsf{Pos}$ has a $\mathsf{Pos}$-enriched left Kan extension $\mathsf{Pos} \to \mathsf{Pos}$. Functors arising in this way are said to have a presentation in discrete arities. In the case that $\mathsf{Set} \to \mathsf{Pos}$ is actually $\mathsf{Set}$-valued, we call the corresponding left Kan extension $\mathsf{Pos} \to \mathsf{Pos}$ its posetification. A $\mathsf{Set}$-functor preserves weak pullbacks if and only if its posetification preserves exact squares. A $\mathsf{Pos}$-functor with a presentation in discrete arities preserves surjections. The inclusion $\mathsf{Set} \to \mathsf{Pos}$ is dense. A functor $\mathsf{Pos} \to \mathsf{Pos}$ has a presentation in discrete arities if and only if it preserves coinserters of `truncated nerves of posets'. A functor $\mathsf{Pos} \to \mathsf{Pos}$ is a posetification if and only if it preserves coinserters of truncated nerves of posets and discrete posets. A locally monotone endofunctor of an ordered variety has a presentation by monotone operations and equations if and only if it preserves $\mathsf{Pos}$-enriched sifted colimits.

math.CT↗
arXiv2015

Presenting Distributive Laws

Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages.

cs.LO↗
arXiv2015

Light-by-light-type corrections to the muon anomalous magnetic moment at four-loop order

The numerically dominant QED contributions to the anomalous magnetic moment of the muon stem from Feynman diagrams with internal electron loops. We consider such corrections and present a calculation of the four-loop light-by-light-type corrections where the external photon couples to a closed electron or muon loop. We perform an asymptotic expansion in the ratio of electron and muon mass and reduce the resulting integrals to master integrals which we evaluate using analytical and numerical methods. We confirm the results present in the literature which are based on different computational methods.

hep-ph↗
arXiv2014

Simplified Coalgebraic Trace Equivalence

The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. LTS. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard LTS and probabilistic labelled transition systems.

cs.LO↗
arXiv2014

Higher-order hadronic and heavy-lepton contributions to the anomalous magnetic moment

We report about recent results obtained for the muon anomalous magnetic moment. Three-loop kernel functions have been computed to obtain the next-to-next-to-leading-order hadronic vacuum polarization contributions. The numerical result, $a_μ^{\rm{had,NNLO}}=1.24\pm 0.01 \times 10^{-10}$, is of the same order of magnitude as the current uncertainty from the hadronic contributions. For heavy-lepton corrections, analytical results are obtained at four-loop order and compared with the known results.

hep-ph↗
arXiv2014

Hadronic contribution to the muon anomalous magnetic moment to next-to-next-to-leading order

We compute the next-to-next-to-leading order hadronic contribution to the muon anomalous magnetic moment originating from the photon vacuum polarization. The corresponding three-loop kernel functions are calculated using asymptotic expansion techniques which lead to analytic expressions. Our final result, $a_μ^{\rm had,NNLO} = 1.24 \pm 0.01 \times 10^{-10}$, has the same order of magnitude as the current uncertainty of the leading order hadronic contribution and should thus be included in future analyses.

hep-ph↗
arXiv2013

Anomalous magnetic moment with heavy virtual leptons

We compute the contributions to the electron and muon anomalous magnetic moment induced by heavy leptons up to four-loop order. Asymptotic expansion is applied to obtain three analytic expansion terms which show rapid convergence.

hep-ph↗
arXiv2013

Nominal Regular Expressions for Languages over Infinite Alphabets. Extended Abstract

We propose regular expressions to abstractly model and study properties of resource-aware computations. Inspired by nominal techniques -- as those popular in process calculi -- we extend classical regular expressions with names (to model computational resources) and suitable operators (for allocation, deallocation, scoping of, and freshness conditions on resources). We discuss classes of such nominal regular expressions, show how such expressions have natural interpretations in terms of languages over infinite alphabets, and give Kleene theorems to characterise their formal languages in terms of nominal automata.

cs.FL↗
arXiv2013

Relation lifting, with an application to the many-valued cover modality

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.

cs.LO↗