2026-05-17T17:30:21Zhttps://keep.lib.asu.edu/oai/request

oai:keep.lib.asu.edu:node-2016112025-05-12T19:35:22Zoai_pmh:alloai_pmh:repo_items

201611 https://hdl.handle.net/2286/R.2.N.201611 http://rightsstatements.org/vocab/InC/1.0/ All Rights Reserved 2025 63 pages Masters Thesis Academic theses en Shukla, Eshita Pedrielli, Giulia Baral, Chitta Srivastava, Siddharth Arizona State University Partial requirement for: M.S., Arizona State University, 2025 Field of study: Computer Engineering Verification of Cyber-Physical Systems (CPS) ensures these systems adhere to desired properties typically expressed through natural language requirements and formally represented using temporal logic. Specification-based monitoring usingformal properties is a widely adopted method to evaluate CPS safety. However, the effectiveness of this monitoring-based approach critically depends on accurately translating natural language requirements into formal temporal logic properties. Often, testing engineers responsible for writing these requirements lack extensive experience with temporal logic and formal methods, highlighting the need for an intelligent, automated translation process. In this thesis, a novel gray-box Natural Language (NL) to Temporal Logic (TL) translation module is proposed. The proposed method conditions LLMs on temporal logic examples and augments them with an intermediate structural representation—a simplified Abstract Syntax Tree (AST). This AST explicitly captures hierarchical relationships between requirement components, facilitating improved model comprehension during translation. Quantifiable criteria are established to evaluate the quality of temporal logic examples used during training and testing, focusing specifically on metrics such as formula complexity and tree depth. By systematically examining these criteria, insights are provided into how formula structural complexity influences translation accuracy. Experiments demonstrate that integrating explicit structural information through ASTs consistently enhances translation accuracy. Additionally, the approach is benchmarked against state-of-the-art LLM-based translation methods, highlighting substantial performance improvements, particularly in complex scenarios characterized by higher formula complexity and increased tree depth. Computer Engineering Fine-tuning Gray Box Large Language Models temporal logic A Gray Box Approach for Large Language Model-guided Natural Language to Temporal Logic Automatic Translation