Author name cluster

Zhilin Wu

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.

9 papers

2 author rows

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

MFCS Conference 2017 Conference Paper

The Complexity of SORE-definability Problems

Ping Lu 0007
Zhilin Wu
Haiming Chen 0001

Single occurrence regular expressions (SORE) are a special kind of deterministic regular expressions, which are extensively used in the schema languages DTD and XSD for XML documents. In this paper, with motivations from the simplification of XML schemas, we consider the SORE-definability problem: Given a regular expression, decide whether it has an equivalent SORE. We investigate extensively the complexity of the SORE-definability problem: We consider both (standard) regular expressions and regular expressions with counting, and distinguish between the alphabets of size at least two and unary alphabets. In all cases, we obtain tight complexity bounds. In addition, we consider another variant of this problem, the bounded SORE-definability problem, which is to decide, given a regular expression E and a number M (encoded in unary or binary), whether there is an SORE, which is equivalent to E on the set of words of length at most M. We show that in several cases, there is an exponential decrease in the complexity when switching from the SORE-definability problem to its bounded variant.

Details

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

I&C Journal 2016 Journal Article

On temporal logics with data variable quantifications: Decidability and complexity

Fu Song
Zhilin Wu

Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. Grumberg, Kupferman and Sheinvald initiated the research on this topic recently and obtained several interesting results. However, there is still a lack of systematic investigation on the theoretical aspects of the variable extensions of temporal logics. Our goal in this paper is to fill this gap. Around this goal, we make the following choices: 1. We consider the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), and allow arbitrary nestings of variable quantifications with Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL). 2. We investigate the decidability and complexity of both the satisfiability and model checking problems, over both finite and infinite words (trees). In particular, we obtain the following results: Existential variable quantifiers or one single universal quantifier in the beginning already entail the undecidability of the satisfiability problems of both VLTL and VCTL, over both finite and infinite words (trees); if only existential path quantifiers are used in VCTL, then the satisfiability problem (over finite trees) is decidable, no matter which variable quantifiers are available; for VLTL formulae with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variables, then its satisfiability problem becomes decidable, over both finite and infinite words; based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.

Details DOI

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

TCS Journal 2014 Journal Article

On effective construction of the greatest solution of language inequality X A ⊆ B X

Olivier Ly
Zhilin Wu

In this paper, we consider effective constructions of the greatest solution of the language inequality X A ⊆ B X. It has been proved by Kunc in 2005 that the greatest solution of X A ⊆ B X is regular provided that B is regular, no matter what A is. However this proof is based on Kruskal's tree theorem, and does not provide any effective way to construct the greatest solution. We focus on this gap in this paper. We give an effective construction of the greatest solution for the following two cases: (i) A, B are regular and there exists k ⩾ 1 such that pref ( B ) A k ∩ B ⩽ k pref ( B ) = ∅, where pref ( B ) is the set of prefixes of words in B, (ii) A, B are regular and B is a code with finite decoding delay. Our construction takes the point of view of games. As shown by Kunc in his regularity proof, the construction of the greatest solution can be reduced to the construction of the winning region of a two-player game. Our contribution is to show that the winning regions of the two-player game for the two cases can be constructed effectively. The main ingredient of the construction for the first case is a shrinking lemma for the words on which one of the players has a winning strategy. While the construction for the second case is based on the observation that the two-player game can be reduced to a two-player reachability game played on the transition graph of a one-counter machine.

Details DOI

Highlights Conference 2014 Conference Abstract

Regular Path Queries on Graphs with Data: A Rigid Approach

Zhilin Wu

Regular path queries (RPQ) is a classical navigational query formalism for graph databases to specify constraints on labeled paths. Recently, RPQs have been extended by Libkin and Vrgoc to incorporate data value comparisons among different nodes on paths, called regular path queries with data (RDPQ). It has been shown that the evaluation problem of RDPQs is PSPACE-complete and NLOGSPACE-complete in data complexity. On the other hand, the containment problem of RDPQs is in general undecidable. In this paper, we propose a novel approach to extend regular path queries with data value comparisons, called rigid regular path queries with data (RRDPQ). The main ingredient of this approach is an automata model called nondeterministic rigid register automata (NRRA), in which the data value comparisons are rigid, in the sense that if the data value in the current position x is compared to a data value in some other position y, then by only using the labels (but not data values), the position y can be uniquely determined from x. We show that NRRAs are robust in the sense that nondeterministic, deterministic and two-way variant of NRRAs, as well as an extension of regular expressions, are all of the same expressivity. We then argue that the expressive power of RDPQs are reasonable by demonstrating that for every graph database, there is a localized transformation of the graph database so that every RDPQ in the original graph database can be turned into an equivalent RRDPQ over the transformed one. Finally, we investigate the computational properties of RRDPQs and conjunctive RRDPQs (CRRDPQ). In particular, we show that the containment of CRRDPQs (and RRDPQs) can be decided in 2EXPSPACE.

PDF Details

CSL Conference 2012 Conference Paper

Commutative Data Automata

Zhilin Wu

Formalisms over infinite alphabets have recently received much focus in the community of theoretical computer science. Data automaton is a formal model for words over an infinite alphabet, that is, the product of a finite set of labels and an infinite set of data values, proposed by Bojanczyk, Muscholl, Schwentick et. al. in 2006. A data automaton consists of two parts, a nondeterministic letter-to-letter transducer, and a class condition specified by a finite automaton, which acts as a condition on each subword of the outputs of the transducer in corresponding to a maximal set of positions with the same data value. It is open whether the nonemptiness of data automata can be decided with elementary complexity, since this problem is equivalent to the reachability of petri nets. Very recently, a restriction of data automata with elementary complexity, called weak data automata, was proposed by Kara, Schwentick and Tan and its nonemptiness problem was shown to be in 2NEXPTIME. In weak data automata, the class conditions are specified by some simple constraints on the number of occurrences of labels occurring in every class. The aim of this paper is to demonstrate that the commutativity of class conditions is the genuine reason accounting for the elementary complexity of weak data automata. For this purpose, we define and investigate commutative data automata, which are data automata with class conditions restricted to commutative regular languages. We show that while the expressive power of commutative data automata is strictly stronger than that of weak data automata, the nonemptiness problem of this model can still be decided with elementary complexity, more precisely, in 3NEXPTIME. In addition, we extend the results to data omega-words and prove that the nonemptiness of commutative Büchi data automata can be decided in 4NEXPTIME. We also provide logical characterizations for commutative (Büchi) data automata, similar to those for weak (Büchi) data automata.

Details

GandALF Workshop 2011 Workshop Paper

A Decidable Extension of Data Automata

Zhilin Wu

Data automata on data words is a decidable model proposed by Bojańczyk et al. in 2006. Class automata, introduced recently by Bojańczyk and Lasota, is an extension of data automata which unifies different automata models on data words. The nonemptiness of class automata is undecidable, since class automata can simulate two-counter machines. In this paper, a decidable model called class automata with priority class condition, which restricts class automata but strictly extends data automata, is proposed. The decidability of this model is obtained by establishing a correspondence with priority multicounter automata. This correspondence also completes the picture of the links between various class conditions of class automata and various models of counter machines. Moreover, this model is applied to extend a decidability result of Alur, Černý and Weinstein on the algorithmic analysis of array-accessing programs.

PDF Details DOI