BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
X-LIC-LOCATION:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260730T152637Z
LOCATION:
DTSTART;TZID=America/Los_Angeles:20260728T124600
DTEND;TZID=America/Los_Angeles:20260728T124600
UID:dac_DAC 2026_sess315_RESEARCH2829@linklings.com
SUMMARY:LLM-Enhanced Two-Stage Signal Temporal Logic Automatic Transformat
 ion with Structured Intermediate Representation
DESCRIPTION:Hongjing Qing (Institute of Software, Chinese Academy of Scien
 ces; University of Chinese Academy of Sciences) and Jie An and Fanjiang Xu
  (Institute of Software, Chinese Academy of Sciences)\n\nSignal Temporal L
 ogic (STL) is a formal specification language for describing real-time and
  real-valued properties of Cyber-Physical Systems (CPS).Accurate and autom
 atic translation of CPS specifications in natural language (NL) into forma
 l STL formulas is crucial. Traditional methods relying on manual templates
  or deep-learning models are limited and lack flexibility.Recently, large-
 language models (LLMs) based methods partially addressed these issues, but
  did not consider the usefulness of the inherent structure of STL both for
  the translation itself and the result evaluation.To address these issues,
  we propose STLGen, a novel LLM-enhanced automatic transformation framewor
 k from NL to STL, which introduces a two-stage generation process with a s
 tructured natural language, named NL2, as the intermediate representation.
 In Stage 1, NL is converted into well-defined NL2 through structured promp
 t engineering. In Stage 2, NL2 is converted into STL formulas using a conv
 erter.Leveraging LLM-aided generation and closed-loop verification with ma
 tching algorithms, as well as fine-tune models in two stages with instruct
 ion fine-tuning and LoRA.Additionally, we introduce two evaluation metrics
 : the structure accuracy to assess STL syntax impact on logic and the STL-
 SCOTES to evaluate semantic consistency via STL trajectories.Experimental 
 results demonstrate that our method outperforms state-of-the-art methods a
 cross the classic evaluation metrics and our proposed metrics.\n\nTopics: 
 Quantum\n\nTrack: DES6. Quantum Computing, Systems\n\nSession Chairs: Hoke
 un Kim (Arizona State University); BaekGyu Kim (Daegu Gyeongbuk Institute 
 of Science and Technology); Xiang Chen (Peking University); Sangyeob Kim (
 Yonsei University); Robert M. Radway (University of Pennsylvania); Prashan
 th Mohan (University of Pittsburgh); Xiaoxuan Yang (University of Virginia
 , Stanford University); Ramtin Zand (University of South Carolina); Hadi K
 amali (University of Central Florida); Jiafeng Xie (Villanova University);
  Prabuddha Chakraborty (University of Maine); Junichiro Kadomoto (Universi
 ty of Tokyo); and Yosuke Ueno (RIKEN)\n\n
END:VEVENT
END:VCALENDAR
