arXiv subjects

Matthias Függer

Publications and source records attributed to Matthias Függer.

At least 19 recordsLinked to original sources

arXiv2026

Agent-Alternation-Free Epistemic Metric Temporal Logic with Past: Model Checking and Complexity

We study model checking for an epistemic metric temporal logic with past, interpreted over finite B\"uchi automata under synchronous perfect recall. The logic is motivated by observation-based verification problems such as diagnosis and opacity, where an observer sees only a projection of an execution and reasons about events that may have occurred earlier. These requirements use no alternation between different agents' knowledge. We therefore consider the agent-alternation-free fragment, in which nested knowledge operators must refer to the same agent. We show that model checking for this fragment is EXPSPACE-complete. The lower bound already holds with one agent, one occurrence of the knowledge operator, and no non-trivial metric bounds. For the upper bound, we combine temporal test automata with perfect-recall observers. Because past formulas may have different truth values on indistinguishable histories ending in the same system state, the observer must track temporal automaton states in addition to system states.

cs.LO↗

arXiv2026

Promoting Simple Agents: Ensemble Methods for Event-Log Prediction

We compare lightweight automata-based models (n-grams) with neural architectures (LSTM, Transformer) for next-activity prediction in streaming event logs. Experiments on synthetic patterns and five real-world process mining datasets show that n-grams with appropriate context windows achieve comparable accuracy to neural models while requiring substantially fewer resources. Unlike windowed neural architectures, which show unstable performance patterns, n-grams provide stable and consistent accuracy. While we demonstrate that classical ensemble methods like voting improve n-gram performance, they require running many agents in parallel during inference, increasing memory consumption and latency. We propose an ensemble method, the promotion algorithm, that dynamically selects between two active models during inference, reducing overhead compared to classical voting schemes. On real-world datasets, these ensembles match or exceed the accuracy of non-windowed neural models with lower computational cost.

cs.LG↗

arXiv2026

Provable Coordination for LLM Agents via Message Sequence Charts

Multi-agent systems built on large language models (LLMs) are difficult to reason about. Coordination errors such as deadlocks or type-mismatched messages are often hard to detect through testing. We introduce a domain-specific language for specifying agent coordination based on message sequence charts (MSCs). The language separates message-passing structure from LLM calls, tool calls, and human control points, whose outcomes remain unpredictable. We define the syntax and semantics of the language and present a syntax-directed projection that generates deadlock-free local agent programs from global coordination specifications. We illustrate the approach with a diagnosis consensus protocol and show how coordination properties can be established independently of LLM nondeterminism. We also describe a runtime planning extension in which an LLM dynamically generates a coordination workflow for which the same structural guarantees apply. An open-source Python implementation of our framework is available as ZipperGen.

cs.PL↗

arXiv2026

Reaching Agreement in Competitive Microbial Systems

We study distributed agreement in microbial distributed systems under stochastic population dynamics and competitive interactions. Motivated by recent applications in synthetic biology, we examine how the presence and absence of direct competition among microbial species influences their ability to reach majority consensus. In this problem, two species are designated as input species, and the goal is to guarantee that eventually only the input species which had the highest initial count prevails. We show that direct competition dynamics reach majority consensus with high probability even when the initial gap between the species is small, i.e., $Ω(\sqrt{n\log n})$, where $n$ is the initial population size. In contrast, we show that absence of direct competition is not robust: solving majority consensus with constant probability requires a large initial gap of $Ω(n)$. To corroborate our analytical results, we use simulations to show that these consensus dynamics occur within practical biological time scales.

cs.DC↗

arXiv2026

Asymptotic Subspace Consensus in Dynamic Networks

We introduce the problem of asymptotic subspace consensus, which requires the outputs of processes to converge onto a common subspace while remaining inside the convex hull of initial vectors.This is a relaxation of asymptotic consensus in which outputs have to converge to a single point, i.e., a zero-dimensional affine subspace. We give a complete characterization of the solvability of asymptotic subspace consensus in oblivious message adversaries. In particular, we show that a large class of algorithms used for asymptotic consensus gracefully degrades to asymptotic subspace consensus in distributed systems with weaker assumptions on the communication network. We also present bounds on the rate by which a lower-than-initial dimension is reached.

cs.DC↗

arXiv2025

Centralized Permutation Equivariant Policy for Cooperative Multi-Agent Reinforcement Learning

The Centralized Training with Decentralized Execution (CTDE) paradigm has gained significant attention in multi-agent reinforcement learning (MARL) and is the foundation of many recent algorithms. However, decentralized policies operate under partial observability and often yield suboptimal performance compared to centralized policies, while fully centralized approaches typically face scalability challenges as the number of agents increases. We propose Centralized Permutation Equivariant (CPE) learning, a centralized training and execution framework that employs a fully centralized policy to overcome these limitations. Our approach leverages a novel permutation equivariant architecture, Global-Local Permutation Equivariant (GLPE) networks, that is lightweight, scalable, and easy to implement. Experiments show that CPE integrates seamlessly with both value decomposition and actor-critic methods, substantially improving the performance of standard CTDE algorithms across cooperative benchmarks including MPE, SMAC, and RWARE, and matching the performance of state-of-the-art RWARE implementations.

cs.MA↗

arXiv2025

A Hybrid Delay Model for Interconnected Multi-Input Gates

Dynamic digital timing analysis is a less accurate but fast alternative to highly accurate but slow analog simulations of digital circuits. It relies on gate delay models, which allow the determination of input-to-output delays of a gate on a per-transition basis. Accurate delay models not only consider the effect of preceding output transitions here but also delay variations induced by multi-input switching (MIS) effects in the case of multi-input gates. Starting out from a first-order hybrid delay model for CMOS two-input NOR gates, we develop a hybrid delay model for Muller C gates and show how to augment these models and their analytic delay formulas by a first-order interconnect. Moreover, we conduct a systematic evaluation of the resulting modeling accuracy: Using SPICE simulations, we quantify the MIS effects on the gate delays under various wire lengths, load capacitances, and input strengths for two different CMOS technologies, comparing these results to the predictions of appropriately parameterized versions of our new gate delay models. Overall, our experimental results reveal that they capture all MIS effects with a surprisingly good accuracy despite being first-order only.

cs.AR↗

arXiv2024

A Framework for Streaming Event-Log Prediction in Business Processes

We present a Python-based framework for event-log prediction in streaming mode, enabling predictions while data is being generated by a business process. The framework allows for easy integration of streaming algorithms, including language models like n-grams and LSTMs, and for combining these predictors using ensemble methods. Using our framework, we conducted experiments on various well-known process-mining data sets and compared classical batch with streaming mode. Though, in batch mode, LSTMs generally achieve the best performance, there is often an n-gram whose accuracy comes very close. Combining basic models in ensemble methods can even outperform LSTMs. The value of basic models with respect to LSTMs becomes even more apparent in streaming mode, where LSTMs generally lack accuracy in the early stages of a prediction run, while basic methods make sensible predictions immediately.

cs.AI↗

arXiv2024

Majority consensus thresholds in competitive Lotka--Volterra populations

One of the key challenges in synthetic biology is devising robust signaling primitives for engineered microbial consortia. In such systems, a fundamental signal amplification problem is the majority consensus problem: given a system with two input species with initial difference of $Δ$ in population sizes, what is the probability that the system reaches a state in which only the initial majority species is present? In this work, we consider a discrete and stochastic version of competitive Lotka--Volterra dynamics, a standard model of microbial community dynamics. We identify new threshold properties for majority consensus under different types of interference competition: - We show that under so-called self-destructive interference competition between the two input species, majority consensus can be reached with high probability if the initial difference satisfies $Δ\in Ω(\log^2 n)$, where $n$ is the initial population size. This gives an exponential improvement compared to the previously known bound of $Ω(\sqrt{n \log n})$ by Cho et al. [Distributed Computing, 2021] given for a special case of the competitive Lotka--Volterra model. In contrast, we show that an initial gap of $Δ\in Ω(\sqrt{\log n})$ is necessary. - On the other hand, we prove that under non-self-destructive interference competition, an initial gap of $Ω(\sqrt{n})$ is necessary to succeed with high probability and that a $Ω(\sqrt{n \log n})$ gap is sufficient. This shows a strong qualitative gap between the performance of self-destructive and non-self-destructive interference competition. Moreover, we show that if in addition the populations exhibit interference competition between the individuals of the same species, then majority consensus cannot always be solved with high probability, no matter what the difference in the initial population counts.

cs.DC↗

arXiv2024

Faithful Dynamic Timing Analysis of Digital Circuits Using Continuous Thresholded Mode-Switched ODEs

Thresholded hybrid systems are restricted dynamical systems, where the current mode, and hence the ODE system describing its behavior, is solely determined by externally supplied digital input signals and where the only output signals are digital ones generated by comparing an internal state variable to a threshold value. An attractive feature of such systems is easy composition, which is facilitated by their purely digital interface. A particularly promising application domain of thresholded hybrid systems is digital integrated circuits: Modern digital circuit design considers them as a composition of Millions and even Billions of elementary logic gates, like inverters, GOR and Gand. Since every such logic gate is eventually implemented as an electronic circuit, however, which exhibits a behavior that is governed by some ODE system, thresholded hybrid systems are ideally suited for making the transition from the analog to the digital world rigorous. In this paper, we prove that the mapping from digital input signals to digital output signals is continuous for a large class of thresholded hybrid systems. Moreover, we show that, under some mild conditions regarding causality, this continuity also continues to hold for arbitrary compositions, which in turn guarantees that the composition faithfully captures the analog reality. By applying our generic results to some recently developed thresholded hybrid gate models, both for single-input single-output gates like inverters and for a two-input CMOS NOR gate, we show that they are continuous. Moreover, we provide a novel thresholded hybrid model for the two-input NOR gate, which is not only continuous but also, unlike the existing one, faithfully models all multi-input switching effects.

eess.SY↗

arXiv2023

PALS: Distributed Gradient Clocking on Chip

Consider an arbitrary network of communicating modules on a chip, each requiring a local signal telling it when to execute a computational step. There are three common solutions to generating such a local clock signal: (i) by deriving it from a single, central clock source, (ii) by local, free-running oscillators, or (iii) by handshaking between neighboring modules. Conceptually, each of these solutions is the result of a perceived dichotomy in which (sub)systems are either clocked or asynchronous. We present a solution and its implementation that lies between these extremes. Based on a distributed gradient clock synchronization algorithm, we show a novel design providing modules with local clocks, the frequency bounds of which are almost as good as those of free-running oscillators, yet neighboring modules are guaranteed to have a phase offset substantially smaller than one clock cycle. Concretely, parameters obtained from a 15nm ASIC simulation running at 2GHz yield mathematical worst-case bounds of 20ps on the phase offset for a $32 \times 32$ node grid network.

cs.AR↗

arXiv2023

On the Susceptibility of QDI Circuits to Transient Faults

By design, quasi delay-insensitive (QDI) circuits exhibit higher resilience against timing variations as compared to their synchronous counterparts. Since computation in QDI circuits is event-based rather than clock-triggered, spurious events due to transient faults such as radiation-induced glitches, a priori are of higher concern in QDI circuits. In this work we propose a formal framework with the goal to gain a deeper understanding on how susceptible QDI circuits are to transient faults. We introduce a worst-case model for transients in circuits. We then prove an equivalence of faults within this framework and use this result to provably exhaustively check QDI circuits, a linear Muller pipeline and a cyclic Muller pipeline, for their susceptibility to produce non-stable output signals.

cs.AR↗

arXiv2023

Continuity of Thresholded Mode-Switched ODEs and Digital Circuit Delay Models

Thresholded mode-switched ODEs are restricted dynamical systems that switch ODEs depending on digital input signals only, and produce a digital output signal by thresholding some internal signal. Such systems arise in recent digital circuit delay models, where the analog signals within a gate are governed by ODEs that change depending on the digital inputs. We prove the continuity of the mapping from digital input signals to digital output signals for a large class of thresholded mode-switched ODEs. This continuity property is known to be instrumental for ensuring the faithfulness of the model w.r.t. propagating short pulses. We apply our result to several instances of such digital delay models, thereby proving them to be faithful.

eess.SY↗

arXiv2021

A Faithful Binary Circuit Model with Adversarial Noise

Accurate delay models are important for static and dynamic timing analysis of digital circuits, and mandatory for formal verification. However, Függer et al. [IEEE TC 2016] proved that pure and inertial delays, which are employed for dynamic timing analysis in state-of-the-art tools like ModelSim, NC-Sim and VCS, do not yield faithful digital circuit models. Involution delays, which are based on delay functions that are mathematical involutions depending on the previous-output-to-input time offset, were introduced by Függer et al. [DATE'15] as a faithful alternative (that can easily be used with existing tools). Although involution delays were shown to predict real signal traces reasonably accurately, any model with a deterministic delay function is naturally limited in its modeling power. In this paper, we thus extend the involution model, by adding non-deterministic delay variations (random or even adversarial), and prove analytically that faithfulness is not impaired by this generalization. Albeit the amount of non-determinism must be considerably restricted to ensure this property, the result is surprising: the involution model differs from non-faithful models mainly in handling fast glitch trains, where small delay shifts have large effects. This originally suggested that adding even small variations should break the faithfulness of the model, which turned out not to be the case. Moreover, the results of our simulations also confirm that this generalized involution model has larger modeling power and, hence, applicability.

cs.OH↗

arXiv2021

A Composable Glitch-Aware Delay Model

We introduce the Composable Involution Delay Model (CIDM) for fast and accurate digital simulation. It is based on the Involution Delay Model (IDM) [Függer et al., IEEE TCAD 2020], which has been shown to be the only existing candidate for faithful glitch propagation known so far. In its present form, however, it has shortcomings that limit its practical applicability and utility. First, IDM delay predictions are conceptually based on discretizing the analog signal waveforms using specific matching input and output discretization threshold voltages. Unfortunately, they are difficult to determine and typically different for interconnected gates. Second, metastability and high-frequency oscillations in a real circuit could be invisible in the IDM signal predictions. Our CIDM reduces the characterization effort by allowing independent discretization thresholds, improves composability and increases the modeling power by exposing canceled pulse trains at the gate interconnect. We formally show that, despite these improvements, the CIDM still retains the IDM's faithfulness, which is a consequence of the mathematical properties of involution delay functions.

cs.OH↗

arXiv2020

Synchronizer-Free Digital Link Controller

This work presents a producer-consumer link between two independent clock domains. The link allows for metastability-free, low-latency, high-throughput communication by slight adjustments to the clock frequencies of the producer and consumer domains steered by a controller circuit. Any such controller cannot deterministically avoid, detect, nor resolve metastability. Typically, this is addressed by synchronizers, incurring a larger dead time in the control loop. We follow the approach of Friedrichs et al. (TC 2018) who proposed metastability-containing circuits. The result is a simple control circuit that may become metastable, yet deterministically avoids buffer underrun or overflow. More specifically, the controller output may become metastable, but this may only affect oscillator speeds within specific bounds. In contrast, communication is guaranteed to remain metastability-free. We formally prove correctness of the producer-consumer link and a possible implementation that has only small overhead. With SPICE simulations of the proposed implementation we further substantiate our claims. The simulation uses 65nm process running at roughly 2GHz.

cs.AR↗

arXiv2020

Synthesis in Presence of Dynamic Links

The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm's correct behavior. Previous work has focused on static networks with an a priori fixed message size. This approach has two shortcomings: Recent work in distributed computing is shifting towards dynamically changing communication networks rather than static ones, and an important class of distributed algorithms are so-called full-information protocols, where nodes piggy-pack previously received messages onto current messages. In this work, we consider the synthesis problem for a system of two nodes communicating in rounds over a dynamic link whose message size is not bounded. Given a network model, i.e., a set of link directions, in each round of the execution, the adversary choses a link from the network model, restricted only by the specification, and delivers messages according to the current link's directions. Motivated by communication buses with direct acknowledge mechanisms, we further assume that nodes are aware of which messages have been delivered. We show that the synthesis problem is decidable for a network model if and only if it does not contain the empty link that dismisses both nodes' messages.

cs.FL↗

arXiv2020

Distributed Computation with Continual Population Growth

Computing with synthetically engineered bacteria is a vibrant and active field with numerous applications in bio-production, bio-sensing, and medicine. Motivated by the lack of robustness and by resource limitation inside single cells, distributed approaches with communication among bacteria have recently gained in interest. In this paper, we focus on the problem of population growth happening concurrently, and possibly interfering, with the desired bio-computation. Specifically, we present a fast protocol in systems with continuous population growth for the majority consensus problem and prove that it correctly identifies the initial majority among two inputs with high probability if the initial difference is $Ω(\sqrt{n\log n})$ where $n$ is the total initial population. We also present a fast protocol that correctly computes the NAND of two inputs with high probability. We demonstrate that combining the NAND gate protocol with the continuous-growth majority consensus protocol, using the latter as an amplifier, it is possible to implement circuits computing arbitrary Boolean functions.

math.PR↗