Trace Alignment is a prominent problem in Declarative Process Mining, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in DECLARE, a strict sublanguage of linear-time temporal logic over finite traces (LTLf). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf. In this paper, we study the timed version of trace alignment, where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf), essentially a superlanguage of LTLf. Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for a more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution of the paper is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.

Timed Trace Alignment with Metric Temporal Logic over Finite Traces / De Giacomo, G.; Murano, A.; Patrizi, F.; Perelli, G.. - (2021), pp. 227-236. (Intervento presentato al convegno 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021 nel 2021) [10.24963/kr.2021/22].

Timed Trace Alignment with Metric Temporal Logic over Finite Traces

De Giacomo G.;Murano A.;Perelli G.
2021

Abstract

Trace Alignment is a prominent problem in Declarative Process Mining, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in DECLARE, a strict sublanguage of linear-time temporal logic over finite traces (LTLf). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf. In this paper, we study the timed version of trace alignment, where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf), essentially a superlanguage of LTLf. Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for a more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution of the paper is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.
2021
978-1-956792-99-7
Timed Trace Alignment with Metric Temporal Logic over Finite Traces / De Giacomo, G.; Murano, A.; Patrizi, F.; Perelli, G.. - (2021), pp. 227-236. (Intervento presentato al convegno 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021 nel 2021) [10.24963/kr.2021/22].
File in 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/11588/880478
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact