9 papers
The -Chain Product: A Succinct Model of Automata (De)Composition (Extended Version)
Roberto Borelli, Davide Bresolin, Luca Geatti +2
The cascade product is a fundamental construction in automata theory, enabling hierarchical composition of automata and playing a central role in decomposition results such as the…
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…
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…
Unified Peripartum Database with Natural-Language-to-SQL Capabilities at Udine University Hospital: Design and Prototype
Doriana Armenise, Ginevra Battello, Andrea Brunello +7
The fragmentation of obstetric information across electronic health record modules, device repositories, and laboratory systems, as it is common in hospitals, hinders both intrapar…
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…
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…
Synthesis of Timeline-Based Planning Strategies Avoiding Determinization
Renato Acampora, Dario Della Monica, Luca Geatti +3
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…
Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)
Luca Geatti, Alessio Mansutti, Angelo Montanari
This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish…