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.

28 papers

2 author rows

FM Conference 2026 Conference Paper

Automated LTL Specification Generation from Industrial Aerospace Requirements

Zhi Ma
Xiao Liang
Cheng Wen
Rui Chen
Bin Gu
Shengchao Qin
Cong Tian
Mengfei Yang

Abstract In the development and verification of safety-critical aero-space software, Linear Temporal Logic (LTL) has been widely used to specify complex system properties derived from requirements. However, a significant gap remains in industrial practice: translating natural language (NL) requirements into formal LTL properties is a labor-intensive and error-prone process that requires rare expertise in both aerospace control engineering and formal methods. While recent NL-to-LTL tools ( e. g. , NL2SPEC, NL2TL, NL2LTL) are capable of automating parts of this process, they often fail on real requirement documents in industrial settings, due to complex domain terminology or implicit temporal and logical structure. To address these challenges, we present Aero Req2LTL, a framework that automates LTL property generation for aerospace requirements using large language models (LLMs), with two key industrial innovations: (i) a data dictionary that normalizes technical jargon into precise atomic propositions; and (ii) a template-based requirement language that makes temporal cues and logical relations explicit before translation. On a real aerospace dataset, Aero Req2LTL achieves 85% precision and 88% recall in LTL generation, and its outputs can be directly consumed by existing verification tools.

DOI

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

TCS Journal 2025 Journal Article

Improved SARSA and DQN algorithms for reinforcement learning

Guangyu Yao
Nan Zhang
Zhenhua Duan
Cong Tian

Reinforcement learning is a branch of machine learning in which an agent interacts with an environment to learn optimal actions that maximize cumulative rewards. This paper aims to enhance the SARSA and DQN algorithms in four key aspects: the ε-greedy policy, reward function, value iteration approach, and sampling probability. The experiments are conducted in three scenarios: path planning, CartPole, and MountainCar. The results show that, in these environments, the improved algorithms exhibit better convergence, higher rewards, and more stable training processes.