arXiv subjects

Christoph Wagner

Publications and source records attributed to Christoph Wagner.

7 recordsLinked to original sources

arXiv2026

Roadmap on UV-C photodetectors: materials, applications and industry perspectives

UV-C photodetectors are poised to play an increasingly important role in future photonic technologies, driven by the rapid emergence of UV-C light sources and new wide bandgap semiconductors. These advances are enabling new levels of spectral selectivity, radiation hardness, sensitivity, and device integration, while opening opportunities across a broad range of applications. This roadmap provides a comprehensive overview of the current landscape of UV-C photodetection, spanning established and emerging material platforms (Ga2O3, AlGaN, BN, diamond, MgZnO, 2-dimensional materials, metal halide perovskites, micro-electromechanical systems), and their applications in metrology, astronomy, communications, environmental monitoring, fire detection, missile warning, gas sensing, and medical diagnostics. By identifying opportunities, bottlenecks, and future directions, this roadmap aims to support both newcomers and established researchers, with the aim of accelerating the translation of UV-C photodetectors into impactful technologies.

physics.app-ph↗

arXiv2023

FTMPST: Fault-Tolerant Multiparty Session Types

Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.

cs.LO↗

arXiv2020

Poster: Benchmarking Financial Data Feed Systems

Data-driven solutions for the investment industry require event-based backend systems to process high-volume financial data feeds with low latency, high throughput, and guaranteed delivery modes. At vwd we process an average of 18 billion incoming event notifications from 500+ data sources for 30 million symbols per day and peak rates of 1+ million notifications per second using custom-built platforms that keep audit logs of every event. We currently assess modern open source event-processing platforms such as Kafka, NATS, Redis, Flink or Storm for the use in our ticker plant to reduce the maintenance effort for cross-cutting concerns and leverage hybrid deployment models. For comparability and repeatability we benchmark candidates with a standardized workload we derived from our real data feeds. We have enhanced an existing light-weight open source benchmarking tool in its processing, logging, and reporting capabilities to cope with our workloads. The resulting tool wrench can simulate workloads or replay snapshots in volume and dynamics like those we process in our ticker plant. We provide the tool as open source. As part of ongoing work we contribute details on (a) our workload and requirements for benchmarking candidate platforms for financial feed processing; (b) the current state of the tool wrench.

cs.PF↗

arXiv2019

Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)

The additional complexity caused by concurrently communicating processes in distributed systems render the verification of such systems into a very hard problem. Multiparty session types were developed to govern communication and concurrency in distributed systems. As such, they provide an efficient verification method w.r.t. properties about communication and concurrency, like communication safety or progress. However, they do not support the analysis of properties that require the consideration of concrete runs or concrete values of variables. We sequentialise well-typed systems of processes guided by the structure of their global type to obtain interaction-free abstractions thereof. Without interaction, concurrency in the system is reduced to sequential and completely independent parallel compositions. In such abstractions, the verification of properties such as e.g. data-based termination that are not covered by multiparty session types, but rely on concrete runs or values of variables, becomes significantly more efficient.

cs.LO↗

arXiv2015

Encoding CSP into CCS

We study encodings from CSP into asynchronous CCS with name passing and matching, so in fact, the asynchronous pi-calculus. By doing so, we discuss two different ways to map the multi-way synchronisation mechanism of CSP into the two-way synchronisation mechanism of CCS. Both encodings satisfy the criteria of Gorla except for compositionality, as both use an additional top-level context. Following the work of Parrow and Sjödin, the first encoding uses a centralised coordinator and establishes a variant of weak bisimilarity between source terms and their translations. The second encoding is decentralised, and thus more efficient, but ensures only a form of coupled similarity between source terms and their translations.

cs.LO↗

arXiv2015

Encoding CSP into CCS (Extended Version)

We study encodings from CSP into asynchronous CCS with name passing and matching, so in fact, the asynchronous pi-calculus. By doing so, we discuss two different ways to map the multi-way synchronisation mechanism of CSP into the two-way synchronisation mechanism of CCS. Both encodings satisfy the criteria of Gorla except for compositionality, as both use an additional top-level context. Following the work of Parrow and Sjödin, the first encoding uses a central coordinator and establishes a variant of weak bisimilarity between source terms and their translations. The second encoding is decentralised, and thus more efficient, but ensures only a form of coupled similarity between source terms and their translations.

cs.LO↗

arXiv2014

States in Process Calculi

Formal reasoning about distributed algorithms (like Consensus) typically requires to analyze global states in a traditional state-based style. This is in contrast to the traditional action-based reasoning of process calculi. Nevertheless, we use domain-specific variants of the latter, as they are convenient modeling languages in which the local code of processes can be programmed explicitly, with the local state information usually managed via parameter lists of process constants. However, domain-specific process calculi are often equipped with (unlabeled) reduction semantics, building upon a rich and convenient notion of structural congruence. Unfortunately, the price for this convenience is that the analysis is cumbersome: the set of reachable states is modulo structural congruence, and the processes' state information is very hard to identify. We extract from congruence classes of reachable states individual state-informative representatives that we supply with a proper formal semantics. As a result, we can now freely switch between the process calculus terms and their representatives, and we can use the stateful representatives to perform assertional reasoning on process calculus models.

cs.LO↗