Arrow Research search

Author name cluster

Cong Tian

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.

27 papers
2 author rows

Possible papers

27

AAAI Conference 2026 Conference Paper

T4NMTD: Transition-Centric Reinforcement Learning for Non-Markovian Task Decomposition

  • Ruixuan Miao
  • Xu Lu
  • Cong Tian
  • Bin Yu
  • Zhenhua Duan

Non-Markovian Tasks (NMTs) are distinguished by their dependence on long-term memory and state-dependent dynamics, setting them apart from the traditional Markovian models typically employed in Reinforcement Learning (RL). NMTs not only suffer from reward sparseness but also rely on historical information, making their resolution considerably more challenging. In this paper, we propose a novel RL framework T4NMTD (Transition-centric framework for NMT Decomposition), designed specifically for learning NMTs which are specified by temporal logic. The core of T4NMTD is a task decomposition mechanism along with a parallel training approach for NMTs. An NMT is first decomposed as basic units based on the transitions of the automata which are derived from temporal logic formulae. The units are then modularized into sub-tasks according to their semantic similarity under logical interpretation. The training strategy of T4NMTD adopts a dual-level structure: the high-level learns to shape the boundaries and coordinate arrangement of the sub-tasks from a global perspective, while the low-level learns those sub-tasks in parallel. In addition, we invent a dynamic policy intervention scheme to mitigate the policy myopic issue during parallel training. A comprehensive evaluation is conducted on benchmark problems with respect to various metrics. The experimental results demonstrate that T4NMTD effectively addresses NMTs, achieving significant performance improvements compared with related studies.

PDF Details DOI

IJCAI Conference 2025 Conference Paper

Neuron Similarity-Based Neural Network Verification via Abstraction and Refinement

  • Yuehao Liu
  • Yansong Dong
  • Liang Zhao
  • Wensheng Wang
  • Cong Tian

Deep neural networks (DNNs) have become integral to numerous safety-critical applications, necessitating rigorous verification of their trustworthiness. However, the problem of verifying DNNs has high computational complexity, and existing techniques have limited efficiency, insufficient to deal with large-scale network models. To address this challenge, we propose a novel abstraction-refinement verification method that reduces network size while maintaining verification accuracy. Specifically, the method quantifies the similarity between neurons based on various factors such as their interval outputs, and then merges similar neurons to generate a smaller abstract network. In addition, a counterexample-guided refinement process is developed to mitigate the impact of potential spurious counterexamples, so that verification results from the abstract network are applicable to the original network. We have implemented this method as a tool named ARVerifier and integrated it with three state-of-the-art verification tools for evaluation on ACAS Xu and MNIST benchmarks. Experimental results demonstrate that ARVerifier significantly reduces network size and yields verification time reductions by 11. 61%, 18. 70%, and 12. 20% compared to α, β-CROWN, Verinet, and Marabou, respectively. Moreover, ARVerifier exhibits efficiency improvements by 26. 64% and 46. 87% compared to existing abstraction-refinement methods NARv and CEGAR-NN, respectively.

PDF Details DOI

IJCAI Conference 2017 Conference Paper

Temporalising Separation Logic for Planning with Search Control Knowledge

  • Xu Lu
  • Cong Tian
  • Zhenhua Duan

Temporal logics are widely adopted in Artificial Intelligence (AI) planning for specifying Search Control Knowledge (SCK). However, traditional temporal logics are limited in expressive power since they are unable to express spatial constraints which are as important as temporal ones in many planning domains. To this end, we propose a two-dimensional (spatial and temporal) logic namely PPTL^SL by temporalising separation logic with Propositional Projection Temporal Logic (PPTL). The new logic is well-suited for specifying SCK containing both spatial and temporal constraints which are useful in AI planning. We show that PPTL^SL is decidable and present a decision procedure. With this basis, a planner namely S-TSolver for computing plans based on the spatio-temporal SCK expressed in PPTL^SL formulas is developed. Evaluation on some selected benchmark domains shows the effectiveness of S-TSolver.

PDF Details

IJCAI Conference 2016 Conference Paper

A Decision Procedure for a Fragment of Linear Time Mu-Calculus

  • Yao Liu
  • Zhenhua Duan
  • Cong Tian

In this paper, we study an expressive fragment, namely Gmu, of linear time mu-calculus as a high-level goal specification language. We define Goal Progression Form (GPF) for Gmu formulas and show that every closed formula can be transformed into this form. Based on GPF, we present the notion of Goal Progression Form Graph (GPG) which can be used to describe models of a formula. Further, we propose a simple and intuitive GPG-based decision procedure for checking satisfiability of Gmu formulas which has the same time complexity as the decision problem of Linear Temporal Logic (LTL). However, Gmu is able to express a wider variety of temporal goals compared with LTL.

PDF Details

TIME Conference 2011 Conference Paper

Synthesising Classic and Interval Temporal Logic

  • Sven Schewe
  • Cong Tian

Linear-Time Temporal Logic (LTL) is one of the most influential logics for the specification and verification of reactive systems. An important selling point of LTL is its striking simplicity, which might be a reason why none of the many extensions suggested to LTL have gained the same influence. Interval based temporal logics like Interval Temporal Logic (ITL) are a more recent branch of temporal logics with their own niche of interesting applications. On first glance, interval based temporal logics very little resemble LTL and the spread of these logics beyond their niche is hampered by a seeming structural incompatibility with LTL. When competing for being applied on a larger scale, interval based temporal logics would fight a losing battle against a more established competitor with better complexity and mature tools. In this paper, we suggest to extend ITL to Pop Logic (PL) by introducing a simple pop operator that revokes the binding of the chop operation-very much like the popping operation in a stack-and show that LTL can be viewed as a syntactic subset of PL. This is a surprising twist: by strengthening the comparably exotic logic ITL slightly and by using the new pop and the old chop operator as primitive constructs, we obtain a logic for which LTL is a de-facto syntactic fragment. The power of this extension is that it can, by subsuming both interval and classic temporal logics, synthesise both concepts to a common framework. The charm of this extension is that PL does not sacrifice the simplicity that makes its sub-logics attractive.

Details