A gray box approach for Large Language Model-guided Natural Language to Temporal Logic Automatic Translation

Verification of Cyberphysical Systems (CPS) is fundamental to design and deployment of devices, and it relies on specification-based monitoring through expert engineers devised properties, subsequently expressed through several forms of formal logic (e.g., first order, propositional, temporal) depending on the needed semantics.