arXiv subjects

Yun Chen Tsai

Publications and source records attributed to Yun Chen Tsai.

6 recordsLinked to original sources

arXiv2026

The Emptiness Problem for Quantum Finite Automata with Classical States

Quantum Finite Automata with Classical states (QFACs) are nondeterministic finite automata over a finite alphabet of quantum operations. We study expressiveness of this model on finite words and the corresponding emptiness problem. We show that regular languages are incomparable with those definable by Quantum Finite Automata (QFAs) and that both are strictly subsumed by QFAC-definable languages. We show that the emptiness problem for a QFAC can be reduced to the emptiness of the language intersection of a QFA and a finite automaton. This intersection is known to be decidable for strict thresholds but undecidable for non-strict cases. Furthermore, we consider the problem for flat QFACs, a restriction where the underlying automata contain no nested loops, and relate it to the higher-dimensional orbit problem, a long-standing open challenge in dynamical systems. Finally, we propose a sound and semi-complete witness searching procedure to verify the non-emptiness of one-loop QFACs, which are sufficiently expressive to represent some prominent quantum algorithms, such as Grover's search and quantum random walks.

cs.FL↗

arXiv2026

Monads and Distributive Laws in Substructural Contexts (Extended Version)

We present a categorical theory of monads and distributive laws in substructural contexts. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin's verbal categories $\mathbf W$, in a uniform and presentation-independent manner. We introduce the classes of $\mathbf W$-operadic monads (those defined via the structural rules in $\mathbf W$) and of $\mathbf W$-commutative monads (those invariant under the structural rules in $\mathbf W$). We give a canonical construction of a distributive law $ST\to TS$ of monads on $\mathbf{Set}$; it is applicable when $S$ is $\mathbf W$-operadic and $T$ is $\mathbf W$-commutative (under mild conditions). This accounts for many known and new distributive laws. Even when $S$ fails to be $\mathbf W$-operadic, we can refine $S$ and force $\mathbf W$-operadicity; this captures Varacca and Winskel's construction of indexed valuations.

cs.LO↗

arXiv2025

Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games

For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components--a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle--a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.

cs.LO↗

arXiv2025

Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)

Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.

cs.FL↗

arXiv2024

Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments

This paper addresses the synthesis of reactive systems that enforce hard constraints while optimizing for quality-based soft constraints. We build on recent advancements in combining reactive synthesis with example-based guidance to handle both types of constraints in stochastic, oblivious environments accessible only through sampling. Our approach constructs examples that satisfy LTL-based hard constraints while maximizing expected rewards-representing the soft constraints-on samples drawn from the environment. We formally define this synthesis problem, prove it to be NP-complete, and propose an SMT-based solution, demonstrating its effectiveness with a case study.

cs.FL↗

arXiv2024

Local Trajectory Variation Exponent (LTVE) for Visualizing Dynamical Systems

The identification and visualization of Lagrangian structures in flows plays a crucial role in the study of dynamic systems and fluid dynamics. The Finite Time Lyapunov Exponent (FTLE) has been widely used for this purpose; however, it only approximates the flow by considering the positions of particles at the initial and final times, ignoring the actual trajectory of the particle. To overcome this limitation, we propose a novel quantity that extends and generalizes the FTLE by incorporating trajectory metrics as a measure of similarity between trajectories. Our proposed method utilizes trajectory metrics to quantify the distance between trajectories, providing a more robust and accurate measure of the LCS. By incorporating trajectory metrics, we can capture the actual path of the particle and account for its behavior over time, resulting in a more comprehensive analysis of the flow. Our approach extends the traditional FTLE approach to include trajectory metrics as a means of capturing the complexity of the flow.

math.DS↗