arXiv subjects

Kazuki Watanabe

Publications and source records attributed to Kazuki Watanabe.

At least 19 recordsLinked to original sources

arXiv2026

Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking

Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a particularly important technique. However, there is a well-known scalability issue due to state-space explosion, especially when verifying complex properties. To mitigate this issue, we propose specification-guided path shortcutting for probabilistic systems, focusing on Markov chains (MCs) and $\omega$-regular properties. The key idea is that, when the verified property is fixed, certain sequences of transitions in an MC can be replaced with a single transition without changing the satisfaction probability, and thus, we can reduce the state space of the MC. We implement the proposed path shortcutting and evaluate its contribution to the performance of probabilistic model checking, using Storm as the baseline model checker. The results suggest that our approach often outperforms the baseline, particularly on benchmark instances with complex specifications.

cs.LO↗

arXiv2026

GLTCAM: Concept of Multi-color Millimeter and Submillimeter Camera for the Greenland Telescope

To investigate the formation history of large-scale structure through the dynamics of galaxy clusters, we are developing a multi-color millimeter and submillimeter-wave continuum camera (GLTCAM) for deployment on the Green-land Telescope (GLT). GLTCAM will observe in six frequency bands - three in the millimeter range (150, 220, and 270 GHz) and three in the submillimeter range (350, 400, and 670 GHz). The optical design provides a compact configuration that fits within the GLT receiver cabin, while delivering diffraction-limited performance over an $18'$ field of view with minimal telecentricity error and distortion. A key advantage of this design is its uniform illumination footprint at the cold stop, which helps minimize thermal loading on both the detectors and the cryogenic stages. The focal plane module comprises a quasi-optical bandpass filter, a conical horn array coupled with planar ortho mode transducers (OMTs), and a superconducting multi-color microwave kinetic inductance detector (MKID) array. Current development efforts are focused on the three-color millimeter-wave module. The detector array employs a single-layer coplanar waveguide (CPW) architecture, which simplifies fabrication and enables scalability to large-format arrays. GLTCAM aims for the early realization of next-generation wide-field, multi-color observations as a pathfinder for future large submillimeter telescopes.

astro-ph.IM↗

arXiv2026

Design Method of Quasi-Lumped Element Bandpass Filters Using Superconducting Coplanar Waveguide for Millimeter-Wave Multichroic Imaging

An on-chip band-defining filter coupled with a superconducting photon detector is a promising technology for developing multi-band imaging cameras at millimeter and submillimeter wavelengths. In this paper, we present the design of on-chip bandpass filters based on coplanar waveguide geometry, which can be easily integrated into large-format multi-band detector arrays. A lumped element filter design is suitable not only for achieving a compact footprint but also for suppressing harmonics to reduce band-to-band crosstalk in a multiplexer. However, the coplanar waveguide geometry and the photolithography process rule limit the maximum available inductance and capacitance of lumped elements, which does not sufficiently meet the requirements of filter circuits. To overcome this limitation, we have established a design method for quasi-lumped element filters, in which the maximum element size is relaxed to a quarter wavelength, exceeding the ideal lumped element size. We achieved design solutions for 150, 220, and 270 GHz 8th-order Chebyshev bandpass filters and a triplexer. We also report on the measurement results of a scaled model of the bandpass filter, demonstrating the validity of our proposed filter design.

astro-ph.IM↗

arXiv2026

Broadband anti-reflection coating for sub-terahertz optics using dielectric multilayers

Sub-terahertz astronomy requires instruments capable of simultaneous observations across multiple spectral bands, motivating the development of broadband anti-reflection coatings (ARCs). We investigated low-loss dielectrics with refractive indices suitable for multilayer ARCs on polyethylene optical elements and identified candidates that partially meet the requirements. To address the remaining gaps in available refractive indices, we applied dielectric multilayer synthesis by combining newly identified thin materials with controlled bonding to realize the required effective refractive indices. As a result, the fabricated 5-layer ARC achieved reflection losses of 0.2% (average) and 3.2% (maximum) over 130-710 GHz.

astro-ph.IM↗

arXiv2026

From Coalgebraic Determinization to Belief Construction for Partial Observability

The belief construction is a fundamental technique for transforming partially observable systems to fully observable ones while preserving the relevant semantics. It plays a central role in the analysis of partially observable systems, in particular partially observable Markov decision processes (POMDPs), which is a central model in artificial intelligence and formal verification. In this paper, we develop a coalgebraic framework for the belief construction. To handle observations categorically, we lift a monad to slice categories and introduce a belief decomposition that reorganizes states according to their observations. This allows us to introduce a coalgebraic generalization of the belief construction, obtained by combining the belief decomposition with the coalgebraic determinization of Silva, Bonchi, Bonsangue, and Rutten. In this framework, we show that the semantics of a partially observable system coincides with that of the corresponding belief coalgebra. We then study when the latter further agrees with the semantics of its fully observable counterpart, and use this to identify conditions under which the semantics of a partially observable system coincides with that of the corresponding fully observable belief system. As consequences, we recover the standard equivalence between POMDPs and belief MDPs, and obtain a new equivalence result for weighted transition systems with the semimodule monad.

cs.LO↗

arXiv2025

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs

We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational product construction -- from linear-time safety verification of effectful higher-order programs to computation of weakest pre-conditions of product programs. This reduction enables us to apply existing algorithms for such well-studied computations of weakest pre-conditions, some of which are available as off-the-shelf solvers. We show the correctness of our denotational product construction by proving a preservation theorem under strong monad morphisms and an existence of suitable liftings along a fibration. We instantiate our framework with both probabilistic and angelic nondeterministic higher-order programs, and implement an automated solver for the probabilistic case based on the existing solver developed by Kura and Unno. To the best of our knowledge, this is the first automated verifier for linear-time temporal verification of probabilistic higher-order programs with recursion.

cs.LO↗

arXiv2025

Initial Algebra Correspondence under Reachability Conditions

Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost surely reachable. In this paper, we present a unifying framework for such reachability conditions that ensures the correspondence of two different semantics. Our categorical framework naturally induces an abstract reachability condition via a suitable adjunction, which allows us to prove coincidences of fixed points, and more generally of initial algebras. We demonstrate the generality of our approach by instantiating several examples, including the almost surely reachability condition for MCs, and the unambiguity condition of automata. We further study a canonical construction of our instance for Markov decision processes by pointwise Kan extensions.

cs.LO↗

arXiv2025

Compositional Verification of Almost-Sure Büchi Objectives in MDPs

This paper studies the verification of almost-sure Büchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is a strategy that ensures that a Büchi objective is almost-surely satisfied. We first show that proper exit sets -- the sets of exits that can be reached within a component without losing locally -- together with the reachability of a Büchi state are a sufficient and necessary statistic for the compositional verification of almost-sure Büchi objectives. The number of proper exit sets may grow exponentially in the number of exits. We define two algorithms: (1) A straightforward bottom-up algorithm that computes this statistic in a recursive manner to obtain the verification result of the entire string diagram and (2) a polynomial-time iterative algorithm which avoids computing all proper exit sets by performing iterative strategy refinement.

cs.LO↗

arXiv2025

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure. Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.

cs.LO↗

arXiv2025

A No-go Theorem for Coalgebraic Product Construction

Verifying traces of systems is a central topic in formal verification. We study model checking of Markov chains (MCs) against temporal properties represented as (finite) automata. For instance, given an MC and a deterministic finite automaton (DFA), a simple but practically useful model checking problem asks for the probability of (terminating) traces accepted by the DFA, which can be computed via a product MC of the given MC and DFA and reduced to a simple reachability problem. Recently, Watanabe, Junges, Rot, and Hasuo proposed coalgebraic product constructions, a categorical framework that uniformly explains such coalgebraic constructions using distributive laws. This framework covers a range of instances, including the model checking of MCs against DFAs. In this paper, on top of their framework we first present a no-go theorem for product constructions, showing a case when we cannot do product constructions for model checking. Specifically, we show that there are no coalgebraic product MCs of MCs and nondeterministic finite automata for computing the probability of the accepting traces. The proof relies on a characterisation of natural transformations between certain functors that determine the type of branching, including nondeterministic or probabilistic branching. Second, we present a coalgebraic product construction of MCs and multiset finite automata (MFAs) as a new instance within our framework. This construction addresses a model checking problem that asks for the expected number of accepting runs on MFAs over traces of MCs. We show that this problem is solvable in polynomial time.

cs.LO↗

arXiv2025

On Piecewise Affine Reachability with Bellman Operators

We study the following reachability problem for piecewise affine maps: Given two vectors $\mathbf{s}, \mathbf{t} \in \mathbb{Q}^d$ and a piecewise affine map $f \colon \mathbb{Q}^d\rightarrow \mathbb{Q}^d$, does there exist $n\in \mathbb{N}$ such that $f^{n}(\mathbf{s}) = \mathbf{t}$? In this work, we focus on this reachability problem for a subclass of piecewise affine maps -- Bellman operators arising from Markov decision processes. We prove that the reachability problem for $\max$- and $\min$-Bellman operators is decidable in any dimension under either of the following conditions: (i) the target vector $\mathbf{t}$ is not the fixed point of the operator $f$; or (ii) the initial and target vectors $\mathbf{s}$ and $\mathbf{t}$ are comparable with respect to the componentwise order. Furthermore, we show that in the two-dimensional case, the reachability problem for Bellman operators is decidable for arbitrary $\mathbf{s}, \mathbf{t} \in \mathbb{Q}^2$. This stands in sharp contrast to the known undecidability of reachability for general piecewise affine maps in dimension $d = 2$.

cs.DM↗

arXiv2025

A Unifying Approach to Product Constructions for Quantitative Temporal Inference

Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temporal inference: to compute the likelihood that the execution traces satisfy a given temporal property. This paper presents a general framework for temporal inference, which applies to a rich variety of quantitative models including those that arise in the operational semantics of probabilistic and weighted programs. The key idea underlying our framework is that in a variety of existing approaches, the main construction that enables temporal inference is that of a product between the system of interest and the temporal property. We provide a unifying mathematical definition of product constructions, enabled by the realisation that 1) both systems and temporal properties can be modelled as coalgebras and 2) product constructions are distributive laws in this context. Our categorical framework leads us to our main contribution: a sufficient condition for correctness, which is precisely what enables to use the product construction for temporal inference. We show that our framework can be instantiated to naturally recover a number of disparate approaches from the literature including, e.g., partial expected rewards in Markov reward models, resource-sensitive reachability analysis, and weighted optimization problems. Further, we demonstrate a product of weighted programs and weighted temporal properties as a new instance to show the scalability of our approach.

cs.LO↗

arXiv2025

String Diagram of Optimal Transports

We present a novel hierarchical framework for optimal transport (OT) using string diagrams, namely string diagrams of optimal transports. This framework reduces complex hierarchical OT problems to standard OT problems, allowing efficient synthesis of optimal hierarchical transportation plans. Our approach uses algebraic compositions of cost matrices to effectively model hierarchical structures. We also study an adversarial situation with multiple choices in the cost matrices, where we present a polynomial-time algorithm for a relaxation of the problem. Experimental results confirm the efficiency and performance advantages of our proposed algorithm over the naive method.

cs.AI↗

arXiv2025

Sinkhorn Algorithm for Sequentially Composed Optimal Transports

Sinkhorn algorithm is the de-facto standard approximation algorithm for optimal transport, which has been applied to a variety of applications, including image processing and natural language processing. In theory, the proof of its convergence follows from the convergence of the Sinkhorn--Knopp algorithm for the matrix scaling problem, and Altschuler et al. show that its worst-case time complexity is in near-linear time. Very recently, sequentially composed optimal transports were proposed by Watanabe and Isobe as a hierarchical extension of optimal transports. In this paper, we present an efficient approximation algorithm, namely Sinkhorn algorithm for sequentially composed optimal transports, for its entropic regularization. Furthermore, we present a theoretical analysis of the Sinkhorn algorithm, namely (i) its exponential convergence to the optimal solution with respect to the Hilbert pseudometric, and (ii) a worst-case complexity analysis for the case of one sequential composition.

cs.DS↗

arXiv2024

A Design Method of an Ultra-Wideband and Easy-to-Array Magic-T: A 6-14 GHz Scaled Model for a mm/submm Camera

We established a design method for a Magic-T with a single-layer dielectric/metal structure suitable for both wideband and multi-element applications for millimeter and submillimeter wave imaging observations. The design method was applied to a Magic-T with a coupled-line, stubs, and single-stage impedance transformers in a frequency-scaled model (6-14 GHz) that is relatively easy to demonstrate through manufacturing and evaluation. The major problem is that using the conventional perfect matching condition for a coupled-line alone produces an impractically large width coplanar coupled-line (CPCL) to satisfy the desired bandwidth ratio. In our study, by removing this constraint and optimizing impedances utilizing a circuit simulator with high computation speed, we found a solution with a $\sim$ 180 $\rm μ$m wide CPCL, which is approximately an order of magnitude smaller than the conventional analytical solution. Furthermore, considering the effect of transition discontinuities in the transmission lines, we optimized the line length and obtained a design solution with return loss < -20 dB, amplitude imbalance < 0.1 dB, and phase imbalance < 0.5$^\circ$ from 6.1 GHz to 14.1 GHz.

astro-ph.IM↗

arXiv2024

Composing Codensity Bisimulations

Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system. In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality. ...

cs.LO↗

arXiv2024

Compositional Value Iteration with Pareto Caching

The de-facto standard approach in MDP verification is based on value iteration (VI). We propose compositional VI, a framework for model checking compositional MDPs, that addresses efficiency while maintaining soundness. Concretely, compositional MDPs naturally arise from the combination of individual components, and their structure can be expressed using, e.g., string diagrams. Towards efficiency, we observe that compositional VI repeatedly verifies individual components. We propose a technique called Pareto caching that allows to reuse verification results, even for previously unseen queries. Towards soundness, we present two stopping criteria: one generalizes the optimistic value iteration paradigm and the other uses Pareto caches in conjunction with recent baseline algorithms. Our experimental evaluations shows the promise of the novel algorithm and its variations, and identifies challenges for future work.

cs.LO↗

arXiv2024

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers string diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a Pareto curve on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach.

cs.LO↗