The translation from temporal logics to automata is the workhorse algorithm of several techniques in computer science and AI, such as reactive synthesis, reasoning about actions, FOND planning with temporal specifications, and reinforcement learning with non-Markovian rewards, just to name a few. Unfortunately, the problem is computationally intractable, requiring the implementation of several heuris- tics to make it usable in practice. In this paper, following the recent interest in temporal logic formalisms over finite traces, we present a compositional approach for dealing with translations of Linear Temporal Logic and Linear Dynamic Logic (LDLf) on finite traces into Deterministic Finite Automata DFA.That is, we inductively transform each LTLf/LDLf subformula into a DFA, and combine them through automata operators. By relying on efficient semi-symbolic automata rep- resentations, we empirically show the effectiveness of our ap- proach and the competitiveness with similar tools. Moreover, this is the first work that provides a scalable and practical tool supporting the translation to DFA not only for LTLf but also for full LDLf .

Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata / De Giacomo, Giuseppe; Favorito, Marco. - (2021), pp. 122-130. ((Intervento presentato al convegno Thirty-First International Conference on Automated Planning and Scheduling, ICAPS 2021 tenutosi a Guangzhou, China.

Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata

Giuseppe De Giacomo;Marco Favorito
2021

Abstract

The translation from temporal logics to automata is the workhorse algorithm of several techniques in computer science and AI, such as reactive synthesis, reasoning about actions, FOND planning with temporal specifications, and reinforcement learning with non-Markovian rewards, just to name a few. Unfortunately, the problem is computationally intractable, requiring the implementation of several heuris- tics to make it usable in practice. In this paper, following the recent interest in temporal logic formalisms over finite traces, we present a compositional approach for dealing with translations of Linear Temporal Logic and Linear Dynamic Logic (LDLf) on finite traces into Deterministic Finite Automata DFA.That is, we inductively transform each LTLf/LDLf subformula into a DFA, and combine them through automata operators. By relying on efficient semi-symbolic automata rep- resentations, we empirically show the effectiveness of our ap- proach and the competitiveness with similar tools. Moreover, this is the first work that provides a scalable and practical tool supporting the translation to DFA not only for LTLf but also for full LDLf .
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/1575288
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? ND
social impact