11 papers
Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling
Andrea Brunello, Cristian Curaba, Luca Geatti +3
Accurate translation from Natural Language to First-Order Logic (NL-to-FOL) underpins neurosymbolic AI systems and Natural Language Inference (NLI), making the quality of NL-to-FOL…
Synthesis of timeline-based planning strategies avoiding determinization
Dario Della Monica, Angelo Montanari, Pietro Sala
Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative…
Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy
Andrea Brunello, Luca Geatti, Michele Mignani +2
Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g.…
Automata-less Monitoring via Trace-Checking (Extended Version)
Andrea Brunello, Luca Geatti, Angelo Montanari +1
In runtime verification, monitoring consists of analyzing the current execution of a system and determining, on the basis of the observed finite trace, whether all its possible con…
Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring
Andrea Brunello, Luca Geatti, Angelo Montanari +1
Monitoring is a runtime verification technique that allows one to check whether an ongoing computation of a system (partial trace) satisfies a given formula. It does not need a com…
Complexity of Safety and coSafety Fragments of Linear Temporal Logic
Alessandro Artale, Luca Geatti, Nicola Gigante +2
Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosa…