Papers

Continual knowledge graph embedding updates entity and relation representations as a graph grows. Existing methods primarily address catastrophic forgetting, but entity admission also changes the candidate universe of every compatible query. A historical answer can therefore lose rank even when its score and its ordering among old entities are preserved. We formalize this effect as candidate-set interference and introduce Matched Excess-Outranker Regularization (MEOR), a host-level objective that compares smooth answer-relative newcomer pressure with score-blind, structurally matched old references. Its one-sided penalty acts only when newcomer competition exceeds the matched reference, preserving the host learner's signal for legitimate new entities. Across eight paired runs on ENTITY-ComplEx, MEOR improves historical current-universe mean reciprocal rank (MRR) by 0.0057 over replay and reduces candidate-set interference by 0.0055, with one-sided 95% lower bounds of 0.0052 and 0.0051, respectively. It satisfies the preservation criteria for old-universe ranking and newcomer acquisition and improves historical current-universe MRR over persistent calibration, matched maximum regularizer (MMR), and unmatched old regularizer (UOR). Direct ablations support each component of its reference construction and aggregation. Adding MEOR also improves historical ranking in all ten reported FBInc-S and FBInc-L host and backbone settings, with every paired 95% confidence interval excluding zero. These results establish candidate admission as a distinct source of continual rank loss and show that it can be controlled without replacing the underlying embedding architecture or continual learner.

Synchronization errors, including insertions, deletions, and substitutions, may occur in bursts in communication systems such as DNA data storage, file synchronization, and magnetic recording. In this paper, we study an error model con?sisting of one burst of t-deletions and one burst of t-substitutions. By reformulating the original sequence into a matrix form, we propose an explicit construction of error-correcting codes capable of correcting one burst of t-deletions and one burst of t-substitutions with O(log n) redundancy.

Large Language Model-based multi-agent systems are increasingly explored for software engineering tasks, but they remain difficult to inspect, debug, and evaluate under controlled failures. We present llmmas-otel, a lightweight and framework-agnostic tool that combines OpenTelemetry-based distributed tracing with fault injection for LLM-based multi-agent systems in software engineering workflows. The tool instruments agent executions with trace-aligned telemetry across workflow phases, agent steps, inter-agent communication, tool calls, and LLM invocations, and supports targeted fault injection at selected interaction points. This makes it possible to compare baseline and faulty executions in a reproducible way and inspect the effects through aligned traces and run artifacts. We describe the motivation, architecture, implementation, current capabilities, and initial validation of the tool on a minimal demo workflow and a real LLM-based multi-agent system for software development.

Taint analysis is a fundamental technique for detecting sensitive data leaks in Android apps. However, traditional static tools, such as FlowDroid, still face well-known challenges due to the complexity of accurately modeling the Android framework. In this paper, we investigate whether off-the-shelf Large Language Models (LLMs) can effectively reason about taint flows in Android apps. Our preliminary approach relies on an agentic interaction strategy, enabling the LLM to iteratively explore code and reason about data flows. We conduct an initial evaluation on the DroidBench benchmark against FlowDroid, where our approach outperforms the baseline: Gemini-3 Flash achieves an F1-score of 0.96, compared to 0.55 for FlowDroid. In particular, we observe improvements in challenging categories such as inter-component communication (0.95 vs. 0.17), implicit flows (0.94 vs. 0.00), and reflection (1.00 vs. 0.50), where FlowDroid typically struggles. On a small set of real-world apps, the LLM-based approach also identifies additional potential data leaks not reported by FlowDroid. These preliminary findings suggest that LLM reasoning may effectively complement traditional static taint analysis, motivating future research on hybrid LLM-enhanced taint analysis pipelines.

This paper proposes methods to extract over 50 types of events from a Dutch historical corpus spanning the 17th and 18th centuries. The methods we propose aim to tackle a very challenging scenario in Machine Learning: extracting the long-tail of the long-tail. Historic data from before the 19th century is in itself a niche domain not covered in the pre-training of Large Language Models, and we aim to extract events only scarcely annotated in the training data available for this domain. We propose creating expert classifiers for subgroups of the events present in the training data. We make these groupings based on similar frequency in the training data or on semantic relatedness. Experts trained on underrepresented events are assigned higher priority when predicting to avoid being dominated by frequency biases. We refer to this new way of combining classifiers, specifically tailored to protect the long-tail, as ROBE: Reversed-Order-Biased-Experts. We also propose a controlled method to create domain-specific synthetic data. Our two implementations of ROBE outperform a simple fine-tuned encoder model with a .16 increase in precision and a .05 increase in recall respectively. The best model achieves a .11 increase in f1 for a group of long-tail classes in our niche data set.

Neural network training has an oracle problem: a run can converge normally and yield a usable model while the software beneath it computes something other than specified. Almost all such work runs on one stack, so there is rarely anything independent to check against. We study whether independently implemented training stacks can serve as differential oracles for a whole fine-tuning pipeline, rather than the operators and inference paths that prior differential testing targets. We define a trajectory-level protocol – a shared specification, cross-check points spanning arithmetic, model loading, data rendering and the learning trajectory, and a separation of independence of the stack, the orchestration and the language runtime – and apply it to a LoRA adaptation of Qwen3-0.6B over 168,574 clinical question-answer pairs under PyTorch and under numbat, an independent framework written in Zig, driven natively and through its C interface from six languages. Across 42 paired evaluations spanning a full epoch the two stacks' held-out cross-entropy differs by 0.134% on average, and four implementations end the epoch within 0.15% of one another. The comparison exposed 17 faults that single-implementation development had missed, two of them notable for software engineering. The fault with the largest effect on the trained model lay outside the numerical kernels: a mismatch in how clinical text was rendered moved held-out loss 0.15, some 500 times more than the arithmetic faults found beside it. And four faults were reachable only from a language whose memory model differs from the first two implementations: a scheduler migrating work across threads, a collector blind to device memory, an ownership discipline needing a primitive the interface lacked. Implementation diversity has several axes, and the runtime is one.

Data assimilation (DA) and inverse modelling are indispensable tools for combining physics-based models with observations, yet the software that implements them is often fragmented: sequential (Kalman and particle) filters and variational (3D/4D-Var) estimators are typically developed as separate codebases, each tied to a specific class of forward model - for example, simple time-marching schemes for ordinary differential equations (ODEs), or full finite element (FE) discretisations of partial differential equations (PDEs). In this work, we present Opal.jl, a Julia package that overcomes this fragmentation by providing a unified environment for a wide range of DA methods and forward model backends, all accessible behind a single high-level interface. Starting from a handful of basic methods, complex inference tools can be built by composing them with advanced capabilities, such as covariance localisation/inflation, online noise covariance estimation, bias-aware correction, and kriging-based calibration of reduced-order surrogates. The package integrates natively with the SciML ecosystem for ODE-governed systems, and with Gridap/GridapROMs for both full-order and reduced-order discretisations of PDEs. Notably, the API is designed to allow a reduced-order surrogate to replace a full-order solver with no change to the code, even at the driver level. We demonstrate the library on a Lorenz-63 benchmark, on a Van der Pol oscillator problem with biased observations, on a turbulent Navier-Stokes flow past a square cavity, where the unknown Reynolds number is inferred from sparse velocity and pressure measurements, and finally on a heat equation using a reduced-order surrogate instead of a more standard full-order model.

Change data synthesis provides a cost-effective solution for expanding training data and improving the performance of change detection models. However, existing synthesis methods typically rely on handcrafted rules to simulate changes, where limited coverage of class transitions restricts the diversity of synthesized data, while predefined transition designs limit their flexibility in accommodating varied change types. In this work, we introduce KnowChange, a knowledge-guided change data synthesis framework that leverages pretrained vision-language models as knowledge sources to reason about plausible change locations and class transitions from pre-change scenes and desired change types. By integrating knowledge-guided change simulation with generalizable synthesis models, KnowChange enables flexible synthesis of diverse change types within a unified framework. Extensive experiments demonstrate that KnowChange-generated data consistently outperforms existing synthetic datasets in both synthetic-to-real transfer and synthetic data augmentation, despite being generated at a compact scale. Further analyses show that the knowledge-guided change simulation can be seamlessly integrated into existing synthesis pipelines and enhance the downstream utility of synthesized data.

We define weighted alternating tree automata — a generalization of weighted (non-alternating) tree automata, (unweighted) alternating tree automata, and weighted alternating (string) automata — over commutative semirings. We study their expressive power, and show that it is equivalent to that of weighted tree automata exactly when the employed semiring is locally finite. In our main result, we characterize the class of weighted tree languages defined by weighted alternating tree automata as the closure of the recognizable weighted tree languages under inverse tree homomorphisms.

Motivated by the study of closure operations on picture languages, we ask when a set of unary tiles can generate all sufficiently large pictures either via repeated horizontal and vertical concatenations or via tiling operations. In one dimension, the lengths of words in the concatenation closure of a unary language form an additive subsemigroup of positive natural numbers; hence, they are finitely generated. Cofiniteness is characterized by the gcd of these generators being one. Since ordinary cofiniteness in two dimensions is too restrictive and essentially reduces to degenerate one-dimensional conditions on strips, we introduce and study asymptotic cofiniteness: all sufficiently large rectangular pictures are generated. A direct extension of the one-dimensional criterion, requiring the gcd of the tile heights and of the tile widths to be one, is not sufficient, because local congruence obstructions may persist in two dimensions. We give an exact arithmetic characterization of asymptotic cofiniteness for arbitrary, possibly infinite, sets of unary rectangular tiles. The characterization is the same for the guillotine closure, obtained by horizontal and vertical concatenation, and for the full tiling closure. For finite tile sets, the proof combines semigroup arguments and an explicit least-common-multiple stacking construction for sufficiency, while necessity is obtained by a roots-of-unity argument applying also to nonsliceable tilings. The extension to infinite tile sets follows from the finite-basis theorem for Klarner systems.

A turn or reversal in a computation of a pushdown automaton is a switch from a phase in which the height of the pushdown store increases to a phase in which it decreases. Given a pushdown automaton, we first consider, for each string in its language, the minimum number of turns made in accepting computations (weak measure). We prove that it is decidable whether a pushdown automaton accepts a bounded language in a constant number of turns and whether it accepts a bounded language in k turns, for any given k>=0. This is in contrast to the general case, in which these problems are known to be undecidable, with the exception of acceptance in 0 turns, which is decidable. Furthermore, we prove that when the number of turns sufficient to accept a bounded language is not limited by any constants, it linearly grows with respect to the input length. Also this is in contrast with the general case where, for each nonnegative k, there exists a language for which the number of turns necessary and sufficient is of the order of log^(k), the k times composition of the logarithm with itself. We also prove that, when the costs of all accepting computations are taken into account (accept measure), a linear lower bound for the number of turns, if not limited by any constants, holds even removing the restriction to bounded languages.

AI systems are increasingly evaluated for legally accountable settings, where correct outputs must also be justifiable against an applicable legal standard. Existing legal-AI benchmarks and LLM-as-judge protocols provide important infrastructure for measuring task performance and open-ended response quality. We contribute one additional evaluation signal: a dual-judge protocol that pairs a standard 0-10 quality judge with a strict binary semantic-equivalence judge against a human-curated reference. We study a controlled, visually grounded regulatory task - UK traffic-sign interpretation, whose meaning is a codified question with a known reference for every input - and measure not merely whether the two judges disagree (by construction they must) but how much and where. On 4,680 evaluations under seven visibility levels and two occlusion modes, the two judges are moderately associated (point-biserial r = 0.644), while revealing an asymmetric Type II pattern affecting 8.0% of all evaluations. Its distribution is instructive: the marginal rate peaks at high visibility (14.2% at v = 0.8) simply because high-scoring answers are common there, but conditioned on the answer already scoring above 7, the rate is highest under heavy occlusion (54-63% at v <= 0.3), so a high quality score is least trustworthy when the input is most degraded. We are explicit that the signal is a property of this judge and reference: a 49-row human check shows the 0-10 judge aligns closely with everyday-reader judgement (Pearson r = 0.81; r = 0.80 with the LLM accuracy sub-score), while the equivalence judge is fairly but one-directionally stricter. The protocol adds one LLM call per evaluation and surfaces a signal single-judge protocols do not report. We release the prompt template, occluded variants, and full evaluation results.

The Post Correspondence Problem is as follows: having a set of dominoes, is there any (maybe repeating) sequence of them such that the words formed by the upper parts and the lower parts by the sequence of dominoes are identical. It is one of the most known problems that is algorithmically undecidable. In this paper, the reverse Post Correspondence Problem is defined, that is, where the two assembled words of the dominos are reversals of each other. Undecidability about this new, modified problem is proven. Further, based on this result, it is also proven that the emptiness problem for 5'->3' String Assembly Systems is undecidable too. 5'->3' String Assembly Systems belong to String Assembly Systems type formal language generating models. The 5'->3' denotes that, in these variants, the derivations of the generated words start from the two extremes. The notation and the new model are bio-motivated as any double stranded DNA has two opposite oriented 5'->3' strands.

CSFLOC is a non-CDCL SAT decision procedure based on counting subsumed full-length ordered clauses. The classical CSFLOC loop traverses the ordered space of full-length clauses by a monotone counter: if the current full-length clause is not subsumed by the input formula, its negation is a satisfying assignment; otherwise, a subsuming clause determines a counter jump. The main bottleneck is the repeated search for such a subsuming clause. This paper presents CSFLOC-WL, and its current implementation CSFLOC-WL3, in which this search is replaced by watched-literal prefix propagation over the negation of the current full-length clause represented by the counter. The central mechanism is early conflict detection: if propagation under a common prefix derives opposite unit consequences for the same variable, then the two reason clauses are resolved immediately and the resolvent is used as a new counter-jump cause. The resulting solver is not a CDCL solver: it has no CDCL decision tree, no restart policy, and no first-UIP backjumping loop. It remains a counter-guided full-length-clause-counting solver, but it imports the watched-literal data structure and reason clauses as engineering tools for discovering jumps. Experiments on selected UNSAT SATLIB instances compare CSFLOC-WL3 with CSFLOC21TU and CaDiCaL 3.0.0. The results are mixed: CSFLOC-WL3 is strong on several random 3-SAT instances near the random-3-SAT satisfiability threshold, whereas CSFLOC21TU remains faster on several structured cases, apparently because it contains a more mature cache mechanism that is not yet present in CSFLOC-WL3.

We consider the independent language property defined by the language equation φ(X)=\emptyset, where the expression φ involves the language variable X, constant languages, and standard regular operations including transductions, but not complementation. This property consists of all languages L satisfying φ(L)=\emptyset. Depending on the choice of the operations in φ, the equation defines a broad class of codes, including combinations of standard variable-length codes and error-detecting codes. We show that any φ-independence is a Jürgensen independence, we define what a witness of non-satisfaction of φ(X)=\emptyset is, for a language L, and we show how to compute a witness of non-satisfaction when L is regular. We also discuss the complexity of the problem, showing that the decision version of the problem is PSPACE-complete.

LLM agents can generate paper reproduction code, yet often produce scientifically unfaithful implementations. We define this failure mode as semantic drift, where generated code silently diverges from the paper's specifications. We introduce SemanticAlign-Bench(SA-Bench), a diagnostic benchmark covering 30 papers from ICLR, ICML and NeurIPS 2025. For each paper, we decompose its specifications into atomic and verifiable implementation claims, which we call Semantic Alignment Units (SAUs) and evaluate repositories along four diagnostic dimensions spanning numerical, methodological, protocol and ordering drift. In total, we construct 1,491 SAUs across five ML domains and evaluate 12 generator configurations (4 models $\times$ 3 scaffolds). Even the strongest configuration (Claude+PaperCoder) achieves a mean SAU score of only 0.301 out of 1.0, with an overall mean of 0.221 across 360 evaluations. A failure taxonomy reveals that agents attempt most requirements but implement them incorrectly, with implementation mismatch and stubs accounting for the majority of zero-scored claims. Our analysis further indicates that scaffolds optimized for executability provide limited leverage for scientific reproduction; narrowing the gap requires scaffolds that prioritize semantic specification verification. The benchmark, annotations and evaluation pipeline are publicly available.

Reversible computing is a novel paradigm that has recently emerged and extends traditional forwards-only computation with the capability to execute in the reverse direction, making it possible for computation to run backwards as well as forwards. Event structures are a foundational model in concurrency theory, providing a way to understand computational processes by describing the events that occur and the relationships between them. In the literature, two structurally different approaches to associating transition system semantics with event structure models have been distinguished. One approach is based on configurations, which are sets of already executed events. The other approach is based on model residuals, which are not yet executed fragments of the model. Configuration-based transition systems appear to be primarily used for semantic representations. Residual-based transition systems are actively applied to demonstrate the consistency between operational and denotational semantics of concurrent process calculi, as well as to visualize the dynamics of models. The present paper focuses on bundle event structures with causal reversibility, which are used in the study of reversible extensions of CCS- and π-like systems. Mappings from the reversible event structure model to the two transition system semantics are developed, which made it possible to prove the isomorphism of the semantics. A category-theoretic characterization of the mappings is provided.

Several experience reports illustrate that mutation testing is capable of supporting a shift-left testing strategy, especially in industries where late bug discovery incurs very high costs and risks. In the context of cyber-physical systems, a shift left implies that engineers need to test the design models used to simulate, prototype, and analyse the feasibility of the system under design. In this paper, we analyse the challenges we encountered and the lessons we learned when incorporating mutation testing in the context of DUCO, a company producing ventilation systems for buildings. The engineers within DUCO have years of experience with model-based engineering centered around Simulink and StateFlow, including unit tests for their models. During a pilot project with our tool prototype MUT4SLX we learned that equivalent mutants, requirement traceability, and mutation testing for Stateflow represent particular challenges not yet reported in the academic literature.

The study of word-representability was initiated by the seminal work of Kitaev and Pyatkin in 2008 that has later led to the monograph by Kitaev and Lozin in 2015. In this paper, we build on the very recent work by Fernau et al. who proposed a general framework that generalizes certain aspects of word-representability, so that any binary language describes a graph class. In this work, we systematically study particularly small languages and observe that they characterize well-known graph classes, e.g., interval, permutation, circle, and bipartite chain graphs. Thus, we strengthen the bond between formal languages and graph classes, even for small binary languages. We also show some limitations of our approach by proving that, e.g., families of sparse graphs like planar graphs cannot be characterized by any language following this approach.

We consider the generating power of the initial algebra semantics of weighted tree automata over strong bimonoids (hence also over semirings) and the question under which conditions the weighted tree automata can produce only finitely many values. We show that there exists a right-distributive strong bimonoid which is bi-locally finite but not locally finite. We also show that if the ranked alphabet contains a symbol with rank at least two, then for any finitely generated strong bimonoid, weighted tree automata can generate, via their initial algebra semantics, all elements of the strong bimonoid. As a consequence of these results, for bi-locally finite right-distributive strong bimonoids which are not locally finite, weighted tree automata can generate infinitely many values, provided that the input ranked alphabet contains a symbol with rank at least two. This is in sharp contrast to the setting of weighted string automata, which can generate only finitely many values. As a further consequence, for any finitely generated semiring, there exists a weighted tree automaton which generates, via its run semantics, all elements of the semiring.

Bandwidth restricts how far transitions can move under an ordering of the states in an automaton. While every finite language admits a bandwidth-2 NFA representation, the deterministic setting is substantially more restrictive. We investigate the bandwidth of partial DFAs accepting finite languages. We show that bounded bandwidth imposes strong structural restrictions on deterministic representations. We prove that there is an infinite hierarchy of classes of finite languages defined by deterministic bandwidth. As a special case of interest, we consider finite languages accepted by bandwidth-1 partial DFAs, and show that they admit a positional characterization, which yields a polynomial-time decision algorithm. We further study how the minimum DFA bandwidth can be estimated from the structure of the minimal DFA. We derive computable upper and lower bounds based on position-unfolding, and local growth of reachable residual states. These bounds can be computed efficiently and differ by at most a linear factor in the maximum word length. We also present a simple language family where the bounds match exactly.

We survey selected open problems in the theory of synchronizing automata, centered around the famous Černý conjecture. A deterministic finite automaton is called synchronizing if it admits a reset word whose action maps all states to a single state. The Černý conjecture states that every synchronizing automaton with n states possesses a reset word of length at most (n-1)^2. We discuss avoiding words, compressing a state with another, synchronization of a (given or any) subset, complexity of deciding the synchronizability, average reset threshold, and linear-algebraic methods. Some new auxiliary results are also presented.

We provide a survey of several families of subregular expressions obtained by modifying the classical operator set consisting of union, concatenation, and Kleene star. More specifically, we consider expression systems based on sets of two or three operations chosen from union, intersection, complementation, concatenation, and Kleene star. The resulting language families range from finite languages to the full class of regular languages. We collect and organize known results on the expressive power and structural properties of these families. We compare the resulting language classes over unary and arbitrary alphabets and summarize known inclusion, equality, and incomparability results. The aim of this survey is to provide a unified view of the language families induced by restricted operator sets and to highlight open relations and possible directions for further research.

Currently available commercial vision-based tactile sensors provide rich contact information but remain vulnerable to abrasion and repeated concentrated loading, limiting their use in demanding robotic applications. This work presents a durable tactile fingertip comprising a soft silicone gel with a nonpigmented, textured, thin thermoplastic-polyurethane protective film and a replaceable sensing cartridge. Durability was evaluated using two accelerated laboratory procedures: a rotating-drum sanding test and a repetitive probe test applying 39.2 N (4.0 kgf) at 45 cycles per minute. Under the defined sanding conditions, the developed sensor reached the protective-film rupture endpoint after approximately 2-3 hours. During repetitive probe testing, all nine developed sensors remained functionally usable when testing was discontinued: seven after 5 days, one after 6 days, and one after 8 days. Commercial GelSight Mini and DIGIT specimens exhibited initial surface-film rupture after approximately 24-30 seconds of sanding and 25-35 minutes of repetitive loading. Damage to the developed sensor progressed gradually and produced little interference with tactile imaging at the test endpoints. These observations establish durability improvements of more than two orders of magnitude under the defined accelerated conditions. Combining increased durability, gradual degradation, and rapid cartridge replacement offers a practical approach to maintainable vision-based tactile sensing for demanding robotic applications.

Reproducibility of heart rate variability (HRV) analysis is limited by differences in preprocessing and computational conventions across software platforms. We developed HRV Studio, an open-source PyQt6-based desktop application integrating transparent HRV analysis with automated quality-control (QC) diagnostics. Validation included large-scale agreement with NeuroKit2, targeted Kubios benchmarking, spectral-method comparison, synthetic perturbation testing, recording-duration sensitivity analysis, and arrhythmia-focused QC stress testing. HRV Studio showed near-identical agreement for the widely used time-domain indices RMSSD and SDNN under matched conditions. In the primary five-minute NeuroKit2 comparison, frequency-domain median relative errors were 1.35% for LF, 0.18% for HF, and 1.41% for LF/HF, while VLF remained more convention-sensitive (37.79%). Nonlinear Poincaré indices also demonstrated high consistency. Sequence-harmonized Kubios benchmarking confirmed near-identical agreement for time-domain and nonlinear indices and strong agreement for most frequency-domain measures. Extended ten-minute analyses reproduced the same overall pattern with lower disagreement for some convention-sensitive spectral outputs. Synthetic and arrhythmia stress tests maintained 100% numerical stability while consistently triggering QC warnings. Overall, HRV Studio provides a transparent and reproducible platform for HRV research, with strong cross-platform consistency when NN sequences, preprocessing, and analytical conventions are harmonized. Stress-test results indicate computational robustness rather than clinical validation.

Inductive inference of one- and two-way cellular automata (CA) is considered. This involves inferring a CA that is compatible with a finite amount of available data. In this paper, this information is provided in the form of a finite set of intervals, where each interval consists of two words w and w' over a state set alphabet, with a positive integer i. The goal is to infer a CA which is compatible with each interval (w,w',i), meaning that it can derive w' from w in i steps. We consider three variations of this problem, 1) where the CA is completely known a priori, and the goal is therefore to verify compatibility, 2) where the CA is partially known a priori and the goal is to extend it to a full CA that is compatible, and 3) where the CA is completely unknown, and the goal is to fully construct one that is compatible if one exists. With all three variations, inference can be completed in polynomial time, and is in fact P-complete.

We prove three theorems on the flow monoids of finite graphs. First, we show that a non-empty finite graph G = (V, E) is connected if and only if its flow monoid contains a constant map on V, equivalently, if and only if it contains all constant maps on V. Second, we give a new characterization of graph minors in terms of division of flow transformation monoids, together with an algebraic crossing condition that detects edges between the vertex sets being contracted. Third, we strengthen this to an embedded-copy theorem: a graph M is a minor of G if and only if, subject to analogous crossing conditions, the flow transformation monoid of M is realized as the induced action of a subsemigroup of the ambient flow monoid of G, this subsemigroup being a monoid with a local idempotent identity.

If L is a unary language, then its binary coded version bin(L) is a binary language containing all binary strings representing any 0^x in L. It is known that if a unary language L is regular and can be recognized by a minimal one-way deterministic finite automaton (1DFA) with n states, then its binary coded version is also regular and can be recognized by a 1DFA with at most n states, but at least 1+log(n) states. Here we shall present related results for two-way automata (2DFAs). First, we shall show that each unary 2DFA A' with n states can be converted to a 2DFA A” recognizing bin(L(A')) with at most O(n.log n) states. If A' is minimal and uses only loops of odd lengths, A” will use at most 2n+2 states, but it must use at least n states. For each n>=7, we shall also present a unary witness language for which a minimal 2DFA uses exactly n states, but any minimal 2DFA recognizing its binary coded version uses at least n states, but less than n+log(n) states.

Longitudinal radiology report generation (LRRG) requires identifying both current findings and their changes relative to a prior study. Existing methods jointly model diagnosis, attribute estimation, temporal comparison, and language generation within implicit representations, which can cause task interference, obscure the evidence underlying each decision, and limit error traceability. They also model progression states as independent labels, ignoring their ordered structure and thus treating missed changes and direction reversals equally. We present STRIVE, Multi-Agent Structured Temporal Reasoning with Integrated Verification for LRRG, which decomposes clinical reasoning into specialized Diagnosis, Attribute, and Temporal Change Agents that produce explicit intermediate evidence. In particular, the Temporal Change Agent is further post-trained using Progression-Aware GRPO, a verifiable, shaped reward that assigns partial credit to direction-preserving errors while scoring direction reversals lowest. STRIVE performs verification at two stages: a deterministic Consistency Gate reconciles the agent outputs before report generation, and a Validation Agent checks whether the generated report is supported by the aggregated clinical evidence. On Longitudinal-MIMIC, STRIVE attains the best clinical efficacy among recent methods and more than doubles Longitudinal Change Concordance (LCC), a measure of temporal agreement with the reference report, over the strongest baseline.

Large Reasoning Models (LRMs) generate intermediate reasoning traces that may contain unsafe content, even when their final responses appear safe. Guardrail models are designed to detect and block unsafe content, yet existing benchmarks for unsafe content detection focus primarily on prompts and final responses, leaving reasoning traces largely unexamined. Moreover, these benchmarks typically provide only binary safety labels, without evidence annotations that justify the judgments. To address these limitations, we introduce TRACE, an evidence-grounded safety evaluation benchmark that covers the entire LRM inference pipeline: prompts, reasoning traces, and final responses. TRACE includes prompts in two languages spanning nine risk categories and ten attack strategies. For each prompt, four LRMs generate reasoning traces and final responses, and we annotate the safety of each component and extract supporting evidence from the corresponding source text. Evaluating 18 guardrail models on TRACE reveals that safety judgment for reasoning traces is substantially more challenging than for prompts or final responses, and that current models struggle to accurately extract supporting evidence. These findings highlight the need for guardrail models that can reliably detect and precisely localize unsafe content across the LRM inference pipeline.