Prima Traduzione da LTL a LTLf+ per Obiettivi a Traccia Infinita

I ricercatori hanno introdotto la prima traduzione dalla Logica Temporale Lineare (LTL) a LTLf+, una logica che estende la LTL a tracce finite a tracce infinite preservando il potere espressivo della LTL. LTL è ampiamente utilizzata nell'IA per specificare obiettivi temporali nella sintesi reattiva, nella pianificazione stocastica e nell'apprendimento per rinforzo. Tradizionalmente, risolvere questi problemi richiede la traduzione di LTL in automi non deterministici su parole infinite e poi la loro determinizzazione, un passo notoriamente difficile. LTLf+ mantiene i vantaggi di LTLf, inclusa la rappresentazione canonica minima e la determinizzazione efficiente per automi finiti su parole finite. La traduzione normalizza la specifica LTL e la converte in LTLf+, consentendo un ragionamento più efficiente. Il lavoro è disponibile su arXiv con identificativo 2608.02454.