Author name cluster

Taolue Chen

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

1 author row

FM Conference 2026 Conference Paper

Can LLM Aid in Solving Constraints with Inductive Definitions?

Weizhi Feng
Shidong Shen
Jiaxiang Liu
Taolue Chen
Fu Song
Zhilin Wu

Abstract Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e. g. , abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

DOI

IJCAI Conference 2025 Conference Paper

Simulate, Refine and Integrate: Strategy Synthesis for Efficient SMT Solving

Bingzhe Zhou
Hannan Wang
Yuan Yao
Taolue Chen
Feng Xu
Xiaoxing Ma

Satisfiability Modulo Theories (SMT) solvers are crucial in many applications, yet their performance is often a bottleneck. This paper introduces SIRISMT, a novel framework that employs machine learning techniques for the automatic synthesis of efficient SMT-solving strategies. Specifically, SIRISMT targets at Z3 and consists of three key stages. First, given a set of training SMT formulas, SIRISMT simulates the solving process by leveraging reinforcement learning to guide its exploration within the strategy space. Next, SIRISMT refines the collected strategies by pruning redundant tactics and generating augmented strategies based on the subsequence structure of the learned strategies. These refined strategies are then fed back into the reinforcement learning model. Finally, the refined and optimized strategies are integrated into one strategy, which can be directly plugged into modern SMT solvers. Extensive evaluations show the superior performance of SIRISMT over the baseline methods. For example, compared to the default Z3, it solves 26. 8% more formulas and achieves up to an 86. 3% improvement in the Par-2 score on benchmark datasets. Additionally, we show that the synthesized strategy can improve the code coverage by up to 11. 8% in a downstream symbolic execution benchmark.

PDF Details DOI

NeurIPS Conference 2023 Conference Paper

Neuro-symbolic Learning Yielding Logical Constraints

Zenan Li
Yunpeng Huang
Zhaoyu Li
Yuan Yao
Jingwei Xu
Taolue Chen
Xiaoxing Ma
Jian Lu

Neuro-symbolic systems combine the abilities of neural perception and logical reasoning. However, end-to-end learning of neuro-symbolic systems is still an unsolved challenge. This paper proposes a natural framework that fuses neural network training, symbol grounding, and logical constraint synthesis into a coherent and efficient end-to-end learning process. The capability of this framework comes from the improved interactions between the neural and the symbolic parts of the system in both the training and inference stages. Technically, to bridge the gap between the continuous neural network and the discrete logical constraint, we introduce a difference-of-convex programming technique to relax the logical constraints while maintaining their precision. We also employ cardinality constraints as the language for logical constraint learning and incorporate a trust region method to avoid the degeneracy of logical constraint in learning. Both theoretical analyses and empirical evaluations substantiate the effectiveness of the proposed framework.

PDF Details

AAAI Conference 2019 Conference Paper

Probabilistic Alternating-Time µ -Calculus

Fu Song
Yedi Zhang
Taolue Chen
Yu Tang
Zhiwu Xu

Reasoning about strategic abilities is key to an AI system consisting of multiple agents with random behaviors. We propose a probabilistic extension of Alternating µ-Calculus (AMC), named PAMC, for reasoning about strategic abilities of agents in stochastic multi-agent systems. PAMC subsumes existing logics AMC and PµTL. The usefulness of PAMC is exemplified by applications in genetic regulatory networks. We show that, for PAMC, the model checking problem is in UP∩co-UP, and the satisfiability problem is EXPTIME-complete, both of which are the same as those for AMC. Moreover, PAMC admits the small model property. We implement the satisfiability checking procedure in a tool PAMCSolver.

PDF Details

TCS Journal 2018 Journal Article

Polynomial-time algorithms for computing distances of fuzzy transition systems

Taolue Chen
Tingting Han
Yongzhi Cao

Behaviour distances to measure the resemblance of two states in a (nondeterministic) fuzzy transition system have been proposed recently in literature. Such a distance, defined as a pseudo-ultrametric over the state space of the model, provides a quantitative analogue of bisimilarity. In this paper, we focus on the problem of computing these distances. We first extend the definition of the pseudo-ultrametric by introducing discount such that the discounting factor being equal to 1 captures the original definition. We then provide polynomial-time algorithms to calculate the behavioural distances, in both the non-discounted and the discounted setting. The algorithm is strongly polynomial in the former case.

Details DOI

AAAI Conference 2016 Conference Paper

Global Model Checking on Pushdown Multi-Agent Systems

Taolue Chen
Fu Song
Zhilin Wu

Pushdown multi-agent systems, modeled by pushdown game structures (PGSs), are an important paradigm of inﬁnite-state multi-agent systems. Alternatingtime temporal logics are well-known speciﬁcation formalisms for multi-agent systems, where the selective path quantiﬁer is introduced to reason about strategies of agents. In this paper, we investigate model checking algorithms for variants of alternating-time temporal logics over PGSs, initiated by Murano and Perelli at IJCAI’15. We ﬁrst give a triply exponential-time model checking algorithm for ATL∗ over PGSs. The algorithm is based on the saturation method, and is the ﬁrst global model checking algorithm with a matching lower bound. Next, we study the model checking problem for the alternating-time μ-calculus. We propose an exponential-time global model checking algorithm which extends similar algorithms for pushdown systems and modal μ-calculus. The algorithm admits a matching lower bound, which holds even for the alternation-free fragment and ATL.

PDF Details

IJCAI Conference 2016 Conference Paper

Verifying Pushdown Multi-Agent Systems against Strategy Logics

Taolue Chen
Fu Song
Zhilin Wu

In this paper, we investigate model checking algorithms for variants of strategy logic over pushdown multi-agent systems, modeled by pushdown game structures (PGSs). We consider various fragments of strategy logic, i. e. , SL[CG], SL[DG], SL[1G] and BSIL. We show that the model checking problems on PGSs for SL[CG], SL[DG] and SL[1G] are 3EXTIME-complete, which are not harder than the problem for the subsumed logic ATL*. When BSIL is concerned, the model checking problem becomes 2EXPTIME-complete. Our algorithms are automata-theoretic and based on the saturation technique, which are amenable to implementations.

PDF Details

I&C Journal 2014 Journal Article

Quantitative verification of implantable cardiac pacemakers over hybrid heart models

Taolue Chen
Marco Diciolla
Marta Kwiatkowska
Alexandru Mereacre

We develop a model-based framework which supports approximate quantitative verification of implantable cardiac pacemaker models over hybrid heart models. The framework is based on hybrid input–output automata and can be instantiated with user-specified pacemaker and heart models. For the specifications, we identify two property patterns which are tailored to the verification of pacemakers: “can the pacemaker maintain a normal heart behaviour? ” and “what is the energy level of the battery after t time units? ”. We implement the framework in Simulink based on the discrete-time simulation semantics and endow it with a range of basic and advanced quantitative property checks. The advanced property checks include the correction of pacemaker mediated Tachycardia and how the noise on sensor leads influences the pacing level. We demonstrate the usefulness of the framework for safety assurance of pacemaker software by instantiating it with two hybrid heart models and verifying a number of correctness properties with encouraging experimental results.

Details DOI

TCS Journal 2011 Journal Article

On the axiomatizability of priority II

Luca Aceto
Taolue Chen
Anna Ingolfsdottir
Bas Luttik
Jaco van de Pol

This paper contributes to the study of the equational theory of the priority operator of Baeten, Bergstra and Klop in the setting of the process algebra BCCSP. It is shown that, in the presence of at least two actions, the collection of process equations over BCCSP with the priority operator that are valid modulo bisimilarity, irrespective of the chosen priority order over actions, is not finitely based. This holds true even if one restricts oneself to the collection of valid process equations that do not contain occurrences of process variables.

Details DOI

I&C Journal 2008 Journal Article

On finite alphabets and infinite bases

Taolue Chen
Wan Fokkink
Bas Luttik
Sumit Nain

Van Glabbeek presented the linear time–branching time spectrum of behavioral semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatizations for most of these semantics. Groote proved for some of van Glabbeek’s axiomatizations that they are ω -complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. In this paper, we settle the remaining open questions for all the semantics in the linear time–branching time spectrum, either positively by giving a finite sound and ground-complete axiomatization that is ω -complete, or negatively by proving that such a finite basis for the equational theory does not exist. We prove that in case of a finite alphabet with at least two actions, failure semantics affords a finite basis, while for ready simulation, completed simulation, simulation, possible worlds, ready trace, failure trace and ready semantics, such a finite basis does not exist. Completed simulation semantics also lacks a finite basis in case of an infinite alphabet of actions.

Details DOI