Paper deep dive
Time to Reason: Scalable Neurosymbolic Learning for LTLf via Fuzzy Semantics
Riccardo Andreoni, Andrei Buliga, Alessandro Daniele, Paolo Felli, Chiara Ghidini, Marco Montali, Massimiliano Ronzani
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 8/23/2026, 2:09:27 AM
Summary
This paper introduces DiffLTLf, a neurosymbolic framework that integrates fuzzy semantics for Linear Temporal Logic on finite traces (LTLf) directly into deep learning architectures. Unlike previous approaches that rely on automata, DiffLTLf uses differentiable fuzzy interpretations (Gödel, Product, Łukasiewicz) to enable scalable and flexible learning under temporal constraints. The authors provide a theoretical analysis of these semantics and demonstrate that DiffLTLf achieves performance comparable to state-of-the-art probabilistic methods while significantly improving scalability.
Entities (10)
Relation Signals (6)
DiffLTLf → uses → Fuzzy Semantics
confidence 95% · DiffLTLf... enabling flexible and scalable learning without relying on the usage of automata... formally defining different fuzzy semantics for LTLf
Gödel semantics → preserves → Classical LTLf Equivalences
confidence 92% · classical ltlf equivalences between temporal operators are preserved in full only under the Gödel semantics
DiffLTLf → avoids → Automata
confidence 90% · enabling flexible and scalable learning without relying on the usage of automata
Weakly Supervised Symbol Grounding → solvedby → DiffLTLf
confidence 90% · In this task, a model must discover the symbolic meaning... supervised only by a binary label... The formal definition... and the proposed neurosymbolic framework, is presented in Sections 4 and 5
DiffLTLf → outperforms → Automata-based approaches
confidence 88% · DiffLTLf achieves performance on par with... state-of-the-art probabilistic approaches while substantially improving scalability
Product semantics → usedby → FuzzyA
confidence 85% · The former [FuzzyA] uses fuzzy automata under the Product semantics
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Neurosymbolic (NeSy) Artificial Intelligence aims to integrate Deep Learning (DL) architectures with symbolic reasoning. While initial NeSy approaches have targeted mainly symbolic reasoning in propositional and first-order logics, recent works have started to address the construction of neurosymbolic frameworks for Temporal Logics, and in particular for LTLf. These approaches have established temporal NeSy as a promising research direction, laying the foundations for learning under temporal constraints. Nonetheless, they leave many questions unanswered. From a theoretical perspective, several differentiable semantics for interpreting LTLf have been proposed but have not yet been formally and systematically defined within a unified framework. Moreover, existing approaches commonly rely on automata to represent temporal knowledge, resulting in limited scalability. Motivated by this research gap, this paper provides the following contributions: (i) formally defining different fuzzy semantics for LTLf, and systematically analysing theoretical properties regarding equivalences and dualities of temporal operators; (ii) showing how these semantics can be directly integrated within a novel NeSy framework, called DiffLTLf, enabling flexible and scalable learning without relying on the usage of automata; and (iii) introducing a novel evaluation protocol of increased complexity of learning tasks w.r.t. existing benchmarks. Our results show that the choice of fuzzy semantics has a significant impact on predictive performance. Moreover, DiffLTLf achieves performance on par with, and sometimes superior to, state-of-the-art probabilistic approaches while substantially improving scalability. Taken together, these results establish direct fuzzy interpretations as a competitive and scalable alternative to existing temporal NeSy frameworks.
Tags
Links
- Source: https://arxiv.org/abs/2608.16443v1
- Canonical: https://arxiv.org/abs/2608.16443v1
Trouble viewing inline? Open PDF directly →
Full Text
153,879 characters extracted from source content.
Expand or collapse full text
Time to Reason: Scalable Neurosymbolic Learning for LTLf via Fuzzy Semantics Journal: Artificial Intelligence Riccardo Andreoni Affiliation: Fondazione Bruno Kessler, Via Sommarive, 18, Trento, 38123, Italy Affiliation: Free University of Bozen-Bolzano, Via Bruno Buozzi, 1, Bolzano, 39100, Italy Andrei Buliga Affiliation: Fondazione Bruno Kessler, Via Sommarive, 18, Trento, 38123, Italy Alessandro Daniele Affiliation: Free University of Bozen-Bolzano, Via Bruno Buozzi, 1, Bolzano, 39100, Italy Paolo Felli Affiliation: Università di Bologna, Via Mura Anteo Zamboni 7, Bologna, 40126, Italy Chiara Ghidini Affiliation: Free University of Bozen-Bolzano, Via Bruno Buozzi, 1, Bolzano, 39100, Italy Marco Montali Affiliation: Free University of Bozen-Bolzano, Via Bruno Buozzi, 1, Bolzano, 39100, Italy Massimiliano Ronzani Affiliation: Fondazione Bruno Kessler, Via Sommarive, 18, Trento, 38123, Italy Abstract Neurosymbolic (NeSy) Artificial Intelligence aims to integrate Deep Learning (DL) architectures with symbolic reasoning. While initial NeSy approaches have targeted mainly symbolic reasoning in propositional and first-order logics, recent works have started to address the construction of neurosymbolic frameworks for Temporal Logics, and in particular for ltlf. These approaches have established temporal NeSy as a promising research direction, laying the foundations for learning under temporal constraints. Nonetheless, they leave many questions unanswered. From a theoretical perspective, several differentiable semantics for interpreting ltlf have been proposed but have not yet been formally and systematically defined within a unified framework. Moreover, existing approaches commonly rely on automata to represent temporal knowledge, resulting in limited scalability. Motivated by this research gap, this paper provides the following contributions: (i) formally defining different fuzzy semantics for ltlf, and systematically analysing theoretical properties regarding equivalences and dualities of temporal operators; (i) showing how these semantics can be directly integrated within a novel NeSy framework, called ∂ , enabling flexible and scalable learning without relying on the usage of automata; and (i) introducing a novel evaluation protocol of increased complexity of learning tasks w.r.t. existing benchmarks. Our results show that the choice of fuzzy semantics has a significant impact on predictive performance. Moreover, ∂ achieves performance on par with, and sometimes superior to, state-of-the-art probabilistic approaches while substantially improving scalability. Taken together, these results establish direct fuzzy interpretations as a competitive and scalable alternative to existing temporal NeSy frameworks. 1 Introduction Neurosymbolic (NeSy) Artificial Intelligence (AI) aims to integrate Deep Learning (DL) architectures with symbolic reasoning techniques [4]. This integration aims to combine the strengths of deep neural networks and symbolic AI while overcoming their respective weaknesses, addressing important problems related to data efficiency, fairness, trust, and safety of AI. A number of NeSy approaches have been proposed in recent years, differing both in the symbolic formalisms they adopt and in how symbolic knowledge is incorporated into gradient-based learning. Concerning the former, most of the efforts have been focused on propositional and first-order logics [23, 2]. Concerning the latter, end-to-end training is typically enabled by relaxing symbolic representations into numerical forms. As a result, different interpretations, including fuzzy and probabilistic semantics, have been explored to align symbolic reasoning with the learning dynamics of neural models [2, 12, 23, 33]. In the last few years the NeSy community has witnessed the emergence of a new series of works (see in particular [20, 29, 22, 1]) that aim to build neurosymbolic frameworks for Temporal Logics, and in particular for Linear time Temporal Logic (ltl) [25] and its variant ltlf on finite traces [9]. This is not surprising. In fact, ltl and ltlf are widely used across a range of domains—including formal methods [25], automated planning [8], AI-augmented process mining [10], and reinforcement learning [7]. These new temporal NeSy formalisms are characterised by the fact that learning must account for sequential data and time-dependent constraints. An important difference between these works concerns the way in which the temporal knowledge is incorporated within the framework. The works of Umili et al. 2023b and Manginas et al. 2025 rely on a finite-state machine (automata) transformation of the temporal formula that is used to define supervision signals over input sequences. The former uses fuzzy automata under the Product semantics, while the latter uses probabilistic automata. Instead, the work of Andreoni et al. 2025 interprets directly ltlf specifications through fuzzy logic under the Gödel semantics to guide the learning process. This is to overcome the computational overhead required to (1) build the automaton and (2) traverse it multiple times during the training procedure. These works have a great merit, as they have extended NeSy frameworks to reference logics for dynamic domains. Nonetheless, they are still first, and somehow preliminary, proposals towards the solid definition of temporal NeSy frameworks. From the description above it is easy to see that they all exploit different differentiable semantics to interpret classical ltl, and none of them takes into account the problem of investigating the impact that this choice has, both in terms of the relationship between the differentiable semantics and the classical one, and in terms of performances. This is a crucial aspect, especially for formalisms based on fuzzy logics, as prior work on propositional logics shows that the choice of fuzzy semantics can significantly affect the predictive performance within NeSy frameworks [17]. A second important merit of the works above is to have identified a clear task for the evaluation of these methods, that is weakly supervised symbol grounding (see Section 2.1). Nonetheless, the works mentioned above provide limited attention to the issue of scalability. While this is understandable, as they are the first works in the field, scalability is an important property that needs to be considered and investigated when developing a NeSy framework. Related to this, Lorello et al. 2025 recently proposed a benchmark for this task. However, it applies only to NeSy methods that compile temporal knowledge into automata, which hampers the assessment of systems relying on alternative integration approaches. This work has the aim to overcome the limitations listed above: (i) generalizing the work of Donadello et al. 2025, we provide a systematic study of fuzzy semantics in temporal NeSy learning, where we show that the classical ltlf equivalences between temporal operators are preserved in full only under the Gödel semantics, whereas under Product and Łukasiewicz some operators lose their interdefinability and require a native definition; (i) we show how different fuzzy semantics can be directly integrated within a novel NeSy framework, called ∂ , enabling flexible learning without having to rely on the usage of automata; (i) we take inspiration from Lorello et al. 2025 and introduce an extensive evaluation protocol for temporal NeSy, that works for both automata-based and automata-free frameworks. To start addressing the problem of scalability, we increase the complexity of learning scenarios w.r.t. [20]. The evaluation shows that: (1) different fuzzy semantics affect predictive performance, and (2) the direct fuzzy interpretations of ∂ overall achieve comparative performance with the state-of-the-art method proposed in [22] while significantly increasing scalability, thus confirming trends already exposed for first-order logics [21] where probabilistic approaches tend to improve predictive performance, while fuzzy logics tend to increase computational efficiency. Besides this particular work, and the proposal of ∂ , we believe that the systematic theoretical investigation of fuzzy ltlf in Section 4, and the novel evaluation setting provided in Section 6 can provide a solid contribution to the development of future temporal NeSy frameworks, thus contributing to the consolidation of this field. The paper is structured as follows. In Section 2 we summarise the required preliminaries and background material; in Section 3 we illustrate the state of the art in temporal NeSy, including available benchmarks, focusing on the most relevant approaches against which our experimental evaluation is carried out; in Section 4 we introduce our fuzzy variant of the ltlf temporal logic, formalising and studying three distinct semantics; in Section 5 we illustrate the overall ∂ framework and formally state the NeSy task at hand; in Section 6 we formulate critical research questions and carry out experimental evaluation, comparing ∂ against the existing approaches in the literature that were already identified; in Section 7 we present the results of our evaluation with respect to the research questions that were formulated; in Section 8 we underline some limitations of the current study. Conclusions are summarised in Section 9, and some technical implementation details and ancillary experimental results are given in appendix. The ∂ implementation and the experiments are available at github.com/andreoniriccardo/DiffLTLf. 2 Background In this section we revise the background notions needed in the paper. We start by introducing the task of weakly supervised symbol grounding which we aim to solve with the proposed ∂ . We continue by revising the definitions of Linear Time Temporal logic both in its classical setting and in the setting of finite traces. For the sake of readability we have decided to omit a separate background section on propositional fuzzy logics. Instead, we introduce the key notions of fuzzy logics when they are needed in defining the fuzzy ltlf variants in Section 4. 2.1 Weakly Supervised Symbol Grounding under Distant Temporal Supervision In this section, we revise the weakly supervised symbol grounding under distant temporal supervision problem addressed by previous temporal neurosymbolic frameworks [20, 29, 22, 1]. In this task, a model must discover the symbolic meaning of visual observations from sequences, supervised only by a binary label for each sequence, where the label expresses compliance with a temporal specification. The setting is as follows: a model observes sequences of images, where each image represents one of a finite set of categories unknown to the model. Each sequence is annotated with a single binary label indicating whether the sequence, interpreted at the symbolic level, satisfies or violates a given temporal specification (i.e., a rule that constrains the admissible ordering of symbols over time). Crucially, the model has no access to the category of the individual images: it is never told which category any particular image belongs to. The learning objective is to train a perception model that maps each raw image to a symbolic category, using only the sequence-level compliance label as supervision. Figure 1: Illustrative example of the weakly supervised learning task on a simplified manufacturing scenario. Left: correct perception leads to a correct assessment of non-compliance, matching the ground-truth label. Right: incorrect perception leads to a wrong assessment of compliance, producing a corrective learning signal. Figure 1 illustrates the task’s learning process on a simplified manufacturing example. This example involves four possible activities: cutting, welding, inspecting, and packaging. Moreover, the scenario at hand is subject to the temporal specification “do not package until inspection has been completed’. Both sides of the figure show the same input sequence, which violates this rule. On the left hand side, the perception module correctly recognises each image, resulting in a correct classification of the sequence as non-compliant. On the right hand side, the perception module misclassifies some images, resulting in an incorrect classification of the sequence as compliant. The mismatch with the ground-truth label produces a large loss, and the resulting learning signal pushes the perception module to correct its predictions (red arrow). In both cases, the model receives only the binary compliance label, and the symbolic category of the individual images is never provided. This example serves as a high-level illustration of the learning problem; the scenario and the images in Figure 1 are not part of the experimental evaluation. The formal definition of the task, including the temporal specification language and the proposed neurosymbolic framework, is presented in Sections 4 and 5 respectively. The experimental evaluation is detailed in Section 6. 2.2 Linear Temporal Logic on Finite Traces Linear-time logics, that is, temporal logics predicating on traces, provide the most natural choice to express symbolic knowledge in our setting. Traditionally, traces are assumed to have an infinite length, as witnessed by Linear Temporal Logic (ltl) [25]. In several application domains, such as planning and process mining, the dynamics of the system are more naturally captured using unbounded, but finite, traces [8]. This led to ltl on finite traces (ltlf) [9]. An ltlf formula φ over a finite set P of propositional symbols follows the grammar [9]: φ::=p∣¬φ∣φ∨φ∣φ∣φφ ::=p X U where p∈p . The semantics of these formulae is defined over finite traces, usually formalised as non-empty sequences λ=⟨A1,A2…,An⟩λ= A_1,A_2…,A_n where each Ai∈2A_i∈ 2^P for i>0i>0 is the set of propositional symbols that are true at instant i, namely is a propositional assignment over P. For uniformity with the fuzzy setting discussed later, and in particular with the definition of traces used in Section 4, we adopt a functional, equivalent definition, where a trace is represented as a non-empty series of instants, each mapping every propositional symbol from P to either 00 (for false) or 11 (for true). Definition 1. A trace of length n is a non-empty vector λ=⟨λ0,…,λn−1⟩λ= _0,…, _n-1 of functions in which, for each instant i=0,…,n−1i=0,…,n-1, the i-th function λi:P↦0,1 _i:P \0,1\ assigns a truth value to each symbol p∈p . Given i∈0,…,n−1i∈\0,…,n-1\ and p∈Pp∈ P, λi(p) _i(p) is equivalently denoted by λ(p,i)λ(p,i). Notably, in this paper we consider only non-empty traces of finite length, and denote the last instant of a trace λ of length n by last(λ)=n−1last(λ)=n-1. i=0i=0 i=1i=1 i=2i=2 i=3i=3 i=4i=4 1 1 0 1 1 0 0 1 1 0 λ 1 1 1 1 0 0 1 1 0 0 aba Ubb Xb Figure 2: Graphical depiction of an ltlf trace of length 5, and satisfaction of the two formulae aba Ub and b Xb in every instant of the trace. Example 1. Figure 2 (top) graphically depicts an ltlf trace λ of length 5 defined over =a,bP=\a,b\. We have last(λ)=4last(λ)=4. Also, λ(,0)=1λ( a,0)=1 is the truth value associated to symbol a at instant 00 (the beginning of the trace), while λ(,1)=1λ( a,1)=1 is the value of a in the following instant. The grammar above extends propositional logic on P with formulae employing the temporal operators X and U, respectively representing (strong) next and (strong) until. Intuitively, when evaluated in an instant of the trace: φ X states that there exists a next instant, and φ holds therein; φ1φ2 _1 U _2 states that φ2 _2 holds in the current or a later instant, and in all instants in between, φ1 _1 holds. Formally, for an ltlf formula φ , a trace λ, and an instant i∈0,…,last(λ)i∈\0,…,last(λ)\, we inductively define that φ is true in instant i of λ, written λ,i⊧φλ,i , as [9]: λ,i⊧p∈if λ(p,i)=1λ,i⊧¬φifλ,i⊧̸φλ,i⊧φ1∨φ2ifλ,i⊧φ1 or λ,i⊧φ2λ,i⊧φifi<last(λ) and λ,i+1⊧φλ,i⊧φ1φ2if λ,j⊧φ2 for some j s.t. i≤j≤last(λ) and λ,k⊧φ1 for every k s.t. i≤k<j array[]l l lλ,i p &if\;\;&λ(p,i)=1\\ λ,i &if&λ,i \\ λ,i _1 _2&if&λ,i _1 or λ,i _2\\ λ,i X &if&i<last(λ) and λ,i+1 \\ λ,i _1 U _2&if &λ,j _2 for some j s.t.~i≤ j≤ last(λ) and \\ && λ,k _1 for every k s.t.~i≤ k<j array We say that λ satisfies φ , written λ⊧φλ , if λ,0⊧φλ,0 . Example 2. Figure 2 (bottom) graphically depicts, instant by instant, the truth values of the two ltlf formulae aba Ub and b Xb, evaluated over the trace λ from Example 1 (and shown in the top part of the same figure). Formula b Xb essentially shifts of one instant ahead the truth values of b as assigned by λ, and is false in instant 4=last(λ)4=last(λ) since there is no next instant in λ. Formula aba Ub evaluates to false in instant 44: while the left-hand side holds therein, there is no later instant in λ where b holds. The formula instead evaluates to true in all other instants: in instants 22 and 33 because the right-hand side holds, and in instants 00 and 11 because the left-hand side holds there and in later instants until, in instant 33, the right-hand side holds. The truth values at instant 00 indicate the overall verdict for the entire trace: λ⊧abλ a Ub, and λ⊧̸bλ Xb. The syntax and semantics of the other standard boolean connectives ⊤ , ⊥ , ∧ , → → are derived as usual. Further key temporal operators are derived from X and U as follows. • weak next (w X_w): wφ≡φ∨¬⊤ X_w ≡ X X , capturing that if there is a next instant, then φ holds therein; • release ( R): φ1φ2≡¬(¬φ1¬φ2) _1 R _2≡ ( _1 U _2), capturing that φ2 _2 holds until, and including the moment, where φ1 _1 holds (if this condition never occurs, then φ2 _2 holds throughout the entire trace); • globally ( G): φ≡⊥φ G ≡ R , capturing that φ holds throughout the entire trace; • eventually ( F): φ≡⊤φ F ≡ U , capturing that φ holds at some instant in the trace. • strong release ( M): φψ≡φψ∧φ Mψ≡ Rψ F , capturing a stronger form of release where φ holds at some point. • weak until ( W): φψ≡φψ∨φ Wψ≡ Uψ G , capturing a weaker form of until where ψ is not required to hold at some point and, in that case, φ must globally hold. The process mining community has selected a number of patterns of ltlf formulas that are particularly significant for describing business processes in a declarative manner. These patterns constitute the declare modelling language [10]. Examples of declare patterns are provided in Table 1 together with their ltlf formalisation and intuitive meaning. Following [29, 1, 28], we use declare formulae in the evaluation of our approach in Section 6. Table 1: declare pattern templates used in the benchmark. A and B denote stream-specific propositions or Boolean combinations of them. declare Pattern ltlf Template Description Response (A→B) G(A→ F\,B) If A occurs, B must eventually follow Not Succession (A→¬B) G(A→ F\,B) If A occurs, B must never follow Chain Succession (A→B) G(A→ X\,B) If A occurs, B must hold at the next timestep Not Chain Succession (A→¬B) G(A→ X\,B) If A occurs, B must not hold at the next timestep Precedence (¬BA)∨(¬B)( B\; U\;A) G( B) B cannot occur before A has occurred Chain Precedence (B→A) G( X\,B→ A) Every occurrence of B is immediately preceded by A Responded Existence A→B F\,A→ F\,B If A occurs at some point, B must also occur Not Co-existence A→¬B F\,A→ F\,B A and B cannot both occur in the sequence 3 State of the Art in Temporal NeSy The majority of works in the NeSy community focus on static, relational domains [4]. Nonetheless recent efforts have started proposing solutions for NeSy learning over temporal domains, dealing with different types of formalisms, architectures, and evaluation protocols. In this section, we describe the main existing frameworks with the goal of highlighting their contributions and their limitations. The limitations illustrated here motivate our overall work and the definition of ∂ . The works we take into account here are FuzzyA [29]11 1 Umili et al. 2023b do not introduce a name for their system. We use here the same name used by Manginas et al. 2025 to refer to the system in [29]., NeSyA [22], T-ILR [1], and the LTLZinc benchmark [20]. We focus on these papers because they provide the most recent and impactful contributions.22 2 Early work that combine temporal logics and neural systems operate on symbolic inputs, assuming propositional truth values rather than grounding them in perceptual data. They then compile temporal (and epistemic) logics into the architecture and weights of neural networks for logical deduction or runtime monitoring [15, 24]. Another, more recent, work [11] exploits ltlf for suffix prediction under ltlf constraints but does not rely on the direct, differentiable integration of temporal logic into NeSy architectures. For these reasons, they are not analysed in this section. The works of Umili et al. 2023a and Umili et al. 2024, which address the tasks of non-Markovian reinforcement learning and suffix prediction under ltlf constraints, respectively, are instead not analysed here as they follow the same conceptual approach of FuzzyA [29]. We first review the three frameworks of FuzzyA [29], NeSyA [22], and T-ILR [1], and we conclude the section with the LTLZinc benchmark [20]. 3.1 NeSy Frameworks for Temporal Logic A first important observation is that all these recent efforts focus on a particular variant of Temporal Logics, that is, Linear time Temporal Logics on finite traces (ltlf). Having said so, they solve the task of Weakly Supervised Symbol Grounding under Distant Temporal Supervision in different manners. We can make explicit these differences along two main dimensions: (i) how the temporal knowledge is integrated into the learning process, and (i) which differentiable semantics is used to interpret the temporal formula. Let us explore these two dimensions one by one. Integration of Knowledge Concerning the way in which temporal knowledge is integrated into the learning process, the dominant approach compiles the ltlf specification into a deterministic finite-state automaton (DFA), which is then evaluated in a differentiable manner over the perception outputs. The two most representative instances of this approach are FuzzyA [29] and NeSyA [22]. In these frameworks, at each timestep, a neural perception module produces soft truth values for the atomic propositions, which are used to evaluate the automaton’s transition guards. The guard values then update the truth values associated with each automaton state, recursively from the first to the last instant of the sequence. The explicit construction of a finite-state automaton from the ltlf formula originates two distinct limitations: first, the automaton must be built before training, and its size is, in the worst case, double-exponential in the size of the ltlf formula [9]. Second, during training the evaluation of the state of the automaton is computed recurrently over the sequence, each timestep depending on the previous one, so the evaluation is inherently sequential, preventing parallelisation over time. To overcome these limitations, T-ILR [1] operates directly on the logical structure of the formula, foregoing the need for an intermediate DFA-based representation. In particular, T-ILR proposes a differentiable framework in which ltlf formulas are evaluated through fuzzy semantics without compiling them into an intermediate automaton. This allows the model to compute a degree of satisfaction directly from the neural outputs, while still enabling gradient-based optimization. In this work we follow the approach of T-ILR, and base our proposal ∂ on this latter approach of evaluating directly ltlf formulas through a differentiable semantics without compiling them into an intermediate automaton. Differentiable Semantics Concerning the differentiable semantics used to interpret the temporal formula, we can observe a heterogeneous situation. In fact, FuzzyA, T-ILR, and NeSyA adopt three different semantics. More in detail, FuzzyA adopts a fuzzy interpretation of the automaton, and exploits the Product semantics for the fuzzy connectives. The authors of FuzzyA claim to be inspired, in their work, by Logic Tensor Networks [2], and the choice of Product semantics appears to be grounded on this inspiration. Similarly to FuzzyA, T-ILR chooses to rely on a fuzzy approach, but opts for the Gödel semantics. This choice is justified in terms of the theoretical investigation of fuzzy ltlf provided in Donadello et al. 2025. Finally, NeSyA replaces fuzzy semantics with probabilistic reasoning. The probabilistic semantics is exact and avoids the approximation introduced by fuzzy evaluations. It comes, however, at a computational cost, as exact probabilistic inference requires solving a Weighted Model Counting (WMC) problem.33 3 In practice, WMC is often evaluated through compiled probabilistic circuits rather than explicit model enumeration, which can enable efficient inference when compact compiled representations are available. The divide between probabilistic and fuzzy approaches is something to be expected, and mimics what has happened for the more established NeSy frameworks for static, relational domains, that is, domains where knowledge is formalised using propositional or first-order logics. Nonetheless, we can observe a lack of systematic investigation of the choices one has and of the impact of these choices on the resulting framework. This is a crucial limitation both for formalisms based on fuzzy logics, and for the choice between probabilistic and fuzzy logics. In fact, prior work on NeSy frameworks for Propositional and First Order Logics shows that the choice of fuzzy semantics can significantly affect the predictive performance within NeSy frameworks [17], and a trade off exists between probabilistic and fuzzy approaches, where probabilistic approaches tend to improve the predictive performance, while fuzzy logics tend to improve (that is, decrease) the computational cost. In this work, we aim for scalability and therefore opt for the fuzzy approach. Nonetheless we do it in a principled manner, first by providing theoretical investigation of different fuzzy semantics for ltlf obtained using different t-norms, and then by defining ∂ as a semantics-agnostic, fuzzy framework for temporal data where one can opt for different fuzzy semantics. Moreover, we aim at providing a first comprehensive and systematic evaluation of the different fuzzy and probabilistic semantics in terms of predictive performance and computational cost, thus obtaining systematic insights on the impact that the different differentiable semantics can have on the task. 3.2 Temporal NeSy benchmarks It is worth noting that, despite their architectural differences, the state-of-the-art methods described above are all evaluated on the task introduced in Section 2.1, where supervision is provided only at the sequence level. A recent benchmark related to this task is that of LTLZinc [20], which targets sequence classification under temporal specifications. While the proposal of a benchmark is extremely important in building a solid research community, we can observe several limitations in this work when we aim to use it for comparing the different aspects of temporal NeSy methods under purely distant supervision. First, its specifications interleave temporal operators with relational constraints, so that the contribution of the temporal reasoning component is not isolated. Second, it introduces intermediate supervision signals at several levels of the pipeline, together with a supervised pre-training of the perception module. While this facilitates training, it makes the benchmark less suitable for assessing how methods perform in more challenging (and possibly more realistic) scenarios when only distant supervision is available. Third, it relies on the supervision on the next state in the finite-state machine. This makes it applicable only to automata-based methods, excluding approaches that evaluate the temporal specification directly. These limitations motivate the evaluation protocol we introduce in Section 6, which relies only on the sequence-level label and applies to both automata-based and automata-free methods. Moreover, our evaluation setting disentangles two distinct critical aspects that affect scalability, by varying the size of the temporal specification and the length of the input sequences in a separate manner. 4 Fuzzy LTLF In this section we introduce the syntax and the semantics of the temporal fuzzy logic that we use to formalise specifications. To define the semantics, as customary for t-norm fuzzy logics, one has to choose how to evaluate the logical connectives, namely conjunction, disjunction, negation and implication, as this is not fixed univocally. Instead of committing to a specific choice of evaluation, in this work we consider three alternatives, in turn obtaining three fuzzy variants of ltlf, which we term fltlGf_f^G, fltlPf_f^P, and fltlLf_f^L. fltlGf_f^G corresponds to the logic previously introduced in [13], that is, fuzzy ltlf with the Gödel semantics; fltlPf_f^P and fltlLf_f^L adopt, respectively, a variant of the Product semantics and the Łukasiewicz semantics. For convenience of presentation, we denote this family of logics as fltlxf_f^x. The remainder of this section is organised as follows: in Section 4.1 we provide the syntax and semantics of the three logics, focussing on the core temporal operators X (next) and U (until). In Section 4.2 we consider additional temporal operators that are well known in the literature on temporal logic, and that in the boolean case are derivable from X and U. In particular, we investigate whether the equivalences known to hold for ltlf hold for our case as well. We show that, irrespective of the semantics chosen, some of these operators can be defined from the two fundamental temporal operators X and U introduced in Section 4.1, while others cannot be derived as abbreviations, and thus their semantics needs to be defined natively. 4.1 fltlxf_f^x Syntax and Semantics The logics we consider are finite-trace variants of the known Fuzzy Linear-time Temporal Logic (fltl) [18, 14] that is interpreted over finite traces, and thus can be seen as fuzzy counterparts of ltlf (see Section 2.2 for preliminaries on ltlf). Given a finite set P of propositional symbols, an fltlxf_f^x formula φ is written according to the following grammar: φ:=⊤|⊥|p|¬φ|φ∧φ|φ∨φ|φ→φ|φ|φφ := ~|~ ~|~p~|~ ~|~ ~|~ ~|~ → ~|~ X ~|~ U where p∈p , the symbols ⊤ and ⊥ are the true and false constants, respectively, and ¬ , ∧ , ∨ , → are fuzzy connectives for negation, conjunction, disjunction, implication. As in ltlf, the fundamental temporal operators are X (next) and U (until). The semantics of these formulae is defined again over finite traces over propositional symbols P. However, whereas the sequences in Section 2.2 assigned only crisp values, namely either 00 or 11, the traces used for fltlxf_f^x are non-empty sequences of instants in which a real value in the interval [0,1][0,1] is assigned to each propositional symbol p∈p , representing the degree of truth of p at each instant. Definition 2. A trace of length n is a vector λ=⟨λ0,…,λn−1⟩λ= _0,…, _n-1 of functions in which, for each instant i=0,…,n−1i=0,…,n-1, the i-th function λi:P↦[0,1] _i:P [0,1] assigns to each symbol p∈p a real value. For brevity, we denote by λ(p,i)λ(p,i) the value associated to p at instant i, namely λi(p) _i(p). Moreover, in Section 5 and following we write λ(p)=⟨p0,p1,…,pn−1⟩λ(p)= p_0,p_1,…,p_n-1 to denote the sequence of all values of p along the trace, namely the sequence of values pi=λ(p,i)p_i=λ(p,i). We restrict to non-empty traces of finite length, thus continue to denote the last instant of a trace λ of length n by last(λ)=n−1last(λ)=n-1. As a consequence, differently from ltlf, the evaluation of an fltlxf_f^x formula φ over a trace λ at instant i≥0i≥ 0, denoted by v(φ,λ,i)v( ,λ,i), returns a real value in [0,1][0,1] rather than necessarily a boolean value in 0,1\0,1\. This is defined below, where p∈p and φ1,φ2 _1, _2 are fltlxf_f^x formulae: v(⊤,λ,i)=1 and v(⊥,λ,i)=0;v(p,λ,i)=λ(p,i);v(¬φ,λ,i)=⊖v(φ,λ,i);v(φ1∧φ2,λ,i)=v(φ1,λ,i)⊗v(φ2,λ,i);v(φ1∨φ2,λ,i)=v(φ1,λ,i)⊕v(φ2,λ,i);v(φ1→φ2,λ,i)=v(φ1,λ,i) ○ →v(φ2,λ,i);v(φ,λ,i)=v(φ,λ,i+1) if i<last(λ), 0 otherwise;v(φ1φ2,λ,i)=v(φ2,λ,i)⊕(v(φ1,λ,i)⊗v((φ1φ2),λ,i)). array[]r c lv( ,λ,i)&=&1 and v( ,λ,i)=0;\\ v(p,λ,i)&=&λ(p,i);\\ v( ,λ,i)&=& v( ,λ,i);\\ v( _1 _2,λ,i)&=&v( _1,λ,i)~ ~v( _2,λ,i);\\ v( _1 _2,λ,i)&=&v( _1,λ,i)~ ~v( _2,λ,i);\\ v( _1→ _2,λ,i)&=&v( _1,λ,i)~ # 0.78$ $ 0.43057pt$ 0.5mu →$ ~v( _2,λ,i);\\ v( X ,λ,i)&=&v( ,λ,i+1) if i<last(λ), 0 otherwise;\\ v( _1 U _2,λ,i)&=&v( _2,λ,i)~ ~(v( _1,λ,i)~ ~v( X( _1 U _2),λ,i)). array where ⊗ , ⊕ , ⊖ , ○ → # 0.78$ $ 0.43057pt$ 0.5mu →$ are the chosen t-norm, t-conorm (or s-norm), negation function and implication function, respectively. As discussed in the remainder of this paper, this is indeed one crucial distinction between ltlf and this fuzzy logic: the semantics of propositional connectives is explicitly given. It is also worth noting that the semantics of U (until) is here given using the alternative, equivalent recursive formulation based on the expansion law for the until operator [3], which in the propositional setting has the form φ1φ2=φ2∨(φ1∧(φ1φ2)) _1 U _2= _2 ( _1 X( _1 U _2)). This makes explicit the role of the chosen t-norm (conjunction) and t-conorm (disjunction) in its semantics and thus in the evaluation. We say that an fltlxf_f^x formula φ has value k in a trace λ at instant i≥0i≥ 0 iff v(φ,λ,i)=kv( ,λ,i)=k. Similarly, we say that φ has value k in λ iff v(φ,λ,0)=kv( ,λ,0)=k, also written v(φ,λ)=kv( ,λ)=k. Finally, we say that two fltlxf_f^x formulae φ1,φ2 _1, _2 are equivalent, written φ1≡φ2 _1≡ _2, if and only if they have the same value in every possible trace. Intuitively, the value of a propositional symbol p∈p at instant i is simply the value assigned to p by the trace, while boolean connectives are computed according to the chosen t-norm, t-conorm, negation and implication functions. A formula of the form φ X is evaluated at i on the next instant i+1i+1 of the trace, and if this does not exist, then the value is 00. Instead, φ1φ2 _1 U _2 expresses that φ2 _2 eventually contributes positively to the value of the entire formula which is until then supported by the value of φ1 _1. However, as customary for t-norm fuzzy logics, it is evident that the precise semantics depends on the choice of connectives, which is not fixed univocally. We consider the following three distinct semantics, thus a family of three resulting logics. fltlGf_f^G: Gödel semantics We fix the interpretation for the generic connectives in the semantics above to match the standard Zadeh logic. Namely, for any values α,β∈[0,1]α,β∈[0,1]: • α⊗β=minα,βα β= \α,β\ • α⊕β=maxα,βα β= \α,β\ • ⊖α=1−α α=1-α • α ○ →β=(⊖α)⊕βα # 0.78$ $ 0.43057pt$ 0.5mu →$ β=( α) β i=0i=0 i=1i=1 i=2i=2 0.5 0.9 0.2 0.2 0.3 0.8 λ v(ab,0)=v(b,0)⊕(v(a,0)⊗v((ab),0)) @inpgf@ignorespaces @inpgf@ignorespaces $ Goldenrod$v(a Ub,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Goldenrod$v(a Ub,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Goldenrod$v(a Ub,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Goldenrod$v(a Ub,0)$$= @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,0)$$ ( @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v( X(a Ub),0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v( X(a Ub),0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v( X(a Ub),0)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v( X(a Ub),0)$$) v(ab,1)=v(b,1)⊕(v(a,1)⊗v((ab),1)) @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v(a Ub,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v(a Ub,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v(a Ub,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ Dandelion$v(a Ub,1)$$= @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,1)$$ ( @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v( X(a Ub),1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v( X(a Ub),1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v( X(a Ub),1)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v( X(a Ub),1)$$) v(ab,2)=v(b,2)⊕(v(a,2)⊗v((ab),2)) @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v(a Ub,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v(a Ub,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v(a Ub,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ BurntOrange$v(a Ub,2)$$= @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(b,2)$$ ( @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v(a,2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v( X(a Ub),2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v( X(a Ub),2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v( X(a Ub),2)$$ @inpgf@ignorespaces @inpgf@ignorespaces $ gray!50$v( X(a Ub),2)$$) max \ 0.2 ,min, \ 0.5 , 0.8 =\\= 0.5 max \ 0.3 ,min, \ 0.9 , 0.8 =\\= 0.8 max \ 0.8 ,min, \ 0.2 , 0 =\\= 0.8 =v(b,2)=v(b,2) 0.2 + (0.5 ⋅· 0.8) - 0.2 ⋅· (0.5 ⋅· 0.8) == 0.52 0.3 + (0.9 ⋅· 0.8) - 0.3 ⋅· (0.9 ⋅· 0.8) ≃ 0.8 (0.8+0.2⋅0)−0.8⋅(0.2⋅0)=(0.8+0.2· 0)-0.8·(0.2· 0)= 0.8 =v(b,2)=v(b,2) min \ 1, 0.2 + max \ 0, 0.5+1-1=\\= 0.7 min \ 1, 0.3 + max \ 0, 0.9+0.8-1=\\= 1 min \ 1,0.8 + max \0,0.2+0-1=\\= 0.8 =v(b,2)=v(b,2) aba Ub GPL Figure 3: Graphical depiction of a fltlxf_f^x trace of length 3, and satisfaction of the formula aba Ub in every instant of the trace, under all three semantics. This logic matches the one considered in [13]. Intuitively, the t-norm preserves the intuitive behavior of the conjunction so that its value depends on the weakest evidence of truth, while the t-conorm preserves the intuitive behavior of disjunction and thus selects the strongest evidence. The remaining connectives correspond to classical negation and the fuzzy counterpart of material implication. fltlPf_f^P: Product semantics, with standard negation This semantics regards truth values as akin to probabilistic information, namely, conjunction progressively weakens the value of truth evidence by multiplicative accumulation, while disjunction accounts for independent evidences. The values for conjunction and disjunction, therefore, behave as the probability of the intersection and union of independent events, respectively: • α⊗β=α⋅βα β=α·β • α⊕β=α+β−α⋅βα β=α+β-α·β • ⊖α=1−α α=1-α • α ○ →β=(⊖α)⊕βα # 0.78$ $ 0.43057pt$ 0.5mu →$ β=( α) β fltlLf_f^L: Łukasiewicz semantics This semantics captures the notion that the truth value can be treated as a limited additive quantity, so by disjunction evidence of truth accumulates additively until a maximum, whereas by conjunction they combine additively but can compensate for each other until a point, so that an insufficient total value collapses to zero: • α⊗β=max0,α+β−1α β= \0,α+β-1\ • α⊕β=min1,α+βα β= \1,α+β\ • ⊖α=1−α α=1-α • α ○ →β=(⊖α)⊕βα # 0.78$ $ 0.43057pt$ 0.5mu →$ β=( α) β To see how the choice of semantics affects the meaning and evaluation of formulas, consider again a formula of the form ϕψφ Uψ evaluated at instant 00. Its value results in general from the contribution of multiple possible choices of the instant j at which the temporal eventuality is realised, namely at which the value v(ψ,λ,j)v(ψ,λ,j) is taken together with the support provided by each v(ϕ,λ,i)v(φ,λ,i) until then for 0≤i<j0≤ i<j. The recursive semantics at each instant combines three ingredients: 1. the value associated with the immediate realization of the eventuality (i.e., the value of ψ); 2. the value of (ϕψ) X(φ Uψ) associated with all the deferred realizations; 3. the local support to these deferred realizations (i.e., the value of ϕφ). Operationally, this occurs in two distinct steps, proceeding backwards, as illustrated in Figure 3. The t-norm ⊗ updates the value of deferred realizations by combining it with their local support given by ϕφ. Instead, the t-conorm ⊕ combines the so-obtained value with the value of ψ (i.e., the value of the immediate realization). In fltlGf_f^G, the t-norm selects the minimum between local support v(ϕ,λ,i)v(φ,λ,i) and the value of deferred realizations, so only one of these is considered. For instance, in the evaluation illustrated in Figure 3 for formula aba Ub, at instant 11 this is value minv(a,λ,1),v(ab,λ,2)=0.8 \v(a,λ,1),v(a Ub,λ,2)\=0.8. Then, the t-conorm selects the maximum, namely the best choice between immediate realization and possible deferred realizations. In Figure 3, for instant 11 this is the value maxv(b,λ,1),0.8=0.8 \v(b,λ,1),0.8\=0.8. As a result, the final value of the formula corresponds exactly to the choice of j such that minv(ϕ,λ,0),⋯,v(ϕ,λ,j−1),v(ψ,λ,j) \v(φ,λ,0),·s, v(φ,λ,j-1), v(ψ,λ,j)\ is maximal. In Figure 3, we indeed see that by selecting j=2j=2 we obtain the maximal value 0.50.5: for j=1j=1 and j=0j=0 the value of b is too low, while the local support given by the value of a is at least 0.50.5. So the final value is the minimum between 0.50.5 and the value of b at instant 22. This behavior fundamentally relies on the fact that the t-conorm is associative and monotonic. Even if the local support at any step supports many deferred realizations at once, these repeated support values do not compound. We can actually think of realizations (choices of j) as evaluated independently, selecting the best one. In fltlPf_f^P, the t-norm updates the value of deferred realizations by multiplying it with their local support v(ϕ,λ,i)v(φ,λ,i), which typically weakens it, so both contribute. Also, to combine the so-obtained value with v(ψ,λ,i)v(ψ,λ,i) for immediate realization, the t-conorm operates a probabilistic-style accumulation: again both contribute, but they are treated as independent events and their value discounted to account for overlaps. Thus, unlike fltlGf_f^G, all possible realizations (choices of j) contribute at once to the final value. In fltlLf_f^L, local support v(ϕ,λ,i)v(φ,λ,i) to deferred realizations is combined with their value by a t-norm that remains positive whenever the sum is greater than 11. This means that weaker support at earlier instants may be offset by stronger support at later instants that is propagated back (i.e., higher support of ϕφ until the eventuality is realised and a higher value of ψ later). The t-conorm combines the resulting value with v(ψ,λ,i)v(ψ,λ,i) for immediate realization additively (up to a value of 11), so the value may progressively strengthen. As for fltlPf_f^P, multiple possible realizations may contribute at once until saturation to 11. So for the same formula, the choice of semantics affects the value also because of how different ways of making the formula ‘true’ interact with each other. 4.2 Additional Temporal Operators In this section we consider additional temporal operators that are a fuzzy counterpart of well known ltlf temporal operators, namely F (eventually), G (always), w X_w (weak next), W (weak until), R (release), M (strong release). As we are going to show, while F, G, w X_w and R can be directly obtained as abbreviations from the base logic in the previous section, the W and M operators in general need to be explicitly defined, with the exception of the fltlGf_f^G case where they can also be derived. We first give below the explicit semantics for each of these. We extend fltlxf_f^x as follows: v(wφ,λ,i)=v(φ,λ,i+1) if i<last(λ), 1 otherwise;v(φ,λ,i)=v(φ,λ,i)⊕v(φ,λ,i);v(φ,λ,i)=v(φ,λ,i)⊗v(wφ,λ,i);v(φ1φ2,λ,i)=v(φ2,λ,i)⊕(v(φ1,λ,i)⊗v(w(φ1φ2),λ,i));v(φ1φ2,λ,i)=v(φ2,λ,i)⊗(v(φ1,λ,i)⊕v((φ1φ2),λ,i));v(φ1φ2,λ,i)=v(φ2,λ,i)⊗(v(φ1,λ,i)⊕v(w(φ1φ2),λ,i)). array[]r c lv( X_w ,λ,i)&=&v( ,λ,i+1) if i<last(λ), 1 otherwise;\\ v( F ,λ,i)&=&v( ,λ,i)~ ~v( X~ F ,λ,i);\\ v( G ,λ,i)&=&v( ,λ,i)~ ~v( X_w~ G ,λ,i);\\ v( _1 W _2,λ,i)&=&v( _2,λ,i)~ ~(v( _1,λ,i)~ ~v( X_w( _1 W _2),λ,i));\\ v( _1 M _2,λ,i)&=&v( _2,λ,i)~ ~(v( _1,λ,i)~ ~v( X( _1 M _2),λ,i));\\ v( _1 R _2,λ,i)&=&v( _2,λ,i)~ ~(v( _1,λ,i)~ ~v( X_w( _1 R _2),λ,i)).\\ array Intuitively, wφ X_w is analogous to φ X , although it does not require the next instant to exist (in which case, the value is trivially 11, i.e., maximally true). The value of φ F measures the evidence of φ being true at any point in the remaining portion of the trace, hence its value is obtained by combining the current and future values of φ using the t-conorm, to account for all possible ways in which the requirement can be satisfied. The value of φ G measures the evidence of φ being true in all instants in the remaining portion of the trace, so its value depends on the value of φ in the current instant and in each instant until the end. All these values are combined using the t-norm. The W operator is the weak counterpart of U: the value of φ1φ2 _1 W _2 depends on the support given by φ1 _1 until the value of φ2 _2 is positive, but a trace in which φ2 _2 has no positive value can still have a positive value. φ1φ2 _1 M _2 is used to express that eventually φ1 _1 has a positive value and up to (and including) that instant the support is given by the value of φ2 _2. Intuitively, after that point, the value of φ2 _2 is ‘released’ from providing support. R is the weak version of M, so there is no requirement on φ1 _1 having a positive eventually. In the propositions we establish next, we use the following convention: whenever the proposition is stated for fltlxf_f^x, this means that the proposition holds for all the three logics fltlGf_f^G, fltlPf_f^P, and fltlLf_f^L. As a preliminary step in our study of inter-definability of temporal operators, we recall two known results on the fuzzy logics we consider. First, the chosen combinations of t-norms, t-conorms and standard negation form so-called De Morgan triplets [16]. Second, the choice of min and max in this setting implies distributivity. As a direct application to our logics, we can state the following two propositions. Proposition 1. The De Morgan’s law holds for fltlxf_f^x. Namely in all these logics v(¬(φ1∧φ2),λ,i)=v(¬φ1∨¬φ2,λ,i)v( ( _1 _2),λ,i)=v( _1 _2,λ,i) and v(¬(φ1∨φ2),λ,i)=v(¬φ1∧¬φ2,λ,i)v( ( _1 _2),λ,i)=v( _1 _2,λ,i) for any λ and 0≤i≤last(λ)0≤ i≤ last(λ). Namely, ⊖(v(φ1,λ,i)⊗v(φ2,λ,i))=⊖v(φ1,λ,i)⊕(⊖v(φ2,λ,i)) (v( _1,λ,i) v( _2,λ,i))= v( _1,λ,i) ( v( _2,λ,i)) and ⊖(v(φ1,λ,i)⊕v(φ2,λ,i))=⊖v(φ1,λ,i)⊗(⊖v(φ2,λ,i)) (v( _1,λ,i) v( _2,λ,i))= v( _1,λ,i) ( v( _2,λ,i)). Proposition 2. In fltlGf_f^G, ⊗ and ⊕ coincide respectively with the meet and join operations of the totally ordered set [0,1][0,1]. Hence they form a distributive lattice and are distributive with respect to each other. However this is not the case for fltlPf_f^P and fltlLf_f^L. We can also immediately prove that the semantics for F and G operators can be simplified as follows, which allows for more efficient implementations. Proposition 3. In fltlxf_f^x: v(φ,λ,i)=v(φ,λ,i)⊕⋯⊕v(φ,λ,last(λ))v(φ,λ,i)=v(φ,λ,i)⊗⋯⊗v(φ,λ,last(λ)) array[]rclv( F ,λ,i)&=&v( ,λ,i) ·s v( ,λ,last(λ))\\ v( G ,λ,i)&=&v( ,λ,i) ·s v( ,λ,last(λ)) array (1) Proof. Recursively using the definition of F and G and the fact that v(φ,λ,i)=0v( X ,λ,i)=0 and v(wφ,λ,i)=1v( X_w ,λ,i)=1 for i≥last(λ)i≥ last(λ) we have v(φ,λ,i)=v(φ,λ,i)⊕…⊕v(φ,λ,last(λ))⊕0…=v(φ,λ,i)⊕…⊕v(φ,λ,last(λ))v( F ,λ,i)=v( ,λ,i) … v( ,λ,last(λ)) 0…=v( ,λ,i) … v( ,λ,last(λ)) and v(φ,λ,i)=v(φ,λ,i)⊗…⊗v(φ,λ,last(λ))⊗1…=v(φ,λ,i)⊗…⊗v(φ,λ,last(λ))v( G ,λ,i)=v( ,λ,i) … v( ,λ,last(λ)) 1…=v( ,λ,i) … v( ,λ,last(λ)). ∎ We finally look at these known equivalences for ltlf to see whether these hold for fltlxf_f^x as well, namely whether the additional temporal operators can be derived by others as abbreviations: φ≡⊤φφ≡¬¬φwφ≡φ∨¬⊤φ1φ2≡φ1φ2∨φ1φ1φ2≡φ2(φ1∧φ2)φ1φ2≡φ2(φ1∧φ2) array[]rclrcl F &≡& U & G &≡& F \\ X_w &≡& X X & _1 W _2&≡& _1 U _2 G _1\\ _1 M _2&≡& _2 U( _1 _2)& _1 R _2&≡& _2 W( _1 _2) array (2) The results are summarised as follows. For ease of notation, in these proofs we write v(φ,i)v( ,i) in place of v(φ,λ,i)v( ,λ,i) since the trace λ is always fixed. Proposition 4. φ≡⊤φ F ≡ U in fltlxf_f^x. Proof. Reasoning by backward induction, first we check the boundary condition: for i=last(λ)i=last(λ) we have v(φ,i)=v(φ,i)=v(⊤φ,i)v( F ,i)=v( ,i)=v( U ,i). In the inductive step, v(⊤φ,i)=v(φ,i)⊕(v(⊤,i)⊗v(⊤φ,i+1))v( U ,i)=v( ,i) (v( ,i) v( U ,i+1)) which by inductive hypothesis is equal to v(φ,i)⊕v(φ,i+1)v( ,i) v( F ,i+1), and thus equal to v(φ,i)v( F ,i). ∎ Proposition 5. φ≡¬¬φ G ≡ F in fltlxf_f^x. Proof. The result follows from Proposition 3 by applying De Morgan’s law, as ⊖(⊖v(φ,i)⊕…⊕⊖v(φ,last(λ))) ( v( ,i) … v( ,last(λ))) is equal to v(¬¬φ,i)v( F ,i). ∎ Proposition 6. wφ≡φ∨¬⊤ X_w ≡ X X in fltlxf_f^x. Proof. We directly show the equality at each instant. v(wφ,i)=v(φ,i+1)v( X_w ,i)=v( ,i+1) if i<last(λ)i<last(λ), 11 otherwise. So for i=last(λ)i=last(λ) we have v(wφ,i)=1=v(¬⊤)v( X_w ,i)=1=v( X ) and v(φ,i)=0v( X ,i)=0, hence equality holds since 0⊕1=10 1=1. For i<last(λ)i<last(λ) we have v(wφ,i)=v(φ,i+1)=v(φ,i)v( X_w ,i)=v( ,i+1)=v( X ,i) while v(¬⊤,i)=0v( X ,i)=0, and these are equal since α⊕0=α 0=α. ∎ Proposition 7. φ1φ2≡(φ1φ2)∨φ1 _1 W _2≡( _1 U _2) G _1 only in fltlGf_f^G. Proof. We start by showing that the equivalence holds for fltlGf_f^G. In particular, we prove the claim by backward induction. First, it is immediate to see that the boundary condition is true, namely for i=last(λ)i=last(λ) v(φ1φ2,i)=v(φ2,i)⊕v(φ1,i)v( _1 W _2,i)=v( _2,i) v( _1,i) while v(φ1φ2,i)=v(φ2,i)v( _1 U _2,i)=v( _2,i) and v(φ1,i)=v(φ1,i)v( G _1,i)=v( _1,i). Then, assuming it holds for some 0<n≤last(λ)0<n≤ last(λ), consider the inductive step for i=n−1i=n-1. On the LHS and RHS we have, respectively: v(φ1φ2,i) v( _1 W _2,i) =v(φ2,i)⊕(v(φ1,i)⊗v(φ1φ2,i+1)), =v( _2,i) (v( _1,i) v( _1 W _2,i+1)), v((φ1φ2)∨φ1,i) v(( _1 U _2) G _1,i) =(v(φ2,i)⊕(v(φ1,i)⊗v(φ1φ2,i+1))⊕(v(φ1,i)⊗v(φ1,i+1))CLOSE. =(v( _2,i) (v( _1,i) v( _1 U _2,i+1)) (v( _1,i) v( G _1,i+1)). Recalling that ⊗ and ⊕ are min and max , respectively, on the RHS we get maxv(φ2,i),minv(φ1,i),maxv(φ1φ2,i+1),v(φ1,i+1) \v( _2,i), \v( _1,i), \v( _1 U _2,i+1),v( G _1,i+1)\\\ by associativity of max and distributivity of min over max . On the LHS instead maxv(φ2,i),minv(φ1,i),v(φ1φ2,i+1) \v( _2,i), \v( _1,i),v( _1 W _2,i+1)\\. These are equal by the inductive hypothesis, namely v(φ1φ2,i+1)=maxv(φ1φ2,i+1),v(φ1,i+1)v( _1 W _2,i+1)= \v( _1 U _2,i+1),v( G _1,i+1)\. Therefore the claim for fltlGf_f^G holds by backward induction. Regarding the negative result for fltlPf_f^P and fltlLf_f^L, the above reasoning fails due to the fact that distributivity does not hold. Indeed, it is immediate to find a counterexample: consider λ=⟨a↦0.5,b↦0.6,a↦0.4,b↦0.7⟩λ= \a 0.5,b 0.6\,\a 0.4,b 0.7\ . In fltlPf_f^P we have on LHS v(ab,1)=0.7⊕(0.4⊗1)=0.82v(a Wb,1)=0.7 (0.4 1)=0.82 and so v(ab,0)=0.6⊕(0.5⊗0.82)=0.764v(a Wb,0)=0.6 (0.5 0.82)=0.764, and on the RHS v(ab,1)=0.7v(a Ub,1)=0.7 and so v(ab,0)=0.6⊕(0.5⊗0.7)=0.74v(a Ub,0)=0.6 (0.5 0.7)=0.74, and also v(a,1)=0.4v( Ga,1)=0.4 and so v(a,0)=0.5⊗0.4=0.2v( Ga,0)=0.5 0.4=0.2. By combining these values, we observe that v(ab,0)≠v(ab,0)⊕v(a,0)v(a Wb,0)≠ v(a Ub,0) v( Ga,0), indeed 0.764≠0.74⊕0.2=0.7920.764≠ 0.74 0.2=0.792. For fltlLf_f^L, we obtain v(ab,1)=0.7⊕(0.4⊗1)=1v(a Wb,1)=0.7 (0.4 1)=1, v(ab,0)=0.6⊕(0.5⊗1)=1v(a Wb,0)=0.6 (0.5 1)=1, v(ab,1)=0.7v(a Ub,1)=0.7, v(ab,0)=0.8v(a Ub,0)=0.8, v(a,1)=0.4v( Ga,1)=0.4 and v(a,0)=0.5⊗0.4=0v( Ga,0)=0.5 0.4=0, by which on the LHS we have v(ab,0)=1v(a Wb,0)=1 whereas on the RHS we get v((ab)∨a,0)=min1,0.8+0=0.8v((a Ub) Ga,0)= \1,0.8+0\=0.8. ∎ Proposition 8. In fltlxf_f^x, operators M and R are dual to W and U, respectively: φ1φ2≡¬(¬φ1¬φ2)φ1φ2≡¬(¬φ1¬φ2) _1 M _2≡ ( _1 W _2) _1 R _2≡ ( _1 U _2) Proof. We show this for M. First, from v(φ1φ2,i)=v(φ2,i)⊗(v(φ1,i)⊕v((φ1φ2),i))v( _1 M _2,i)=v( _2,i) (v( _1,i) v( X( _1 M _2),i)), by repeated application of De Morgan and since ⊖v(φ,i)=v(¬φ,i) v( ,i)=v( ,i) and ⊖v(φ,i)=v(¬φ,i) v( X ,i)=v( X ,i), we obtain v(¬(φ1φ2),i)=v(¬φ2,i)⊕(v(¬φ1,i)⊗v(¬(φ1φ2),i))v( ( _1 M _2),i)=v( _2,i) (v( _1,i) v( X ( _1 M _2),i)). Now we show that ¬(φ1φ2)≡(¬φ1¬φ2) ( _1 M _2)≡( _1 W _2) by backward induction. The boundary condition is true: for i=last(λ)i=last(λ), on the LHS of the equivalence we have v(¬(φ1φ2),i)=⊖(v(φ2,i)⊗(v(φ1,i)⊕0))=v(¬φ2,i)⊕v(¬φ1,i)v( ( _1 M _2),i)= (v( _2,i) (v( _1,i) 0))=v( _2,i) v( _1,i). Likewise, on RHS v(¬φ1¬φ2,i)=v(¬φ2,i)⊕(v(¬φ1,i)⊗1)=v(¬φ2,i)⊕v(¬φ1,i)v( _1 W _2,i)=v( _2,i) (v( _1,i) 1)=v( _2,i) v( _1,i). For the inductive step (so for 0≤i<last(λ)0≤ i<last(λ)), on the LHS and RHS we have, respectively: v(¬(φ1φ2),i) v( ( _1 M _2),i) =v(¬φ2,i)⊕(v(¬φ1,i)⊗v(¬(φ1φ2),i+1)) =v( _2,i) (v( _1,i) v( ( _1 M _2),i+1)) v(¬φ1¬φ2,i) v( _1 W _2,i) =v(¬φ2,i)⊕(v(¬φ1,i)⊗v(¬φ1¬φ2,i+1)) =v( _2,i) (v( _1,i) v( _1 W _2,i+1)) which are equal by hypothesis v(φ1φ2,i+1)=v(¬(¬φ1¬φ2),i+1)v( _1 M _2,i+1)=v( ( _1 W _2),i+1). The proof for R (latter equivalence) has the exact same structure. ∎ Proposition 9. In fltlPf_f^P and fltlLf_f^L M and R cannot be derived by these standard ltlf equivalences: φ1φ2≡φ2(φ1∧φ2)φ1φ2≡φ2(φ1∧φ2) _1 M _2≡ _2 U( _1 _2) _1 R _2≡ _2 W( _1 _2) whereas in fltlGf_f^G these equivalences hold. Proof. We first consider M (former equivalence). Given any λ, assume that v(φ1φ2,n)=v(φ2(φ1∧φ2),n)v( _1 M _2,n)=v( _2 U( _1 _2),n) holds for some 0<n≤last(λ)0<n≤ last(λ). Consider i=n−1i=n-1. By applying the semantics and the hypothesis, on the LHS and RHS we have, respectively: v(φ1φ2,i) v( _1 M _2,i) =v(φ2,i)⊗(v(φ1,i)⊕v(φ1φ2,i+1)) =v( _2,i) (v( _1,i) v( _1 M _2,i+1)) v(φ2(φ1∧φ2),i) v( _2 U( _1 _2),i) =(v(φ1,i)⊗v(φ2,i))⊕(v(φ2,i)⊗v(φ1φ2,i+1)) =(v( _1,i) v( _2,i)) (v( _2,i) v( _1 M _2,i+1)) As to equate these directly requires distributivity, this fails for fltlPf_f^P and fltlLf_f^L since that property does not hold for these semantics. We provide a counterexample which also highlights this aspect: assume λ=⟨a↦0.5,b↦0.6,a↦0.4,b↦0.7⟩λ= \a 0.5,b 0.6\,\a 0.4,b 0.7\ . For fltlPf_f^P, on the LHS we have v(ab,1)=0.7⊗(0.4⊕0)=0.7⋅0.4=0.28v(a Mb,1)=0.7 (0.4 0)=0.7· 0.4=0.28 and so v(ab,0)=0.6⊗(0.5⊕0.28)=0.6⋅(0.5+0.28−0.14)=0.384v(a Mb,0)=0.6 (0.5 0.28)=0.6·(0.5+0.28-0.14)=0.384, while for the RHS we have v(b(a⊗b),1)=0.7⊗(0.4⊕0)=0.28v(b U(a b),1)=0.7 (0.4 0)=0.28 and so v(b(a⊗b),0)=(0.5⊗0.6)⊕(0.6⊗0.28)=0.3+0.168−0.3⋅0.168=0.4176v(b U(a b),0)=(0.5 0.6) (0.6 0.28)=0.3+0.168-0.3· 0.168=0.4176. For fltlLf_f^L, on the LHS we have v(ab,1)=0.7⊗(0.4⊕0)=0.1v(a Mb,1)=0.7 (0.4 0)=0.1 and so v(ab,0)=0.6⊗(0.5⊕0.1)=max0,0.6+min1,0.5+0.1−1=0.2v(a Mb,0)=0.6 (0.5 0.1)= \0,0.6+ \1,0.5+0.1\-1\=0.2, while for the RHS we have v(b(a⊗b),1)=v(a⊗b,1)=max0,0.4+0.7−1=0.1v(b U(a b),1)=v(a b,1)= \0,0.4+0.7-1\=0.1 and so v(b(a⊗b),0)=(0.5⊗0.6)⊕(0.6⊗0.1)=min1,0.1+0=0.1v(b U(a b),0)=(0.5 0.6) (0.6 0.1)= \1,0.1+0\=0.1. For fltlGf_f^G instead the equality in the inductive step holds because of distributivity. Moreover, the boundary condition holds as well (as it does for fltlPf_f^P and fltlLf_f^L, since this only requires ⊕(x,0)=x (x,0)=x and commutativity of ⊗ ): for i=last(λ)i=last(λ), on the LHS we have v(φ1φ2,i)=v(φ2,i)⊗(v(φ1,i)⊕0)=v(φ1,i)⊗v(φ2,i)v( _1 M _2,i)=v( _2,i) (v( _1,i) 0)=v( _1,i) v( _2,i) and on the RHS v(φ2(φ1∧φ2),i)=(v(φ1,i)⊗v(φ2,i))⊕(v(φ2,i)⊗0)=v(φ1,i)⊗v(φ2,i)v( _2 U( _1 _2),i)=(v( _1,i) v( _2,i)) (v( _2,i) 0)=v( _1,i) v( _2,i). Thus we obtain the claim by backward induction. For R (latter equivalence), in the inductive step (hence with 0<i<last(λ)0<i<last(λ), namely the next instant exists) we apply the semantics and the hypothesis (i.e., that v(φ1φ2,i+1)=v(φ2(φ1∧φ2),i+1)v( _1 R _2,i+1)=v( _2 W( _1 _2),i+1)), obtaining on the LHS and RHS, respectively: v(φ1φ2,i) v( _1 R _2,i) =v(φ2,i)⊗(v(φ1,i)⊕v(φ1φ2,i+1)) =v( _2,i) (v( _1,i) v( _1 R _2,i+1)) v(φ2(φ1∧φ2),i) v( _2 W( _1 _2),i) =(v(φ1,i)⊗v(φ2,i))⊕(v(φ2,i)⊗v(φ1φ2,i+1)) =(v( _1,i) v( _2,i)) (v( _2,i) v( _1 R _2,i+1)) which has the exact shape obtained for the former equivalence, so the same considerations apply regarding fltlPf_f^P and fltlLf_f^L. Indeed, for the counter-example trace λ as above, we obtain distinct values: for fltlPf_f^P v(ab,1)=0.7v(a Rb,1)=0.7, v(ab,0)=0.6⊗(0.5⊕0.7)=0.51v(a Rb,0)=0.6 (0.5 0.7)=0.51, v(b(a∧b),1)=(0.4⊗0.7)⊕(0.7⊗1)=0.784v(b W(a b),1)=(0.4 0.7) (0.7 1)=0.784, v(b(a∧b),0)=(0.5⊗0.6)⊕(0.6⊗0.784)=0.62928v(b W(a b),0)=(0.5 0.6) (0.6 0.784)=0.62928. For fltlLf_f^L v(ab,1)=0.7v(a Rb,1)=0.7, v(ab,0)=0.6⊗(0.5⊕0.7)=0.6v(a Rb,0)=0.6 (0.5 0.7)=0.6, v(b(a∧b),1)=(0.4⊗0.7)⊕(0.7⊗1)=0.8v(b W(a b),1)=(0.4 0.7) (0.7 1)=0.8, v(b(a∧b),0)=(0.5⊗0.6)⊕(0.6⊗0.8)=0.5v(b W(a b),0)=(0.5 0.6) (0.6 0.8)=0.5. Again, the boundary condition holds for fltlGf_f^G: for i=last(λ)i=last(λ) we have v(φ1φ2,i)=v(φ2,i)⊗(v(φ1,i)⊕1)=minv(φ2,i),1=v(φ2,i)v( _1 R _2,i)=v( _2,i) (v( _1,i) 1)= \v( _2,i),1\=v( _2,i). And likewise: v(φ2(φ1∧φ2),i)=(v(φ1,i)⊗v(φ2,i))⊕(v(φ2,i)⊗1)=maxminv(φ1,i),v(φ2,i),v(φ2,i)=v(φ2,i)v( _2 W( _1 _2),i)=(v( _1,i) v( _2,i)) (v( _2,i) 1)= \ \v( _1,i),v( _2,i)\,v( _2,i)\=v( _2,i). So the boundary condition holds and by distributivity so does the inductive equality, hence the claim follows by backward induction. ∎ These results show that R can be obtained by duality from U in fltlxf_f^x and M from W, however W is an abbreviation only in fltlGf_f^G. Therefore, the temporal logical basis for fltlGf_f^G can be expressed as ,\ X, U\, whereas for the other semantics we consider also W as primitive. As a final remark, note that irrespective of the semantics chosen, since standard negation is also crisp, these logics collapse to ltlf in the special case in which only 00/11 values are present in a trace (and thus it can be taken as a standard ltlf trace as in Definition 1). Indeed, on boolean values the t-norm corresponds to the boolean conjunction and the t-conorm to the boolean disjunction. 5 The ∂ Framework In this section, we introduce the ∂ framework, starting with the problem formulation in Section 5.1, before introducing the proposed approach in Section 5.2, and its implementation in Section 5.3. 5.1 Problem Formulation We consider a weakly supervised sequence classification task defined over multiple streams of observations, such as images. Let =1,…,SS=\1,…,S\ be a set of distinct perceptual streams and let X be the observation space containing the raw data. A sequence of length n is =⟨0,…,n−1⟩x= _0,…,x_n-1 , where each element i=⟨xi1,…,xi||⟩x_i= x_i^1,…,x_i^|S| at instant i∈0,…,n−1i∈\0,…,n-1\ is a tuple of observations, one for each stream s∈s , with xis∈x_i^s . We define two sets, C and P. The set of classes C is the set of possible labels of an observation (e.g., the digits 0,…,90,…,9 for the MNIST dataset), and, for simplicity, we assume it is shared across streams. 44 4 For notational simplicity, we assume that all streams share a common observation space X. The framework extends simply to the general case of stream-specific observation spaces sX^s, one for each s∈s , by replacing the shared perception module fθf_θ with stream-specific modules fθs:s→[0,1]|s|f_θ^s:X^s→[0,1]^|C^s|. The set of atomic propositions P is the alphabet over which the symbolic traces of Section 4 are defined. For each stream s, we employ a distinct set of propositional symbols sP^s, where pcs∈sp_c^s ^s denotes the fact that an observation in stream s belongs to class c∈c . Therefore, =⋃s∈sP= _s P^s is the full propositional alphabet, with s∩s′=∅P^s ^s = for s≠s′s≠ s . The learning task is guided by a temporal specification Φ , expressed as an ltlf formula over the alphabet P. Each input sequence of observations x corresponds to a crisp symbolic trace λ=⟨λ0,…,λn−1⟩λ^x= _0,…, _n-1 as defined in Definition 1, with λi(pcs)=1 _i(p_c^s)=1 if xisx_i^s is of class c, and 00 otherwise. The binary label y associated with x is 11 if λ^x satisfies Φ , and 00 otherwise: y=1if λ⊧ltlfΦ0otherwisey= cases1&if λ^x _ ltl_f \\ 0&otherwise cases (3) The crisp trace λ^x, however, is not available during training. The dataset D is a collection of M pairs (,y)(x,y), where only the sub-symbolic input x and the binary label y are observed. The goal is to learn the parameters θ of a perception module, modelled as a function fθ:→[0,1]||f_θ:X→[0,1]^|C|, shared across streams, that maps each raw observation to a vector of fuzzy truth values. In other words, the task is an instance of weakly supervised symbol grounding, a common setting in neurosymbolic AI [23, 6]. The learning of the concepts is not driven by direct per-concept supervision, but by background knowledge, in our case the temporal specification Φ , together with the resulting sequence-level binary label y. 5.2 Framework Figure 4: Overview of the ∂ framework. The perception module fθf_θ produces the fuzzy trace λθ _θ (rows represent the propositions pcsp^s_c grouped by stream). The temporal logic module evaluates Φ under the fltlxf_f^x semantics. The loss evaluates the predictions of the temporal logic module in comparison with the ground truth label. ∂ is a neurosymbolic framework that, given an observation sequence x and a temporal specification Φ , computes a fuzzy satisfaction value for formula Φ . Internally, it first computes the fuzzy truth values of propositions P through a perception module fθf_θ, and then it feeds them to the temporal logic module to compute the final truth value. Since the framework is differentiable almost everywhere, it can be trained end-to-end directly by applying a loss function to its outputs. The entire pipeline of ∂ is illustrated in Figure 4 and consists of three components: perception module, temporal logic module, and loss. Perception module The perception module fθf_θ is applied independently to each observation xisx_i^s in every stream and at every instant. Each application of the perception module to an observation produces a vector in [0,1]||[0,1]^|C| whose c-th element is the fuzzy truth value assigned to the atomic proposition pcsp_c^s at that instant: λi(pcs)=fθ(xis)c,for c∈,s∈,i∈0,…,n−1. _i(p_c^s)=f_θ(x_i^s)_c, c ,\ s ,\ i∈\0,…,n-1\. (4) In the general formulation, atoms pcsp^s_c are not assumed to be mutually exclusive. When mutual exclusivity holds, i.e., each observation represents a single class, a softmax output layer can be applied to fθf_θ, giving ∑c∈fθ(xis)c=1 _c f_θ(x_i^s)_c=1. Collecting these values across all instants yields, for each atom pcsp_c^s, the sequence λ(pcs)=⟨fθ(x0s)c,…,fθ(xn−1s)c⟩λ(p^s_c)= f_θ(x_0^s)_c,…,f_θ(x_n-1^s)_c in the sense of Definition 2. Across all atoms and streams, these sequences form the fuzzy trace λθ _θ. Temporal logic module The temporal specification Φ is represented by its syntactic tree, shown in Figure 4, whose leaves are the atomic propositions in P and whose internal nodes are the connectives and temporal operators occurring in Φ . The formula is evaluated directly on the fuzzy trace λθ _θ by application of the fltlxf_f^x semantics defined in Section 4, under any of its three fuzzy semantic instances, without any intermediate automaton construction, proceeding from the leaves of the tree to its root. The output is the value v(Φ,λθ,0)∈[0,1]v( , _θ,0)∈[0,1], which represents the degree of satisfaction of Φ at the beginning of the trace. For conciseness we denote it with v(Φ,λθ)v( , _θ), as in Section 4. The evaluation is differentiable almost everywhere with respect to the perception outputs, allowing the perception module to be trained using standard automatic differentiation. Loss The fuzzy satisfaction value v(Φ,λθ)v( , _θ) is compared against the binary label y via binary cross-entropy. Gradients of the resulting loss are backpropagated through the temporal logic module and the perception module to update θ. In contrast to existing temporal neurosymbolic approaches based on ltlf [29, 22], which compile Φ into deterministic finite automata and propagate state values across the input sequence, ∂ evaluates Φ by recursive application of the fltlxf_f^x semantics directly on the fuzzy trace produced by the perception module. Our use of fuzzy semantics to evaluate logical formulas is shared with static neurosymbolic frameworks such as LTN [2] and SBR [12], but the setting is different. There, the formula is assumed to hold for all instances, and its satisfaction is maximised during training. Here Φ is not assumed to hold, and its satisfaction is the prediction of the model. Following von Rüden et al. 2023, this makes those frameworks loss-based and ∂ model-based, with Φ acting as a differentiable layer that stays in the model at inference time. 55 5 The ∂ framework is not limited to this setting, as it can be instantiated in a loss-based fashion, and the theoretical analysis of Section 4 applies unchanged. We leave such extensions to future work. 5.3 Implementation The temporal logic module is implemented as a Python library built on top of PyTorch66 6 https://pytorch.org/ and operates on batches of sequences in tensor form. A batch consists of B sequences, indexed by b∈0,…,B−1b∈\0,…,B-1\, of possibly different lengths nbn_b. Representing a batch as a single tensor allows every step of the evaluation to be carried out by one tensor operation over all its sequences at once, but requires them to share a common length. We therefore let T=maxbnbT= _bn_b be the maximum length in the batch, and pad the shorter sequences up to T. Padding is introduced for this purpose alone, and how it is treated is described later in this section. The batch is then represented by two tensors. The first, Λθ∈[0,1]B×T×|| _θ∈[0,1]^B× T×|P|, collects the fuzzy values produced by the perception module fθf_θ on every observation of every sequence. Its slice (Λθ)b( _θ)_b is the tensor encoding of the fuzzy trace λθ(b) _θ^(b) of the b-th sequence. Along the time axis, for a fixed proposition p, the slice (Λθ)b,:,p( _θ)_b,:,p encodes λ(p)λ(p) for the b-th sequence. Here the colon denotes all the entries along that axis, so that the slice collects the values that p takes at every instant of the sequence. The second tensor, μ∈0,1B×Tμ∈\0,1\^B× T, is a boolean mask that flags the valid instants with 1 and the padded ones with 0: μb,i=1if i≤nb−10otherwise. _b,i= cases1&if i≤ n_b-1\\ 0&otherwise. cases (5) Algorithm 1 Recursive tensor evaluation for fltlxf_f^x formulas. 1: function Eval(φ , Λθ _θ, μ) 2: if φ is an atom p then 3: return (Λθ):,:,p( _θ)_:,:,p 4: else if φ=φ1∧φ2 = _1 _2 then ⊳ analogously for ∨,¬,→ , ,→ 5: return Eval(φ1,Λθ,μ)⊗Eval(φ2,Λθ,μ) Eval( _1, _θ,μ) Eval( _2, _θ,μ) 6: else if φ=ψ = Xψ then ⊳ analogously for w X_w with fill 11 and last column 11 7: V←Eval(ψ,Λθ,μ)V← Eval(ψ, _θ,μ) 8: V~←fill(V,μ,0) V (V,μ,0) 9: return left shift of V~ V by one position, last column ←0← 0 10: else if φ=ψ = Gψ then ⊳ analogously for F with fill 00 and ⊕ 11: V←Eval(ψ,Λθ,μ)V← Eval(ψ, _θ,μ) 12: V~←fill(V,μ,1) V (V,μ,1) 13: return reverse cumulative ⊗ of V~ V along the time axis 14: else if φ=φ1φ2 = _1 U _2 then ⊳ analogously for ,, W, R, M 15: V~1←fill(Eval(φ1,Λθ,μ),μ,0) V_1 ( Eval( _1, _θ,μ),μ,0) 16: V~2←fill(Eval(φ2,Λθ,μ),μ,0) V_2 ( Eval( _2, _θ,μ),μ,0) 17: V←V← empty tensor of shape (B,T)(B,T); curr←0curr← 0 18: for i=T−1i=T-1 down to 00 do 19: curr←(V~2):,i⊕((V~1):,i⊗curr)curr←( V_2)_:,i (( V_1)_:,i ) 20: V:,i←currV_:,i 21: end for 22: return V 23: end if 24: end function The recursive evaluator, given as the function Eval of Algorithm 1, visits the syntactic structure of Φ from the leaves to the root, associating to each sub-formula φ a tensor Vφ∈[0,1]B×TV_ ∈[0,1]^B× T such that (Vφ)b,i=v(φ,λθ(b),i)(V_ )_b,i=v( , _θ^(b),i) at every valid instant. For each sequence b in the batch, the satisfaction value v(Φ,λθ(b),0)v( , _θ^(b),0) fed to the loss is the element (VΦ)b,0(V_ )_b,0 of the value tensor. For sequences shorter than T, the evaluation would be affected by the padded positions. To prevent this, and so to properly manage padding values, we introduce two auxiliary operators ∇0 _0 and ∇1 _1. Applied to an operand value at an instant within nbn_b, they return that value unchanged, while applied past the end of the trace, they return 0 and 1, respectively. Each temporal operator of fltlxf_f^x is associated with one of the two, determined by its semantics at the boundary. When a temporal operator associated with ∇∈∇0,∇1∇∈\ _0, _1\ is applied to a sub-formula with the value tensor VφV_ , the operator first replaces the padded entries of VφV_ with the value ∇ returns past the end of the trace (00 for ∇0 _0, 11 for ∇1 _1), obtaining (V~φ)b,i=(Vφ)b,iif μb,i=10if μb,i=0 and ∇=∇01if μb,i=0 and ∇=∇1( V_ )_b,i= cases(V_ )_b,i&if _b,i=1\\ 0&if _b,i=0 and ∇= _0\\ 1&if _b,i=0 and ∇= _1 cases (6) It then applies its tensor operation to V~φ V_ . This substitution is performed by the function fillfill of Algorithm 1. Padded positions therefore contribute only this boundary value and cannot affect the result at any valid instant. Propositional connectives are pointwise and require no padding logic. Their pointwise nature implies that a padded value at (b,i)(b,i) can affect only the outputs at the same (b,i)(b,i) in subsequent propositional steps, and it is overwritten by the boundary value of any temporal operator further up. Since the loss considers VΦV_ only at i=0i=0, which is a valid instant in every sequence, what happens at padded positions has no effect on the satisfaction value. Each operator is computed by a standard tensor operation on its operand(s), one for each branch of Eval. Propositional connectives apply the elementwise t-norm, t-conorm, and fuzzy negation of the chosen semantics (Algorithm 1, line 4). VφV_ X is obtained by shifting V~φ V_ (with ∇=∇0∇= _0) one position to the left and filling the last column with 00 (line 6). VwφV_ X_w is analogous, with ∇1 _1 and last column filled with 11. VφV_ G at instant i is the iterated t-norm of V~φ V_ (with ∇=∇1∇= _1) from i to the end of the trace, computed as a reverse cumulative ⊗ along the time axis (line 10). VφV_ F is the iterated t-conorm (with ∇=∇0∇= _0): (Vφ)b,i=⨂k=iT−1(V~φ)b,k,(Vφ)b,i=⨁k=iT−1(V~φ)b,k.(V_ G )_b,i= _k=i^T-1( V_ )_b,k, (V_ F )_b,i= _k=i^T-1( V_ )_b,k. (7) φ1φ2 _1 U _2 is computed by backward iteration over time on V~φ1 V_ _1 and V~φ2 V_ _2 (both with ∇=∇0∇= _0), following the recursive computation v(φ1φ2,λ,i)=v(φ2,λ,i)⊕(v(φ1,λ,i)⊗v(φ1φ2,λ,i+1))v( _1 U _2,λ,i)=v( _2,λ,i) (v( _1,λ,i) v( _1 U _2,λ,i+1)) (8) initialised at the end of the trace with the value returned by ∇0 _0 (Algorithm 1, lines 14-22). The remaining operators of fltlxf_f^x can be handled in the same way. Example 3. Consider Φ=(a→b) = G(a→ Fb), interpreted under Gödel semantics, on a trace of length 33 padded to T=5T=5, so that μ=(1,1,1,0,0)μ=(1,1,1,0,0). The perception module assigns to a and b the values Va=(0.8, 0.1, 0.2,∗,∗)V_a=(0.8,\,0.1,\,0.2,\,*,\,*) and Vb=(0.1, 0.3, 0.7,∗,∗)V_b=(0.1,\,0.3,\,0.7,\,*,\,*), where ∗* marks padded positions. The evaluator proceeds bottom-up. The sub-formula b Fb uses ∇0 _0, so its padded entries become 00, obtaining V~b=(0.1, 0.3, 0.7, 0, 0) V_b=(0.1,\,0.3,\,0.7,\,0,\,0). Since 00 is the identity of ⊕ , the iterated t-conorm is unaffected, and Vb=(0.7, 0.7, 0.7,∗,∗)V_ Fb=(0.7,\,0.7,\,0.7,\,*,\,*). The implication connective is pointwise, i.e., it is computed independently at each instant, and with ¬a=(0.2, 0.9, 0.8,∗,∗) a=(0.2,\,0.9,\,0.8,\,*,\,*) this yields Va→b=(0.7, 0.9, 0.8,∗,∗)V_a→ Fb=(0.7,\,0.9,\,0.8,\,*,\,*). Finally, G uses ∇1 _1, filling the padded entries with 11. Since 11 is the identity of ⊗ , the iterated t-norm is unaffected, and v(Φ,λ)=(VΦ)0=0.7v( ,λ)=(V_ )_0=0.7, matching the evaluation on the unpadded trace. fuzzy trace λθ _θi=0i=0 i=1i=1 i=2i=2 i=3i=3 i=4i=4 11 11 11 00 00 0.80.8 0.10.1 0.20.2 ∗* ∗* 0.10.1 0.30.3 0.70.7 ∗* ∗* μ _aVbV_b¬a aelementwise ⊖ 0.20.2 0.90.9 0.80.8 ∗* ∗* V¬aV_ ab Fb∇0 _00.10.1 0.30.3 0.70.7 00 00 0.70.7 0.70.7 0.70.7 ∗* ∗* V~b V_bVbV_ Fbreverse cumulative ⊕ →b≡¬a∨ba→ Fb\;≡\; a Fb0.20.2 0.90.9 0.80.8 ∗* ∗* 0.70.7 0.70.7 0.70.7 ∗* ∗* 0.70.7 0.90.9 0.80.8 ∗* ∗* V¬aV_ aVbV_ FbV¬a∨bV_ a Fbelementwise ⊕ Φ=(¬a∨b) = G( a Fb)∇1 _10.70.7 0.90.9 0.80.8 11 11 0.70.7 0.80.8 0.80.8 ∗* ∗* V~¬a∨b V_ a FbVΦV_ reverse cumulative ⊗ (Φ,λθ)=(VΦ)0=0.7v( , _θ)=(V_ )_0=0.7 Gödel semantics: α⊗β=minα,βα β= \α,β\, α⊕β=maxα,βα β= \α,β\, ⊖α=1−α α=1-α. Figure 5: Computation of v((a→b),λ)v( G(a→ Fb),λ), from Example 3. 6 Evaluation In this section, we evaluate ∂ on a temporal neurosymbolic learning task involving multi-stream perception traces and complex temporal dependencies. We compare our approach against two state-of-the-art approaches based on deterministic finite-state automata (DFA), introduced in Section 3, namely FuzzyA [29] and NeSyA [22]. Our evaluation focuses on two complementary aspects: (i) performance in terms of sequence-level classification accuracy, and symbol grounding quality under weak supervision; (i) computational scalability with respect to increasing formula complexity and sequence lengths. To structure the experimental analysis, we will address the following research questions: 1. RQ1: Impact of fuzzy temporal semantics. How do different fuzzy ltlf semantics used in ∂ affect the sequence classification accuracy and symbol grounding performance of the proposed approach? 2. RQ2: Comparison with state of the art. How does the proposed approach compare against existing state-of-the-art temporal neurosymbolic integration methods in terms of classification accuracy and symbol grounding performance? 3. RQ3: Scalability. How do different temporal NeSy approaches scale in terms of runtime complexity as formula complexity and sequence length increase? RQ1 aims to determine the impact of the different fuzzy semantics introduced in Section 4 within the ∂ framework on classification performance at both the sequence level and the symbol grounding level. While comparisons of fuzzy semantics have previously been conducted in non-temporal domains [17], their impact in temporal settings remains largely unexplored. For RQ2, we compare the best-performing fuzzy semantics with state-of-the-art temporal neurosymbolic approaches in terms of classification accuracy at both the sequence level and the individual symbol grounding level. To this end, we vary both the complexity of the formulas and the length of the input sequences. This allows us to assess how the different methods perform not only in terms of predictive accuracy but also in their ability to scale with increasing formula complexity and input length. For RQ3, similarly to RQ2, we evaluate how the proposed method compares with state-of-the-art approaches in terms of computational cost during training when increasing sequence length and formula complexity. Specifically, we measure the runtime of the logic modules per training epoch for each technique. 6.1 Temporal Multi-Stream Benchmark We evaluate ∂ on a temporal multi-stream benchmark, which represents a specific instantiation of the problem defined in Section 5. Our evaluation builds on the LTLZinc benchmarking framework [20], which generates temporal sequence classification tasks from ltlf specifications and static relational constraints. We introduce three deliberate modifications that adapt the framework to our evaluation objectives. First, we remove all relational constraints from the specification. LTLZinc tasks interleave temporal operators with relational predicates, resulting from arithmetic comparisons or global constraints (e.g. all_different). While this design is appropriate for evaluating the joint effect of relational and temporal reasoning, it may confound the two distinct reasoning capabilities. A method that fails on such a task may do so because of flawed temporal reasoning, flawed relational reasoning, or both. The evaluation cannot distinguish between the two cases. By restricting our specifications to purely temporal formulas, we isolate a model’s temporal reasoning capabilities and obtain a more sound evaluation. Second, we increase the complexity of the temporal specifications beyond the level considered in prior work. Third, we adopt a strictly weaker form of supervision. The LTLZinc benchmark provides annotations at multiple levels: ground-truth image labels at every timestep, relational constraint satisfaction, automaton states, in addition to sequence-level satisfaction label. Accordingly, the training pipeline proposed by LTLZinc employs four separate loss terms that supervise image classification, relational constraint classification, next-state prediction, and sequence classification independently. In addition, it employs a pre-training phase with direct supervision on the image labels to ensure convergence [20]. In contrast, our setting provides only the binary satisfaction label of the temporal formula as supervision. In other words, the neurosymbolic system must solve the symbol grounding problem entirely from this sequence-level supervisory signal, without access to intermediate annotations. This choice reflects a more realistic scenario, since in practical applications ground-truth symbolic traces, automaton states, and constraint labels are typically unavailable. Moreover, supervision on automaton states is intrinsically DFA-based and it is not applicable to methods such as ∂ that evaluate temporal formulas directly. As a result, LTLZinc’s evaluation protocol restricts fair comparison to DFA-based approaches only. In our proposed benchmark, the input sequences consist of S=3S=3 parallel streams, denoted as (X,Y,Z)(X,Y,Z), each receiving a sequence of images, as in LTLZinc [20]. The temporal specifications used in our experiments are built from the ltlf templates introduced in Section 2 and listed in Table 1, which have been previously adopted within the experimental setting of temporal NeSy architectures [29, 1, 28]. Based on these eight templates, we define two separate sets of formulas in order to distinguish between different classes of temporal dependencies and to assess their impact independently. In particular, the partition separates constraints that primarily capture forward-looking (response-type) relations from those that enforce backward-looking or co-occurrence (precedence-type) relations, which differ in both semantics and verification complexity. The first set, Set 1, combines the first four patterns from Table 1, namely Response, Not Succession, Chain Succession, and Not Chain Succession templates. Conversely, Set 2 combines the last four templates: Precedence, Chain Precedence, Responded Existence, and Not Co-existence. Each formula set is paired with two image datasets, which are also used within the LTLZinc benchmark [20]: MNIST [19] and Fashion-MNIST [32], resulting in four experimental cases in total. 6.1.1 Varying Formula Complexity In this evaluation direction, the temporal specification Φ is defined as a conjunction of K independent temporal sub-formulas, Φ=⋀k=1Kφk = _k=1^K _k, where each sub-formula φk _k is an instantiation of a template from Table 1. Since each sub-formula introduces two additional classes, the total number of classes in the temporal specification grows as ||=2K|C|=2K. By varying K∈1,2,3,4K∈\1,2,3,4\, we increase the complexity of the temporal specification and, as a consequence, of the learning task. The dataset for each setting is composed of sequences of varying lengths, sampled uniformly from the integer interval [2,10][2,10]. Sequence length is deliberately kept short and fixed in distribution across all values of K, so that variation in performance is attributable to formula complexity alone, and not confounded by sequence length, whose effect is examined using the setting described in Section 6.1.2. As an example, for Set 1 with K=2K=2 the specification is Φ=(p0X→p1Y)∧G((p2Y∨p3Z)→¬p3X) = G(p^X_0→ Fp^Y_1) G((p^Y_2 p^Z_3)→ Fp^X_3), which conjoins the Response and Not Succession patterns. 6.1.2 Varying Sequence Length In this evaluation direction, the temporal specification is fixed, and the sequence length varies from 20 to 200 in steps of 20. Unlike the previous setting, all sequences within each configuration share the same fixed length, so as to isolate the effect of sequence length on learning performance. The image dataset is MNIST [19]. We consider two specifications of different complexity, based on either the Response or Precedence template from Table 1. The first involves ||=4|C|=4 classes and is defined as a conjunction of two Response sub-formulas. The second involves ||=8|C|=8 classes and takes the form Φ=(φ1∧φ2)∨(φ3∧φ4) =( _1 _2) ( _3 _4), where each φk _k is an instantiation of the Precedence pattern. 77 7 When traces are sampled uniformly at random, the fraction of positive traces in the generated dataset generally depends on the trace length, and for most templates in Table 1 it degenerates towards 00 or 11 as the length grows. The Response and Precedence templates do not show this behaviour, as their satisfaction probability converges to a constant as the trace length increases. The way the sub-formulas are combined is chosen for the same reason, that is, to obtain datasets that are as balanced as possible. Using two specifications allows us to observe whether the effect of increasing sequence length depends also on the complexity of the temporal specification itself. 6.2 Evaluation Metrics We use two accuracy metrics, both computed on the held-out test set. Symbol grounding accuracy is the fraction of correctly classified images. Each observation xisx_i^s is assigned to the class argmaxcfθ(xis)c _cf_θ(x_i^s)_c and compared against its ground-truth class, and averaged over all observations, streams, and sequences. Sequence classification accuracy is the fraction of sequences whose predicted satisfaction matches the label y. A sequence is predicted to satisfy Φ when v(Φ,λθ)≥0.5v( , _θ)≥ 0.5. The per-image ground-truth labels serve only to evaluate symbol grounding performance and are never used during training, consistently with the weakly supervised setting of Section 2.1. Finally, computational cost is measured as the logic-module time per training epoch. 7 Results This section presents the experimental results structured around the three research questions introduced in Section 6. RQ1 (Section 7.1) investigates the impact of the fuzzy semantics on the sequence classification and on the symbol grounding accuracy performance within ∂ . RQ2 (Section 7.2) compares the best-performing ∂ semantic configuration against state-of-the-art temporal neurosymbolic methods in terms of classification accuracy at both the sequence and symbol grounding level. RQ3 (Section 7.3) evaluates the computational scalability of the compared methods. The three subsections share the same structure: each one first provides a direct answer to the corresponding research question, supported by the experimental evidence, and then discusses the results in greater depth, providing additional insights. All results are averaged over 10 independent runs. As all methods share seeds, splits, and sampled sequences, differing only in the logic module, statistical significance is assessed with a paired one-sided Wilcoxon signed-rank test. Throughout, results marked in bold denote a method that is significantly better than all competitors at p<0.05p<0.05. The complete experimental setup, including perception architecture, optimiser, learning rate, batch size, number of training epochs, dataset construction, and hardware, is identical across all compared methods and is reported in B. 7.1 RQ1: Impact of Fuzzy Temporal Semantics Figure 6: Symbol grounding accuracy (%) across 10 independent runs for ∂ instantiated with the three fuzzy semantics: Product (fltlPf_f^P), Łukasiewicz (fltlLf_f^L), and Gödel (fltlGf_f^G). Each subplot corresponds to one experimental setting (formula set × image dataset), with the number of classes |||C| on the horizontal axis. We evaluate the effect of the underlying fuzzy semantics on the classification performance of ∂ . Specifically, we compare the three instantiations of fltlxf_f^x introduced in Section 4: Gödel (fltlGf_f^G), Product (fltlPf_f^P), and Łukasiewicz (fltlLf_f^L). The comparison is conducted across all four experimental settings of Section 6.1.1, with the number of classes |||C|, equal to twice the number of conjoined sub-formulas, ranging from 22 to 88. Figure 6 shows the symbol grounding accuracy attained by each semantics at each value of |||C|. Table 2 reports the average of the symbol grounding and the sequence classification accuracy over the four settings. Table 2: Symbol grounding and sequence classification accuracy (%) of ∂ under the three fuzzy semantics, averaged over the four experimental settings and 10 runs. Results in bold are significantly better than both other semantics (Wilcoxon, p<0.05p<0.05). Img. Acc. (%) ↑ Seq. Acc. (%) ↑ |||C| 2 4 6 8 2 4 6 8 fltlPf_f^P 99.9 97.7 93.3 89.2 99.9 98.9 97.0 96.0 fltlGf_f^G 99.9 62.2 32.1 19.9 99.9 90.0 88.6 86.2 fltlLf_f^L 94.9 64.0 49.2 37.6 96.6 90.6 89.3 87.7 7.1.1 Answer to RQ1 The choice of the fuzzy semantics has a substantial impact on the accuracy performance of ∂ , and Product is the only semantics that remains robust as the complexity of the temporal specification grows. fltlPf_f^P maintains consistently high symbol grounding accuracy, with low variance, across all values of |||C| and across all settings. Its average accuracy remains above 92%92\% and 85%85\% for the MNIST and Fashion-MNIST datasets, respectively, even at ||=8|C|=8. The low variance throughout the 10 runs indicates that convergence to a correct grounding does not depend on the initialisation. Gödel and Łukasiewicz semantics, in contrast, are competitive only on the simplest specifications. At ||=2|C|=2, where the temporal specification involves only two classes, all three semantics achieve comparable performances, with average grounding accuracy above 99%99\% in almost all settings. Differences emerge as the formula complexity increases, as both Gödel and Łukasiewicz exhibit a significant increase in variance. For ||=4|C|=4, while these two semantics occasionally reach near-optimal levels of performance, many runs converge to lower values. For ||≥6|C|≥ 6, the degradation of performance becomes more severe. This pattern suggests sensitivity to local optima during training. Sequence classification accuracy follows the same ranking, but with much smaller differences (Table 2), as sequence classification is an easier task than symbol grounding. Based on these findings, all subsequent experiments adopt fltlPf_f^P Product semantics as the default configuration of ∂ . Having answered RQ1, the remainder of this subsection discusses these results in greater depth and provides further insights. 7.1.2 Discussion on RQ1 The pattern observed above is consistent with prior findings in non-temporal neurosymbolic settings, where Product logic has been shown to provide more informative gradients than Gödel and Łukasiewicz for constraint satisfaction tasks [17]. The present results extend this observation to the temporal domain and can be explained by analysing the gradient properties of the underlying operators. In our setting, the temporal operators G and F reduce to iterated applications of the t-norm and t-conorm respectively, over the trace length. Under Product semantics, the t-norm α⊗β=α⋅βα β=α·β has partial derivative β with respect to α, and the t-conorm α⊕β=α+β−α⋅βα β=α+β-α·β has partial derivative 1−β1-β. Both are non-vanishing on almost the entire input domain. As a result, when G is evaluated over a trace of length n, every timestep receives a non-zero gradient, enabling the perception module to update all its predictions in each training step. Under Gödel semantics, the min and max operators are single-passing. As shown in [17], any composition of single-passing functions is itself single-passing. As a consequence, the entire computation graph derived from a temporal formula inherits this property. Concretely, given a sequence of n observations, exactly one receives a non-zero gradient. For this reason, convergence becomes sensitive to which single observation happens to receive the learning signal. This makes learning increasingly hard as the formula’s complexity grows, explaining the performance degradation and high variance observed in Figure 6. Under Łukasiewicz semantics, the t-norm α⊗β=max(α+β−1,0)α β= (α+β-1,0) has gradient 11 when α+β>1α+β>1 and 00 otherwise. For the n-ary case, which corresponds to the evaluation of G over a trace of length n, van Krieken et al. [17] show that the gradient is non-vanishing only when the mean truth value of the n arguments is greater than (n−1)/n(n-1)/n, and that the fraction of the input space satisfying this condition is 1/n!1/n!. This condition is particularly difficult to satisfy, especially during early training, when the perception module produces output with intermediate truth values. The t-conorm min(α+β,1) (α+β,1) shows a symmetrical issue, with its gradient vanishing when the sum of its arguments exceeds 11. As |||C| increases, the outer conjunction further stresses the problem. This explains the performance degradation at higher |||C| (Figure 6). 7.2 RQ2: Comparison with State of the Art Following the outcome of RQ1, we instantiate ∂ with Product semantics and compare it against two state-of-the-art temporal neurosymbolic methods: FuzzyA 88 8 We use the FuzzyA implementation from the LTLZinc benchmark [20], which deviates from the original in state normalisation and training loss; see A for a precise description. [29] and NeSyA [22]. The comparison is conducted along two complementary directions: increasing the formula complexity (Table 3) and increasing the sequence length (Table 4). Both tables also report the logic module time per epoch, which is discussed separately in Section 7.3. Figure 7 summarises the formula-complexity results averaged over the four settings. It additionally includes four further methods: T-ILR [1], the original FuzzyA implementation, and two purely neural baselines, obtained by replacing the logic module with a GRU [5] and with a Transformer encoder [31], respectively. All of them fall substantially behind the three neurosymbolic methods compared above, increasingly so as the specification becomes more complex. For this reason, we do not include them in the tables of this section, nor in the sequence-length comparison, and we provide their complete numerical results in C. Table 3: Performance comparison varying formula complexity. Results are averaged over 10 independent runs. Img. Acc: Symbol Grounding Accuracy; Seq. Acc: Sequence Classification Accuracy; Time: Logic Module Time per Epoch. Results in bold are statistically significantly better than all other methods (Wilcoxon, p<0.05p<0.05). Img. Acc. (%\%) ↑ Seq. Acc. (%\%) ↑ Time (s) ↓ Setting |||C| ∂ FuzzyA NeSyA ∂ FuzzyA NeSyA ∂ FuzzyA NeSyA MNIST Set1 2 99.9 99.9 99.9 99.8 99.8 99.8 0.04 0.17 0.17 4 97.4 97.4 97.4 98.9 98.9 99.0 0.05 0.33 0.40 6 95.7 95.6 91.3 98.3 98.3 97.6 0.05 0.63 0.99 8 92.7 91.5 88.4 96.7 96.5 95.5 0.05 1.97 5.08 MNIST Set2 2 99.9 99.9 99.9 99.8 99.9 99.9 0.05 0.17 0.15 4 97.4 97.3 97.3 99.0 99.1 99.0 0.06 0.34 0.37 6 95.0 95.0 95.0 98.1 98.2 98.1 0.06 0.69 0.88 8 92.7 92.7 92.7 98.0 98.0 97.9 0.07 4.86 10.38 F-MNIST Set1 2 100.0 100.0 100.0 100.0 100.0 100.0 0.04 0.14 0.30 4 97.8 97.9 97.9 98.7 98.7 98.8 0.05 0.35 0.59 6 91.7 91.7 92.0 95.5 95.3 95.7 0.05 0.69 1.27 8 86.0 85.6 83.9 93.2 93.2 92.8 0.05 2.24 5.42 F-MNIST Set2 2 99.9 99.9 99.9 99.9 99.9 99.9 0.05 0.14 0.14 4 98.0 98.0 98.0 99.0 98.9 99.0 0.05 0.25 0.34 6 90.9 91.1 91.0 96.2 96.3 96.1 0.06 0.71 0.87 8 85.1 85.6 85.4 96.2 96.2 96.4 0.07 4.83 10.49 7.2.1 Answer to RQ2 Figure 7: Comparison of symbol grounding accuracy (left) and logic module time per epoch (right) across number of classes ||∈2,4,6,8|C|∈\2,4,6,8\. Values are averaged across all four experimental settings (formula set × image dataset). We answer RQ2 by discussing the two evaluation directions. Varying formula complexity Table 3 and Figure 7 report classification performance as the number of classes |||C| increases from 22 to 88. At ||=2|C|=2, all three neurosymbolic methods achieve near-perfect grounding accuracy across all settings, with almost no statistically significant differences. As the symbolic complexity grows, the three methods remain competitive with no single method consistently superior across all configurations. The only exceptions are two isolated configurations in which NeSyA attains a statistically significant advantage over both competitors, although with always less than half a percentage point in difference. The absolute accuracy of all three neurosymbolic methods decreases as |||C| grows, indicating that the increase in specification complexity makes the weakly supervised grounding problem harder for every method considered. The two purely neural baselines fail to learn a valid symbol grounding, as their grounding accuracy collapses towards random-guess performance as |||C| grows (Figure 7, left), confirming that explicit temporal logic injection is necessary for this weakly supervised task. Table 4: Performance comparison varying sequence length. Results are averaged over 10 independent runs. Img. Acc: Symbol Grounding Accuracy; Seq. Acc: Sequence Classification Accuracy; Time: Logic Module Time per Epoch. Results in bold are statistically significantly better than all other methods (Wilcoxon, p<0.05p<0.05). Img. Acc. (%\%) ↑ Seq. Acc. (%\%) ↑ Time (s) ↓ |||C| Len ∂ FuzzyA NeSyA ∂ FuzzyA NeSyA ∂ FuzzyA NeSyA 4 20 97.9 97.9 98.0 97.7 97.8 97.8 0.007 0.41 0.57 40 97.9 98.0 98.0 98.0 98.1 98.1 0.007 0.74 1.14 60 97.9 98.1 98.1 97.2 97.7 97.6 0.007 1.09 1.74 80 98.0 97.9 97.9 98.0 98.2 98.2 0.007 1.46 2.33 100 98.0 98.0 98.1 98.1 98.0 98.0 0.008 1.83 2.91 120 97.9 97.9 97.9 98.0 98.2 98.0 0.008 2.21 3.53 140 98.1 98.1 98.1 98.9 99.0 99.0 0.008 2.59 4.12 160 97.7 97.7 97.8 97.3 97.2 97.3 0.008 2.96 4.74 180 97.9 98.0 98.0 98.4 98.5 98.5 0.008 3.31 5.34 200 97.7 97.8 97.8 97.6 97.5 97.6 0.008 3.69 5.89 8 20 95.8 95.3 95.8 95.3 94.0 95.5 0.16 2.32 3.43 40 96.0 95.6 96.0 94.5 92.8 94.7 0.30 4.73 6.90 60 95.6 94.7 95.4 94.7 92.2 94.1 0.44 7.12 10.45 80 95.7 94.6 95.4 95.0 93.5 94.2 0.62 9.56 13.93 100 95.6 94.2 95.6 94.5 90.1 94.2 0.79 11.91 17.39 120 95.5 93.6 94.7 93.0 90.0 91.8 0.95 14.35 21.00 140 96.1 93.7 95.5 93.5 88.9 91.8 1.11 16.72 24.64 160 95.8 94.2 95.3 94.0 90.5 92.9 1.25 19.09 27.87 180 95.8 88.3 95.3 93.7 83.2 91.8 1.42 21.58 29.88 200 95.6 92.2 95.0 94.7 86.3 92.9 1.57 23.84 32.58 Figure 8: Comparison of symbol grounding accuracy (top row) and logic module time per epoch (bottom row) across sequence lengths varying from 20 to 200. Left column: temporal specification with ||=4|C|=4 classes. Right column: temporal specification with ||=8|C|=8 classes. Lines represent the mean over 10 independent runs; shaded bands indicate the range between the minimum and maximum values. Time is shown on a logarithmic scale. Varying sequence length Table 4 and Figure 8 report the performance as the sequence length increases from 20 to 200, following the setup described in Section 6.1.2. With ||=4|C|=4, all three methods achieve high and stable grounding accuracy across the entire range of sequence lengths. NeSyA achieves statistically significant improvements over both competitors at several lengths; however, the absolute differences never exceed 0.20.2 percentage points. In practice, the three methods are on par in terms of accuracy on this specification. In contrast, with ||=8|C|=8, at short sequence lengths ∂ and NeSyA achieve comparable grounding accuracy. However, as the sequence length increases, both FuzzyA and NeSyA show performance degradation and fall behind ∂ in both image and sequence classification accuracy, with statistically significant differences appearing from length 60 onward. Such degradation is not visible for ∂ , which maintains stable grounding accuracy across the entire range of sequence lengths. For clarity, the two purely neural baselines are omitted from Figure 8 and Table 4, as they do not reach a valid solution on this task (grounding accuracy close to a random-guess classifier across all sequence lengths). Their complete numerical results are reported in C. These results demonstrate that ∂ attains classification performance on par with both DFA-based competitors, and outperforms them in the most demanding configurations, characterized by high formula complexity and sequence length, at both the symbol grounding and sequence classification levels. Section 7.3 shows that this level of accuracy is attained at a fraction of the computational cost required by the DFA-based competitors. Having answered RQ2, the remainder of this subsection discusses these results in greater depth and provides further insights. 7.2.2 Discussion on RQ2 We have shown in the previous section that the relative performance of the three neurosymbolic methods is not uniform across the experimental configurations. On most of them, all three methods are statistically indistinguishable; on a few, NeSyA achieves a small but statistically significant advantage; while on the most demanding configurations, ∂ consistently achieves higher accuracy. Understanding which characteristics of the logic module are responsible for these performance differences, and why such differences appear under certain configurations, remains an open question. The end-of-training accuracy metrics, while sufficient to answer RQ2, do not provide the evidence needed to identify the mechanism that produces such differences. Comparing the methods at the level of the gradient rather than of the final accuracy appears to be a promising starting point. Feeding the same perception output to each logic module and inspecting the gradient it propagates back (both in terms of magnitude and how it is distributed across the timesteps) for different configurations may provide more insight about the learning signal each module provides. The interest in this direction is motivated by the gradient-level discussion of Section 7.1.2, where the differences between the fuzzy semantics can be attributed to the gradient properties of the underlying operators. However, whether this suffices as an explanation for the choice of the logic module is itself an open question, and we leave its investigation to future work. 7.3 RQ3: Computational Scalability We now focus on the computational cost of the compared methods, measured as the time per training epoch spent by the temporal module. For the neurosymbolic methods this is the logic module, while for the two purely neural baselines it is the GRU or the Transformer encoder that replaces it. This metric isolates the overhead introduced by the temporal module, as the perception module is identical across all methods. 7.3.1 Answer to RQ3 By looking at Table 3 and Table 4, we observe that ∂ is the fastest of the three neurosymbolic methods in every configuration tested and the margin increases with both dimensions of the evaluation (i.e., formula complexity and sequence length). Along the formula-complexity direction (Figure 7), the time required by ∂ is essentially invariant with respect to the complexity of the specification: going from ||=2|C|=2 to ||=8|C|=8, i.e. from one to four conjoined sub-formulas, produces negligible overhead (from 0.040.04 s to 0.070.07 s per epoch). Both DFA-based competitors, in contrast, grow super-linearly with |||C|. Their cost increases by roughly an order of magnitude in a single step from ||=6|C|=6 to ||=8|C|=8. Along the sequence-length direction (Figure 8), all three neurosymbolic methods scale linearly with the sequence length. However, at the longest sequences tested, ∂ is faster than both competitors by between one and nearly three orders of magnitude, with NeSyA consistently the slowest of the two. Moreover, the reported cost accounts only for training. The cost of constructing the automaton, which ∂ does not incur at all, is excluded, so the reported gap is a lower bound. The two purely neural baselines attain lower per-epoch times, as they avoid any symbolic computation, but their speed is not meaningful here since they do not learn the task. 7.3.2 Discussion on RQ3 Both FuzzyA and NeSyA rely on the explicit construction of a finite-state automaton from the ltlf formula, which carries two distinct limitations. First, the automaton must be built before training, and its size is, in the worst case, double-exponential in the size of the ltlf formula [9]. This is what the formula-complexity direction measures. Since Φ conjoins K=||/2K=|C|/2 sub-formulas (see Section 6.1.1), a larger |||C| means a larger formula, hence a larger automaton, and a fast growth of the computational cost of both methods. Second, the automaton’s states valuation is computed recurrently over the sequence, each timestep depending on the previous one, so the evaluation is inherently sequential, preventing parallelisation over time. On top of this common cost, the two methods differ in how each transition is evaluated. FuzzyA evaluates each transition guard according to fuzzy semantics, and updates the vector of fuzzy truth values over the automaton states. NeSyA instead computes the probability that each transition guard is satisfied, and these probabilities determine the transition matrix by which the state distribution is updated. The probabilistic semantics is exact and avoids the approximation introduced by fuzzy evaluation. It comes, however, at a computational cost, as weighted model counting must be carried out for every transition at every timestep. This is what makes NeSyA the most computationally demanding of the compared methods. This is reflected in the observation that the gap between FuzzyA and NeSyA remains stable as the sequence length grows, and widens as the temporal specification becomes more complex (for which larger automata are built). ∂ incurs neither cost, as it avoids the automaton altogether and evaluates the temporal specification directly on the perception output. The cost of the evaluation is governed by the size of the temporal specification Φ , and not by that of an automaton which may be double-exponentially larger. Combined with the accuracy result of Section 7.2, these results show that direct fuzzy evaluation of ltlf specifications achieves comparable or higher classification accuracy than DFA-based methods while requiring a fraction of the computational cost. 8 Threats to Validity In this section, we highlight some limitations of the current study. Synthetic dataset The input sequences used in the evaluation are synthetically built. This choice is deliberate as synthetic generation provides full control over the independent variables of the evaluation, namely formula complexity and sequence length. Control over such variables is necessary to fully assess the performance and scalability of the temporal reasoning component, and to stress-test it under increasingly demanding conditions. To the best of our knowledge, no real-world temporal datasets annotated with ground-truth ltlf satisfaction labels exist at the scale required by our experimental evaluation. The image datasets used for the perceptual component, MNIST and Fashion-MNIST, are standard benchmarks adopted across temporal neurosymbolic works [29, 20]. Selection of temporal specifications The temporal specifications used in the evaluation are built as conjunctions or simple combinations of declare patterns, rather than ltlf formulas with deeply nested temporal operators. This was done, in line with previous work [29], due to the fact that declare patterns are a set of well-established temporal constraints widely adopted in the process mining literature [10]. The conjunctive structure of the temporal formula allows control of its complexity through the number of sub-formulas K, which serves as the independent variable in the formula-complexity experiments (Section 6.1.1). Design choices No exhaustive hyperparameter search was performed. The training configuration, including optimizer (Adam), learning rate (10−410^-4), and number of training epochs, directly follows configurations of a related temporal neurosymbolic benchmark [20]. All the compared methods share the same training configuration to ensure fair comparison. The train/test partition follows a standard 80/20 split. 9 Conclusions This paper introduced ∂ , a differentiable framework for injecting ltlf specifications into neural sequence classifiers while avoiding intermediate automata-based representations. The method evaluates temporal formulas directly on finite traces through various fuzzy semantics, allowing the symbolic specification to contribute to the training objective while keeping the perception module’s architecture unchanged. Alongside the framework, we provided a systematic study of fuzzy temporal semantics, highlighting how the choice of semantics affects both the interpretation of temporal operators and the resulting learning behaviour. Moreover, ∂ was evaluated on classification tasks under different temporal specifications, formula complexities, numbers of classes, and sequence lengths, and compared against DFA-based neurosymbolic baselines. The results show that different fuzzy semantics lead to different predictive behaviour, confirming that the choice of semantics is an important design decision in temporal NeSy frameworks. At the same time, ∂ achieves comparable or better classification performance while being substantially more efficient than existing state-of-the-art techniques. This advantage is especially clear as the specifications become more complex, since ∂ avoids the automaton-size blow-up that can affect DFA-based methods. Overall, our findings demonstrate that direct fuzzy evaluation of ltlf formulas provides a practical and scalable alternative to automata-based integration of temporal knowledge. In addition, the theoretical analysis of fuzzy temporal semantics and the evaluation protocol introduced in this work provide a foundation for the development and systematic assessment of future temporal neurosymbolic systems. Future work will investigate richer temporal logics, larger and more realistic benchmarks, and methods for jointly learning or refining temporal specifications from data. Acknowledgements This work is funded by the project TRUStworthy predictive models for Temporal Event Data (TRUSTED), start-up fund, Free University of Bozen-Bolzano. References Andreoni et al. [2025] Andreoni, R., Buliga, A., Daniele, A., Ghidini, C., Montali, M., Ronzani, M., 2025. T-ILR: a neurosymbolic integration for LTLf, in: Gilpin, L.H., Giunchiglia, E., Hitzler, P., van Krieken, E. (Eds.), Proceedings of The 19th International Conference on Neurosymbolic Learning and Reasoning (NeSy 2025), 8-10 September 2025, Santa Cruz, CA, USA, PMLR. p. 252–265. URL: https://proceedings.mlr.press/v284/andreoni25a.html. Badreddine et al. [2022] Badreddine, S., d’Avila Garcez, A.S., Serafini, L., Spranger, M., 2022. Logic tensor networks. Artif. Intell. 303, 103649. doi:10.1016/J.ARTINT.2021.103649. Baier and Katoen [2008] Baier, C., Katoen, J., 2008. Principles of model checking. MIT Press. Besold et al. [2021] Besold, T.R., d’Avila Garcez, A.S., Bader, S., Bowman, H., Domingos, P.M., Hitzler, P., Kühnberger, K., Lamb, L.C., Lima, P.M.V., de Penning, L., Pinkas, G., Poon, H., Zaverucha, G., 2021. Neural-symbolic learning and reasoning: A survey and interpretation, in: Hitzler, P., Sarker, M.K. (Eds.), Neuro-Symbolic Artificial Intelligence: The State of the Art. IOS Press. Frontiers in Artificial Intelligence and Applications, p. 1–51. URL: https://doi.org/10.3233/FAIA210348, doi:10.3233/FAIA210348. Cho et al. [2014] Cho, K., van Merrienboer, B., Gülçehre, Ç., Bahdanau, D., Bougares, F., Schwenk, H., Bengio, Y., 2014. Learning phrase representations using RNN encoder-decoder for statistical machine translation, in: Moschitti, A., Pang, B., Daelemans, W. (Eds.), Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing, EMNLP 2014, October 25-29, 2014, Doha, Qatar, A meeting of SIGDAT, a Special Interest Group of the ACL, ACL. p. 1724–1734. URL: https://doi.org/10.3115/v1/d14-1179, doi:10.3115/V1/D14-1179. Daniele et al. [2023] Daniele, A., van Krieken, E., Serafini, L., van Harmelen, F., 2023. Refining neural network predictions using background knowledge. Mach. Learn. 112, 3293–3331. URL: https://doi.org/10.1007/s10994-023-06310-3, doi:10.1007/S10994-023-06310-3. De Giacomo et al. [2020] De Giacomo, G., Iocchi, L., Favorito, M., Patrizi, F., 2020. Restraining bolts for reinforcement learning agents, in: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, AAAI Press. p. 13659–13662. doi:10.1609/AAAI.V34I09.7114. De Giacomo et al. [2014] De Giacomo, G., Masellis, R.D., Montali, M., 2014. Reasoning on LTL on finite traces: Insensitivity to infiniteness, in: Brodley, C.E., Stone, P. (Eds.), Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada, AAAI Press. p. 1027–1033. doi:10.1609/AAAI.V28I1.8872. De Giacomo and Vardi [2013] De Giacomo, G., Vardi, M.Y., 2013. Linear temporal logic and linear dynamic logic on finite traces, in: Rossi, F. (Ed.), IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, IJCAI/AAAI. p. 854–860. URL: http://w.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997. Di Ciccio and Montali [2022] Di Ciccio, C., Montali, M., 2022. Declarative process specifications: Reasoning, discovery, monitoring, in: Process Mining Handbook. Springer Science and Business Media. volume 448, p. 45. doi:10.1007/978-3-031-08848-34. Di Francescomarino et al. [2017] Di Francescomarino, C., Ghidini, C., Maggi, F.M., Petrucci, G., Yeshchenko, A., 2017. An eye into the future: Leveraging a-priori knowledge in predictive business process monitoring, in: Carmona, J., Engels, G., Kumar, A. (Eds.), Business Process Management - 15th International Conference, BPM 2017, Barcelona, Spain, September 10-15, 2017, Proceedings, Springer. p. 252–268. doi:10.1007/978-3-319-65000-5\_15. Diligenti et al. [2017] Diligenti, M., Gori, M., Saccà, C., 2017. Semantic-based regularization for learning and inference. Artif. Intell. 244, 143–165. doi:10.1016/J.ARTINT.2015.08.011. Donadello et al. [2025] Donadello, I., Felli, P., Innes, C., Maggi, F.M., Montali, M., 2025. LTL-based conformance checking of fuzzy event logs. Process Sci. 2. URL: https://doi.org/10.1007/s44311-025-00020-w, doi:10.1007/S44311-025-00020-W. Frigeri et al. [2014] Frigeri, A., Pasquale, L., Spoletini, P., 2014. Fuzzy time in linear temporal logic. ACM Trans. Comput. Log. 15, 1–22. Garcez and Lamb [2003] Garcez, A., Lamb, L., 2003. Reasoning about time and knowledge in neural symbolic learning systems, in: Thrun, S., Saul, L., Schölkopf, B. (Eds.), Advances in Neural Information Processing Systems, MIT Press. URL: https://proceedings.neurips.c/paper_files/paper/2003/file/347665597cbfaef834886adbb848011f-Paper.pdf. Klir and Yuan [1995] Klir, G.J., Yuan, B., 1995. Fuzzy sets and fuzzy logic - theory and applications. Prentice Hall. van Krieken et al. [2022] van Krieken, E., Acar, E., van Harmelen, F., 2022. Analyzing differentiable fuzzy logic operators. Artif. Intell. 302, 103602. URL: https://doi.org/10.1016/j.artint.2021.103602, doi:10.1016/J.ARTINT.2021.103602. Lamine and Kabanza [2000] Lamine, K., Kabanza, F., 2000. History checking of temporal fuzzy logic formulas for monitoring behavior-based mobile robots, in: ICTAI, p. 312–319. LeCun et al. [1998] LeCun, Y., Bottou, L., Bengio, Y., Haffner, P., 1998. Gradient-based learning applied to document recognition. Proc. IEEE 86, 2278–2324. doi:10.1109/5.726791. Lorello et al. [2025] Lorello, L.S., Lippi, M., Melacci, S., 2025. A neuro-symbolic framework for sequence classification with relational and temporal knowledge, in: Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, August 16-22, 2025, ijcai.org. p. 5833–5841. URL: https://doi.org/10.24963/ijcai.2025/649, doi:10.24963/IJCAI.2025/649. Maene and Raedt [2023] Maene, J., Raedt, L.D., 2023. Soft-unification in deep probabilistic logic, in: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (Eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023. URL: http://papers.nips.c/paper_files/paper/2023/hash/bf215fa7fe70a38c5e967e59c44a99d0-Abstract-Conference.html. Manginas et al. [2025] Manginas, N., Paliouras, G., Raedt, L.D., 2025. Nesya: Neurosymbolic automata, in: Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, August 16-22, 2025, ijcai.org. p. 5950–5958. URL: https://doi.org/10.24963/ijcai.2025/662, doi:10.24963/IJCAI.2025/662. Manhaeve et al. [2018] Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., Raedt, L.D., 2018. Deepproblog: Neural probabilistic logic programming, in: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (Eds.), Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, p. 3753–3763. URL: https://proceedings.neurips.c/paper/2018/hash/dc5d637ed5e62c36ecb73b654b05ba2a-Abstract.html. Perotti et al. [2014] Perotti, A., d’Avila Garcez, A., Boella, G., 2014. Neural networks for runtime verification, in: 2014 International Joint Conference on Neural Networks (IJCNN), p. 2637–2644. doi:10.1109/IJCNN.2014.6889961. Pnueli [1977] Pnueli, A., 1977. The temporal logic of programs, in: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, IEEE Computer Society. p. 46–57. doi:10.1109/SFCS.1977.32. von Rüden et al. [2023] von Rüden, L., Mayer, S., Beckh, K., Georgiev, B., Giesselbach, S., Heese, R., Kirsch, B., Pfrommer, J., Pick, A., Ramamurthy, R., Walczak, M., Garcke, J., Bauckhage, C., Schuecker, J., 2023. Informed machine learning - A taxonomy and survey of integrating prior knowledge into learning systems. IEEE Trans. Knowl. Data Eng. 35, 614–633. URL: https://doi.org/10.1109/TKDE.2021.3079836, doi:10.1109/TKDE.2021.3079836. Umili et al. [2023a] Umili, E., Argenziano, F., Barbin, A., Capobianco, R., 2023a. Visual reward machines, in: d’Avila Garcez, A.S., Besold, T.R., Gori, M., Jiménez-Ruiz, E. (Eds.), Proceedings of the 17th International Workshop on Neural-Symbolic Learning and Reasoning, La Certosa di Pontignano, Siena, Italy, July 3-5, 2023, CEUR-WS.org. p. 255–267. URL: https://ceur-ws.org/Vol-3432/paper23.pdf. Umili and Capobianco [2024] Umili, E., Capobianco, R., 2024. Deepdfa: Automata learning through neural probabilistic relaxations, in: Endriss, U., Melo, F.S., Bach, K., Diz, A.J.B., Alonso-Moral, J.M., Barro, S., Heintz, F. (Eds.), ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain - Including 13th Conference on Prestigious Applications of Intelligent Systems (PAIS 2024), IOS Press. p. 1051–1058. URL: https://doi.org/10.3233/FAIA240596, doi:10.3233/FAIA240596. Umili et al. [2023b] Umili, E., Capobianco, R., De Giacomo, G., 2023b. Grounding LTLf specifications in image sequences, in: Marquis, P., Son, T.C., Kern-Isberner, G. (Eds.), Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, p. 668–678. doi:10.24963/KR.2023/65. Umili et al. [2024] Umili, E., Licks, G.P., Patrizi, F., 2024. Enhancing deep sequence generation with logical temporal knowledge, in: Giacomo, G.D., Fionda, V., Fournier, F., Ielo, A., Limonad, L., Montali, M. (Eds.), Proceedings of the 3rd International Workshop on Process Management in the AI Era (PMAI 2024) co-located with 27th European Conference on Artificial Intelligence (ECAI 2024), Santiago de Compostela, Spain, October 19, 2024, CEUR-WS.org. p. 23–34. URL: https://ceur-ws.org/Vol-3779/paper4.pdf. Vaswani et al. [2017] Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L., Polosukhin, I., 2017. Attention is all you need, in: Guyon, I., von Luxburg, U., Bengio, S., Wallach, H.M., Fergus, R., Vishwanathan, S.V.N., Garnett, R. (Eds.), Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, p. 5998–6008. URL: https://proceedings.neurips.c/paper/2017/hash/3f5e243547dee91fbd053c1c4a845a-Abstract.html. Xiao et al. [2017] Xiao, H., Rasul, K., Vollgraf, R., 2017. Fashion-mnist: a novel image dataset for benchmarking machine learning algorithms. arXiv:cs.LG/1708.07747. Xu et al. [2018] Xu, J., Zhang, Z., Friedman, T., Liang, Y., den Broeck, G.V., 2018. A semantic loss function for deep learning with symbolic knowledge, in: Dy, J.G., Krause, A. (Eds.), Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, July 10-15, 2018, PMLR. p. 5498–5507. URL: http://proceedings.mlr.press/v80/xu18h.html. Appendix A Implementation Details of Baselines This appendix provides details regarding the implementation of the baseline methods, FuzzyA [29] and NeSyA [22], considered in our comparative analysis. We adopted specific baseline implementations to ensure a fair comparison in terms of computational efficiency and adherence to the theoretical foundations of each method. A.1 FuzzyA For the FuzzyA baseline, we adopted the implementation provided in the LTLZinc codebase [20], which, in addition to batched sequence evaluation, differs from the original implementation [29] in two aspects. First, at each timestep the automaton’s state distribution is renormalized through a softmax before the next transition step. Second, the training objective is a binary cross-entropy loss between the sum of the fuzzy values assigned to the accepting states and the sequence label, rather than the loss function used in [29]. The original loss function combines the fuzzy values of the accepting states through a fuzzy exclusive-or (for positive examples) and through a conjunction of negations (for negative examples). We verified empirically that, under identical perception module and training parameters, the LTLZinc implementation variant yields substantially higher symbol-grounding accuracy and sequence classification accuracy than the original implementation variant on our benchmark. Moreover, the change of loss function accounts for most of the gap (C). The core mechanism of this approach remains unchanged and involves building a propositional formula for each potential next state of the automaton. The formula is built as the disjunction of all valid incoming transitions, where a transition is defined as the conjunction of the previous state and the corresponding transition guard. Each previous state in the automaton is treated as a logical variable. These formulas are evaluated by mapping conjunctions to multiplications and disjunctions to algebraic summations. A.2 NeSyA For the NeSyA baseline, we did not utilize the implementation found in the LTLZinc codebase, as it compiles state variables and transition guards together into a single logical circuit and can be computationally inefficient for large automata. Instead, we implemented the architecture described in the original NeSyA work [22]. In this setup, only the transition guards are compiled into d-DNNF circuits to enable exact probabilistic reasoning over the input symbols. At each timestep, these compiled circuits are evaluated to populate a transition matrix. The probability over the states is updated via matrix multiplication between the previous state distribution and the transition matrix. Appendix B Experimental Setup Details This appendix provides the training configuration, model architecture, and dataset construction details used across all experiments. Perception module All methods share the same convolutional neural network as the perception module, ensuring that differences in performance are to be attributed exclusively to the temporal reasoning component. The network consists of two convolutional layers with 32 and 64 filters respectively (kernel size 5×55× 5), each followed by a ReLU activation and 2×22× 2 max-pooling. The convolutional layers are followed by two fully connected layers of size 1024 and |C||C|, with ReLU activation and dropout (p=0.5p=0.5) applied after the first fully connected layer. The input images are resized to 32×3232× 32 pixels. Since each image represents a single class, mutual exclusivity of the class atoms holds. The output logits are passed through a softmax layer, so that the per-class truth values of each observation are normalized to sum to one. Training configuration All models are trained with the Adam optimizer using a fixed learning rate of 10−410^-4 and a batch size of 64. The loss function is a binary cross-entropy between the predicted satisfaction value and the ground-truth sequence label y∈0,1y∈\0,1\. In the formula-complexity experiments (Section 6.1.1), the training runs for 50 epochs. In the sequence-length experiments (Section 6.1.2), training is limited to 30 epochs. The reduced number of training epochs reflects the substantially higher per-epoch training time of DFA-based methods on long sequences. Since a fair comparison requires all methods to train for the same number of epochs, we selected a number of epochs that remains feasible for the slowest method under evaluation. Each configuration is repeated over 10 independent runs with distinct random seeds. Dataset construction For each experimental configuration, we generate a dataset of 1000 sequences. Each sequence is constructed by independently sampling, at every timestep and for each of the S=3S=3 streams, a class label uniformly at random from 0,…,|C|−1\0,…,|C|-1\ and retrieving a corresponding image from the MNIST or Fashion-MNIST training set. The ground-truth sequence label is computed by evaluating the ltlf specification Φ on the crisp symbolic trace obtained by the sampled class label. The resulting dataset is partitioned into 80% training and 20% test sets; the test set is held out and never observed during training. Hardware and software All experiments were performed on a single NVIDIA RTX A6000 GPU (48 GB), using PyTorch 2.3.1 with CUDA 12.1. Appendix C Complete Experimental Results Results in Section 7 report only the representative temporal neurosymbolic methods (∂ with fltlPf_f^P semantics, FuzzyA, and NeSyA). Here we report the complete results for all evaluated methods: the three ∂ semantics (Product, Gödel, Łukasiewicz), T-ILR, FuzzyA (both the LTLZinc variant used throughout the paper and the original implementation, see A), NeSyA, and the two purely neural baselines (GRU and Transformer). Tables 5 and 6 report the formula-complexity experiment (Section 6.1.1) and Tables 7 and 8 the sequence-length experiment (Section 6.1.2). All values are averaged over 10 runs and use the same protocol as the main text; bold marks statistical significance over all other methods (Wilcoxon signed-rank, p<0.05p<0.05). Table 5: Full results varying formula complexity on MNIST, averaged over 10 runs. Img. Acc.: Symbol Grounding Accuracy; Seq. Acc.: Sequence Classification Accuracy; Time: Logic Module Time per Epoch. Results in bold are statistically significantly better than all other methods (Wilcoxon, p<0.05p<0.05). Method Set 1 Set 2 |||C|: 2 4 6 8 2 4 6 8 Img. Acc. (%) ↑ ∂ (Product) 99.9 97.4 95.7 92.7 99.9 97.4 95.0 92.7 ∂ (Gödel) 99.9 60.8 32.7 22.8 99.9 59.2 29.6 16.3 ∂ (Łukasiewicz) 90.1 58.4 46.2 35.4 99.9 62.6 57.1 42.0 T-ILR 99.9 60.8 32.7 22.8 99.9 59.2 29.6 16.3 FuzzyA 99.9 97.4 95.6 91.5 99.9 97.3 95.0 92.7 FuzzyA (orig.) 70.2 44.5 22.8 22.0 99.9 37.2 17.9 17.2 NeSyA 99.9 97.4 91.3 88.4 99.9 97.3 95.0 92.7 GRU 65.8 34.5 20.5 15.5 63.1 30.8 19.0 18.4 Transformer 70.5 34.9 23.8 18.4 65.8 34.7 24.6 21.0 Seq. Acc. (%) ↑ ∂ (Product) 99.8 98.9 98.3 96.7 99.8 99.0 98.1 98.0 ∂ (Gödel) 99.8 87.2 90.2 82.8 99.8 93.0 86.8 87.3 ∂ (Łukasiewicz) 93.3 88.5 90.8 87.3 99.8 93.5 87.9 88.5 T-ILR 99.8 87.2 90.2 82.8 99.8 93.0 86.8 87.3 FuzzyA 99.8 98.9 98.3 96.5 99.9 99.1 98.2 98.0 FuzzyA (orig.) 79.5 86.5 87.0 86.7 99.8 88.2 85.5 86.2 NeSyA 99.8 99.0 97.6 95.5 99.9 99.0 98.1 97.9 GRU 99.5 87.0 87.3 82.5 79.4 88.1 85.5 86.8 Transformer 99.3 89.0 90.7 87.5 99.5 91.5 88.3 88.8 Time (s) ↓ ∂ (Product) 0.042 0.045 0.048 0.050 0.050 0.059 0.061 0.065 ∂ (Gödel) 0.003 0.006 0.008 0.011 0.050 0.052 0.054 0.061 ∂ (Łukasiewicz) 0.004 0.007 0.010 0.013 0.050 0.055 0.055 0.065 T-ILR 0.098 0.295 0.279 0.479 0.099 0.158 0.221 0.297 FuzzyA 0.166 0.327 0.628 1.97 0.167 0.345 0.694 4.86 FuzzyA (orig.) 0.089 0.247 0.697 1.91 0.087 0.209 0.625 4.64 NeSyA 0.165 0.397 0.990 5.08 0.154 0.367 0.878 10.38 GRU 0.002 0.002 0.002 0.002 0.003 0.003 0.002 0.002 Transformer 0.014 0.012 0.012 0.013 0.012 0.012 0.012 0.012 Table 6: Full results varying formula complexity on Fashion-MNIST, averaged over 10 runs. Img. Acc.: symbol grounding accuracy; Seq. Acc.: sequence classification accuracy; Time: Logic Module Time per Epoch. Results in bold are statistically significantly better than all other methods (Wilcoxon, p<0.05p<0.05). Method Set 1 Set 2 |||C|: 2 4 6 8 2 4 6 8 Img. Acc. (%) ↑ ∂ (Product) 100.0 97.8 91.7 86.0 99.9 98.0 90.9 85.1 ∂ (Gödel) 100.0 76.0 34.0 23.6 99.9 52.7 32.0 16.7 ∂ (Łukasiewicz) 89.9 55.9 47.6 40.0 99.9 79.2 45.8 33.0 T-ILR 100.0 76.0 34.0 23.6 99.9 52.7 32.0 16.7 FuzzyA 100.0 97.9 91.7 85.6 99.9 98.0 91.1 85.6 FuzzyA (orig.) 54.0 41.6 28.3 23.5 84.8 27.0 25.2 15.9 NeSyA 100.0 97.9 92.0 83.9 99.9 98.0 91.0 85.4 GRU 70.4 33.5 20.6 18.2 54.5 29.3 17.8 17.3 Transformer 71.6 35.5 28.0 19.4 71.2 34.6 24.8 18.4 Seq. Acc. (%) ↑ ∂ (Product) 100.0 98.7 95.5 93.2 99.9 99.0 96.2 96.2 ∂ (Gödel) 100.0 89.0 89.9 85.5 99.9 91.0 87.3 89.2 ∂ (Łukasiewicz) 93.3 87.1 89.5 85.8 99.9 93.1 88.9 89.3 T-ILR 100.0 89.0 89.9 85.5 99.9 91.0 87.3 89.2 FuzzyA 100.0 98.7 95.3 93.2 99.9 98.9 96.3 96.2 FuzzyA (orig.) 67.0 82.7 87.0 86.3 90.0 88.5 87.2 87.6 NeSyA 100.0 98.8 95.7 92.8 99.9 99.0 96.1 96.4 GRU 99.8 86.0 87.8 83.3 73.0 88.5 88.7 88.2 Transformer 99.7 89.0 89.2 86.5 99.5 91.8 90.0 90.6 Time (s) ↓ ∂ (Product) 0.042 0.046 0.048 0.050 0.051 0.053 0.062 0.068 ∂ (Gödel) 0.003 0.006 0.008 0.010 0.050 0.053 0.058 0.062 ∂ (Łukasiewicz) 0.004 0.007 0.009 0.012 0.048 0.053 0.053 0.062 T-ILR 0.135 0.222 0.321 0.427 0.134 0.246 0.256 0.239 FuzzyA 0.144 0.353 0.690 2.24 0.137 0.245 0.714 4.83 FuzzyA (orig.) 0.095 0.201 0.637 1.89 0.113 0.266 0.624 4.66 NeSyA 0.299 0.595 1.27 5.42 0.135 0.339 0.867 10.49 GRU 0.003 0.004 0.003 0.003 0.003 0.002 0.002 0.002 Transformer 0.018 0.021 0.025 0.026 0.012 0.012 0.012 0.012 Table 7: Full results varying the sequence length, ||=4|C|=4, averaged over 10 runs. Img. Acc.: Symbol Grounding Accuracy; Seq. Acc.: Sequence Classification Accuracy; Time: Logic Module Time per Epoch. Bold marks a value statistically significantly better than all other methods (Wilcoxon, p<0.05p<0.05). Sequence length Method 20 40 60 80 100 120 140 160 180 200 Img. Acc. (%) ↑ ∂ (Product) 97.9 97.9 97.9 98.0 98.0 97.9 98.1 97.7 97.9 97.7 ∂ (Gödel) 43.5 35.0 47.2 35.9 49.9 48.5 41.1 55.4 55.0 54.8 ∂ (Łukasiewicz) 72.9 92.7 87.8 92.1 85.5 78.6 82.6 86.6 91.1 81.2 T-ILR 43.5 35.0 47.2 35.9 49.9 48.5 41.1 55.4 55.0 54.8 FuzzyA 97.9 98.0 98.1 97.9 98.0 97.9 98.1 97.7 98.0 97.8 FuzzyA (orig.) 22.7 22.7 22.8 22.8 22.8 22.7 22.7 22.8 22.7 22.8 NeSyA 98.0 98.0 98.1 97.9 98.1 97.9 98.1 97.8 98.0 97.8 GRU 44.9 41.1 36.9 43.0 39.4 41.4 39.5 37.8 36.3 38.0 Transformer 46.6 36.3 42.3 39.0 36.0 38.4 43.2 32.8 34.3 44.0 Seq. Acc. (%) ↑ ∂ (Product) 97.7 98.0 97.2 98.0 98.1 98.0 98.9 97.3 98.4 97.6 ∂ (Gödel) 70.6 64.7 72.0 68.5 74.2 75.0 70.1 75.5 71.9 75.0 ∂ (Łukasiewicz) 84.4 90.0 89.5 91.2 87.8 85.7 86.8 87.3 90.2 84.8 T-ILR 70.6 64.7 72.0 68.5 74.2 75.0 70.1 75.5 71.9 75.0 FuzzyA 97.8 98.1 97.7 98.2 98.0 98.2 99.0 97.2 98.5 97.5 FuzzyA (orig.) 32.7 36.2 35.5 35.1 33.5 34.9 35.7 35.2 37.5 37.5 NeSyA 97.8 98.1 97.6 98.2 98.0 98.0 99.0 97.3 98.5 97.6 GRU 78.4 79.1 78.3 81.1 79.5 79.2 79.2 77.5 76.5 78.2 Transformer 80.4 78.3 76.9 74.1 73.5 71.0 67.2 69.5 62.8 67.2 Time (s) ↓ ∂ (Product) 0.007 0.007 0.007 0.008 0.007 0.008 0.008 0.008 0.008 0.008 ∂ (Gödel) 0.025 0.026 0.023 0.026 0.023 0.023 0.022 0.025 0.024 0.027 ∂ (Łukasiewicz) 0.026 0.028 0.025 0.028 0.024 0.025 0.025 0.027 0.025 0.027 T-ILR 0.340 0.760 1.32 2.02 2.86 3.84 4.93 6.38 7.63 9.25 FuzzyA 0.410 0.740 1.09 1.46 1.83 2.21 2.59 2.96 3.31 3.69 FuzzyA (orig.) 0.351 0.686 1.03 1.39 1.75 2.11 2.44 2.80 3.20 3.50 NeSyA 0.568 1.14 1.74 2.33 2.91 3.53 4.12 4.74 5.34 5.89 GRU 0.004 0.004 0.004 0.004 0.005 0.005 0.005 0.005 0.006 0.006 Transformer 0.016 0.018 0.015 0.017 0.020 0.023 0.028 0.031 0.033 0.039 Table 8: Full results varying the sequence length, ||=8|C|=8, averaged over 10 runs. Img. Acc.: Symbol Grounding Accuracy; Seq. Acc.: Sequence Classification Accuracy; Time: Logic Module Time per Epoch. Results in bold are statistically significantly better than all other methods (Wilcoxon, p<0.05p<0.05). Sequence length Method 20 40 60 80 100 120 140 160 180 200 Img. Acc. (%) ↑ ∂ (Product) 95.8 96.0 95.6 95.7 95.6 95.5 96.1 95.8 95.8 95.6 ∂ (Gödel) 17.5 17.1 17.7 16.7 17.3 15.1 14.8 16.4 15.2 14.9 ∂ (Łukasiewicz) 14.6 14.6 14.6 14.6 14.5 14.5 14.5 14.5 14.6 14.6 T-ILR 17.5 17.1 17.7 16.7 17.3 15.1 14.8 16.4 15.2 14.9 FuzzyA 95.3 95.6 94.7 94.6 94.2 93.6 93.7 94.2 88.3 92.2 FuzzyA (orig.) 15.5 24.8 39.1 18.9 42.6 38.5 29.0 45.7 45.1 51.2 NeSyA 95.8 96.0 95.4 95.4 95.6 94.7 95.5 95.3 95.3 95.0 GRU 16.1 17.1 16.7 18.2 16.2 16.1 17.7 17.0 16.1 17.2 Transformer 21.4 22.7 21.2 19.6 21.0 21.3 17.0 17.9 21.4 19.2 Seq. Acc. (%) ↑ ∂ (Product) 95.3 94.5 94.7 95.0 94.5 93.0 93.5 94.0 93.7 94.7 ∂ (Gödel) 57.0 55.1 53.4 54.1 54.1 53.3 50.3 53.8 52.2 52.6 ∂ (Łukasiewicz) 50.8 52.9 51.0 47.9 51.5 51.5 47.4 50.8 50.9 51.6 T-ILR 57.0 55.1 53.4 54.1 54.1 53.3 50.3 53.8 52.2 52.6 FuzzyA 94.0 92.8 92.2 93.5 90.1 90.0 88.9 90.5 83.2 86.3 FuzzyA (orig.) 50.8 58.8 71.2 59.7 71.0 68.3 65.8 70.0 71.4 71.7 NeSyA 95.5 94.7 94.1 94.2 94.2 91.8 91.8 92.9 91.8 92.9 GRU 54.0 54.5 53.7 55.4 54.5 51.6 54.5 55.1 52.8 56.4 Transformer 63.2 63.8 61.7 57.1 54.5 58.1 53.4 54.2 55.2 53.0 Time (s) ↓ ∂ (Product) 0.161 0.300 0.441 0.624 0.790 0.953 1.11 1.25 1.42 1.57 ∂ (Gödel) 0.053 0.098 0.134 0.186 0.229 0.275 0.354 0.393 0.420 0.465 ∂ (Łukasiewicz) 0.064 0.109 0.137 0.185 0.230 0.276 0.324 0.371 0.421 0.471 T-ILR 0.911 1.90 2.66 2.74 3.02 3.62 4.29 4.95 6.95 8.04 FuzzyA 2.32 4.73 7.12 9.56 11.91 14.35 16.72 19.09 21.58 23.84 FuzzyA (orig.) 3.06 4.93 7.94 9.57 12.27 13.04 15.32 17.33 19.00 21.20 NeSyA 3.43 6.90 10.45 13.93 17.39 21.00 24.64 27.87 29.88 32.58 GRU 0.004 0.004 0.004 0.005 0.005 0.006 0.006 0.006 0.006 0.006 Transformer 0.014 0.014 0.014 0.017 0.020 0.022 0.027 0.029 0.032 0.039