arXiv subjects

Yanjing Wang

Publications and source records attributed to Yanjing Wang.

At least 19 recordsLinked to original sources

arXiv2026

Proceedings of the Sixteenth International Conference on Advances in Modal Logic

Advances in Modal Logic (AiML) was founded in 1995 as an initiative devoted to presenting an up-to-date picture of research in modal logic and its many applications. It combines a conference series with volumes arising from the conferences, and has become the flagship international forum for work on all aspects of modal logic. Over the past three decades, AiML has both recorded and helped shape developments across the field, bringing together semantic, proof-theoretic, algebraic, topological, computational, philosophical, and applied perspectives on modal and related logics. Exactly thirty years after the first AiML conference, AiML 2026, the sixteenth conference in the series, is organized by the Institute of Logic, Language and Computation (ILLC) of the University of Amsterdam. The conference takes place in Amsterdam, the Netherlands, from 29 June to 3 July 2026. This volume contains abstracts of invited talks and full papers accepted for the conference. Beginning with AiML 2026, the proceedings are published open access via Electronic Proceedings in Theoretical Computer Science (EPTCS).

cs.LO↗

arXiv2025

Cohet: A CXL-Driven Coherent Heterogeneous Computing Framework with Hardware-Calibrated Full-System Simulation

Conventional heterogeneous computing systems built on PCIe interconnects suffer from inefficient fine-grained host-device interactions and complex programming models. In recent years, many proprietary and open cache-coherent interconnect standards have emerged, among which compute express link (CXL) prevails in the open-standard domain after acquiring several competing solutions. Although CXL-based coherent heterogeneous computing holds the potential to fundamentally transform the collaborative computing mode of CPUs and XPUs, research in this direction remains hampered by the scarcity of available CXL-supported platforms, immature software/hardware ecosystems, and unclear application prospects. This paper presents Cohet, the first CXL-driven coherent heterogeneous computing framework. Cohet decouples the compute and memory resources to form unbiased CPU and XPU pools which share a single unified and coherent memory pool. It exposes a standard malloc/mmap interface to both CPU and XPU compute threads, leaving the OS dealing with smart memory allocation and management of heterogeneous resources. To facilitate Cohet research, we also present a full-system cycle-level simulator named SimCXL, which is capable of modeling all CXL sub-protocols and device types. SimCXL has been rigorously calibrated against a real CXL testbed with various CXL memory and accelerators, showing an average simulation error of 3%. Our evaluation reveals that CXL.cache reduces latency by 68% and increases bandwidth by 14.4x compared to DMA transfers at cacheline granularity. Building upon these insights, we demonstrate the benefits of Cohet with two killer apps, which are remote atomic operation (RAO) and remote procedure call (RPC). Compared to PCIe-NIC design, CXL-NIC achieves a 5.5 to 40.2x speedup for RAO offloading and an average speedup of 1.86x for RPC (de)serialization offloading.

cs.AR↗

arXiv2025

Distributed Knowing How

Distributed knowledge is a key concept in the standard epistemic logic of knowledge-that. In this paper, we propose a corresponding notion of distributed knowledge-how and study its logic. Our framework generalizes two existing traditions in the logic of know-how: the individual-based multi-step framework and the coalition-based single-step framework. In particular, we assume a group can accomplish more than what its individuals can jointly do. The distributed knowledge-how is based on the distributed knowledge-that of a group whose multi-step strategies derive from distributed actions that subgroups can collectively perform. As the main result, we obtain a sound and strongly complete proof system for our logic of distributed knowledge-how, which closely resembles the logic of distributed knowledge-that in both the axioms and the proof method of completeness.

cs.LO↗

arXiv2025

A Full-System Simulation Framework for CXL-Based SSD Memory System

Compute eXpress Link (CXL) is a promising technology for memory disaggregation and expansion. Especially, CXL makes it more effectively for large-capacity storage devices such as Solid State Drive (SSD) to be deployed in the memory pool. However, CXL-based SSDs are still in early stages, necessitating the development of reliable simulation tools. In this paper, we propose CXL-SSD-Sim, the first open-source full-system simulator designed to simulate CXL-based SSD memory system. Constructed on the foundation of gem5 and SimpleSSD, CXL-SSD-Sim extends an high fidelity SSD memory expander model along with the corresponding device driver. In addition, CXL-SSD-Sim models a DRAM layer as a caching mechanism for the SSD, meticulously engineered to counteract latency issues inherent to CXL-based SSD memory access. Experiments are performed among five different memory devices with CXL-SSD-Sim in aspect of latency, bandwidth and real-world benchmark performance. These experiments serve to underscore the efficacy of our simulation tool in providing a comprehensive analysis of CXL-based SSD memory systems. The CXL-SSD-Sim simulator is available at https://github.com/WangYaohuii/CXL-SSD-Sim.

cs.AR↗

arXiv2024

CXL-DMSim: A Full-System CXL Disaggregated Memory Simulator With Comprehensive Silicon Validation

Compute eXpress Link (CXL) has emerged as a key enabler of memory disaggregation for future heterogeneous computing systems to expand memory on-demand and improve resource utilization. However, CXL is still in its infancy stage and lacks commodity products on the market, thus necessitating a reliable system-level simulation tool for research and development. In this paper, we propose CXL-DMSim, an open-source full-system simulator to simulate CXL disaggregated memory systems with high fidelity at a gem5-comparable simulation speed. CXL-DMSim incorporates a flexible CXL memory expander model along with its associated device driver, and CXL protocol support with CXL.io and CXL.mem. It can operate in both app-managed mode and kernel-managed mode, with the latter using a dedicated NUMA-compatible mechanism. The simulator has been rigorously verified against a real hardware testbed with both FPGAand ASIC-based CXL memory devices, which demonstrates the qualification of CXL-DMSim in simulating the characteristics of various CXL memory devices at an average simulation error of 3.4%. The experimental results using LMbench and STREAM benchmarks suggest that the CXL-FPGA memory exhibits a ~2.88x higher latency than local DDR while the CXL-ASIC latency is ~2.18x; CXL-FPGA achieves 45-69% of local DDR memory bandwidth, whereas the number for CXLASIC is 82-83%. The study also reveals that CXL memory can significantly enhance the performance of memory-intensive applications, improved by 23x at most with limited local memory for Viper key-value database and approximately 60% in memorybandwidth-sensitive scenarios such as MERCI. Moreover, the simulator's observability and expandability are showcased with detailed case-studies, highlighting its great potential for research on future CXL-interconnected hybrid memory pool.

cs.ET↗

arXiv2023

Epistemic Syllogistic: First Steps

Aristotle's discussions on modal syllogistic have often been viewed as error-prone and have garnered significant attention in the literature due to historical and philosophical interests. However, from a contemporary standpoint, they also introduced natural fragments of first-order modal logic, warranting a comprehensive technical analysis. In this paper, drawing inspiration from the natural logic program, we propose and examine several variants of modal syllogistic within the epistemic context, thereby coining the term Epistemic Syllogistic. Specifically, we concentrate on the de re interpretation of epistemic syllogisms containing non-trivial yet natural expressions such as "all things known to be A are also known to be not B." We explore the epistemic apodeictic syllogistic and its extensions, which accommodate more complex terms. Our main contributions include several axiomatizations of these logics, with completeness proofs that may be of independent interest.

cs.AI↗

arXiv2022

Inquisitive Logic as an Epistemic Logic of Knowing How

In this paper, we present an alternative interpretation of propositional inquisitive logic as an epistemic logic of knowing how. In our setting, an inquisitive logic formula $α$ being supported by a state is formalized as "knowing how to resolve $α$" (more colloquially, "knowing how $α$ is true") holds on the S5 epistemic model corresponding to the state. Based on this epistemic interpretation, we use a dynamic epistemic logic with both know-how and know-that operators to capture the epistemic information behind the innocent-looking connectives in inquisitive logic. We show that the set of valid know-how formulas corresponds precisely to the inquisitive logic. The main result is a complete axiomatization with intuitive axioms using the full dynamic epistemic language. Moreover, we show that the know-how operator and the dynamic operator can both be eliminated without changing the expressivity over models, which is consistent with the modal translation of inquisitive logic existing in the literature. We hope our framework can give an intuitive alternative interpretation of various concepts and technical results in inquisitive logic, and also provide a powerful and flexible tool to do inquisitive reasoning in an epistemic context.

math.LO↗

arXiv2022

An Epistemic Interpretation of Tensor Disjunction

This paper aims to give an epistemic interpretation to the tensor disjunction in dependence logic, through a rather surprising connection to the so-called weak disjunction in Medvedev's early work on intermediate logic under the Brouwer-Heyting-Kolmogorov (BHK)-interpretation. We expose this connection in the setting of inquisitive logic with tensor disjunction discussed by Ciardelli and Barbero (2019}, but from an epistemic perspective. More specifically, we translate the propositional formulae of inquisitive logic with tensor into modal formulae in a powerful epistemic language of "knowing how" following the proposal by Wang (2021). We give a complete axiomatization of the logic of our full language based on Fine's axiomatization of S5 modal logic with propositional quantifiers. Finally, we generalize the tensor operator with parameters $k$ and $n$, which intuitively captures the epistemic situation that one knows $n$ potential answers to $n$ questions and is sure $k$ answers of them must be correct. The original tensor disjunction is the special case when $k=1$ and $n=2$. We show that the generalized tensor operators do not increase the expressive power of our logic, the inquisitive logic, and propositional dependence logic, though most of these generalized tensors are not uniformly definable in these logics, except in our dynamic epistemic logic of knowing how.

math.LO↗

arXiv2022

Are Bundles Good Deals for FOML?

Bundled products are often offered as good deals to customers. When we bundle quantifiers and modalities together (as in $\exists x \Box$, $\Diamond \forall x$ etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting fragments of FOML without any restriction on the arity of predicates, the number of variables, or the modal scope. It is well-known that finding decidable fragments of FOML is hard, so we may ask: do bundled fragments that exploit the distinct expressivity of FOML constitute good deals in balancing the expressivity and complexity? There are a few positive earlier results on some particular fragments. In this paper, we try to fully map the terrain of bundled fragments of FOML in (un)decidability, and in the cases without a definite answer yet, we show that they lack the finite model property. Moreover, whether the logics are interpreted over constant domains (across states/worlds) or increasing domains presents another layer of complexity. We also present the \textit{loosely bundled fragment}, which generalizes the bundles and yet retain decidability (over increasing domain models).

cs.LO↗

arXiv2021

Knowing How to Plan

Various planning-based know-how logics have been studied in the recent literature. In this paper, we use such a logic to do know-how-based planning via model checking. In particular, we can handle the higher-order epistemic planning involving know-how formulas as the goal, e.g., find a plan to make sure p such that the adversary does not know how to make p false in the future. We give a PTIME algorithm for the model checking problem over finite epistemic transition systems and axiomatize the logic under the assumption of perfect recall.

cs.AI↗

arXiv2021

De Re Updates

In this paper, we propose a lightweight yet powerful dynamic epistemic logic that captures not only the distinction between de dicto and de re knowledge but also the distinction between de dicto and de re updates. The logic is based on the dynamified version of an epistemic language extended with the assignment operator borrowed from dynamic logic, following the work of Wang and Seligman (Proc. AiML 2018). We obtain complete axiomatizations for the counterparts of public announcement logic and event-model-based DEL based on new reduction axioms taking care of the interactions between dynamics and assignments.

cs.AI↗

arXiv2019

How to Agree without Understanding Each Other: Public Announcement Logic with Boolean Definitions

In standard epistemic logic, knowing that p is the same as knowing that p is true, but it does not say anything about understanding p or knowing its meaning. In this paper, we present a conservative extension of Public Announcement Logic (PAL) in which agents have knowledge or belief about both the truth values and the meanings of propositions. We give a complete axiomatization of PAL with Boolean Definitions and discuss various examples. An agent may understand a proposition without knowing its truth value or the other way round. Moreover, multiple agents can agree on something without agreeing on its meaning and vice versa.

cs.LO↗

arXiv2019

Weakly Aggregative Modal Logic: Characterization and Interpolation (new version)

Weakly Aggregative Modal Logic (WAML) is a collection of disguised polyadic modal logics with n-ary modalities whose arguments are all the same. WAML has some interesting applications on epistemic logic and logic of games, so we study some basic model theoretical aspects of WAML in this paper. Specifically, we give a van Benthem-Rosen characterization theorem of WAML based on an intuitive notion of bisimulation and show that each basic WAML system K_n lacks Craig Interpolation.

cs.LO↗

arXiv2018

When Names Are Not Commonly Known: Epistemic Logic with Assignments

In standard epistemic logic, agent names are usually assumed to be common knowledge implicitly. This is unreasonable for various applications. Inspired by term modal logic and assignment operators in dynamic logic, we introduce a lightweight modal predicate logic where names can be non-rigid. The language can handle various de dicto and de re distinctions in a natural way. The main technical result is a complete axiomatisation of this logic over S5 models.

cs.AI↗

arXiv2018

Bundled fragments of first-order modal logic: (un)decidability

Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the domain stays the same across worlds, or not. In particular, we show that the bundle $\forall \Box$ is undecidable over constant domain interpretations, even with only monadic predicates, whereas $\exists \Box$ bundle is decidable. On the other hand, over increasing domain interpretations, we get decidability with both $\forall \Box$ and $\exists \Box$ bundles with unrestricted predicates. In these cases, we also obtain tableau based procedures that run in \PSPACE. We further show that the $\exists \Box$ bundle cannot distinguish between constant domain and increasing domain interpretations.

cs.LO↗

arXiv2017

A New Modal Framework for Epistemic Logic

Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of $\exists x \Box ϕ$, e.g., knowing how to achieve $ϕ$ roughly means that there exists a way such that you know that it is a way to ensure that $ϕ$. Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality $\Box^x$, which packs exactly $\exists x \Box$ together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t.\ first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between $\Box^x$ and know-that operator in an epistemic setting.

cs.AI↗

arXiv2017

Strategically knowing how

In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve $ϕ$ means that there exists a (uniform) strategy such that the agent knows that it can make sure $ϕ$. We give an intuitive axiomatization of our logic and prove the soundness, completeness, and decidability of the logic. The crucial axioms relating knowing that and knowing how illustrate our understanding of knowing how in this setting. This logic can be used in representing both knowledge-that and knowledge-how.

cs.AI↗

arXiv2017

True Lies

A true lie is a lie that becomes true when announced. In a logic of announcements, where the announcing agent is not modelled, a true lie is a formula (that is false and) that becomes true when announced. We investigate true lies and other types of interaction between announced formulas, their preconditions and their postconditions, in the setting of Gerbrandy's logic of believed announcements, wherein agents may have or obtain incorrect beliefs. Our results are on the satisfiability and validity of instantiations of these semantically defined categories, on iterated announcements, including arbitrarily often iterated announcements, and on syntactic characterization. We close with results for iterated announcements in the logic of knowledge (instead of belief), and for lying as private announcements (instead of public announcements) to different agents. Detailed examples illustrate our lying concepts.

cs.AI↗