Neuro-Symbolic Learning from Temporal Sequences in Safety-Critical Systems

Abstract

Safety-critical systems have seldom been used as an application domain for neuro-symbolic AI, despite their inherent characteristics that combine generation and processing of raw data, coming from heterogeneous devices, with enforcement or discovery of properties, usually encoded as rules or constraints. In this paper, we consider the task of classifying sequences of perceptual stimuli collected from a safety-critical system, where safety-related properties are represented in the form of linear temporal logic formulae. Our preliminary results on a benchmarking framework for temporal reasoning show that this kind of problem can be extremely challenging, for both neural-only and temporal neuro-symbolic approaches.

1. Introduction

Neuro-Symbolic (NeSy) Artificial Intelligence (AI) aims to combine neural networks with symbolic approaches, with the goal of complementing the capability of the former to handle and learn from large data collections, with the expressivity of the latter in representing domain knowledge, typically in the form of rules, constraints, or logic facts [ 1 ]. Despite the growing interest in this research area, the successful applications of NeSy AI to real-world problems is widely recognized as one of the most urgent open challenges in the field [ 2 ]. Most of the existing literature in NeSy AI focuses on proof-of-concept implementations, proposed throughout the years in several domains, ranging from computer vision to knowledge base completion. Yet, the community is constantly looking for new benchmarks and tasks with a wider and stronger impact on society [ 3 ].

In this paper, we propose to consider the domain of safetycritical systems as a suitable scenario to test and apply NeSy techniques. Safety-critical systems (SCSs) are domains in which failure might produce significant damage to the system itself or to the environment, or even loss of life [ 4 ]. Typical application areas include healthcare, for critical tasks such as the monitoring of biomedical devices [ 5 ], transportation, as in the case of aircraft flight control systems [ 6 ], or space missions, for the detection of anomalies and cybersecurity vulnerabilities [ 7 ]. In most of these scenarios, safety must be ensured by assessing that the behaviour of the system is compliant with strict constraints, such as time constraints (e.g., tasks that must complete their executions within certain time limits) or logic constraints (e.g., events that must occur in a predefined sequential order) [ 8, 9 ]. Many formalisms can be used to model these systems, such as stochastic time Petri nets [ 10 ], deterministic or symbolic ifnite automata [ 11 ], linear temporal logic (ltl) [ 12 ], fault trees [ 13, 14 ] and others, with the aim of quantitatively evaluating dependability attributes [ 15, 16 ].

From the perspective of NeSy AI, SCSs represent an ideal setting to design novel benchmarks on real-world problems because it combines the availability of large data collections generated by physical devices interacting with the environment, with domain knowledge described via rules and constraints. Several NeSy tasks can be conceived in this setting, depending on whether domain knowledge is explicitly available or should rather be learned from examples, and the variables of interest are fully or partially observable [ 17 ]. In this paper, we propose to exploit NeSy AI approaches in the context of SCSs, in particular for the task of classifying sequences of perceptual stimuli according to their compliance to a certain ltl formula [ 18 ].

2. Case study

Consider an SCS made of two devices ( and ) characterized by ten possible states {0, . . . , 9} ∈ , each associated with a perceptual signature, in the form of audio spectrograms {0, . . . , 9} ∈ . Suppose this system must comply to a liveness property [ 19 ] ℱ , asserting that an event (“the sensor is in state 4”) registered by sensor must always be followed by another event (“the sensor is in state 7”), observed by sensor . Events can be tracked, by systematically evaluating the validity of a set of relational predicates , on the state of the system over time. The behavior described above can be represented compactly by the following specification: : = { : = {0, . . . , 9} , , : = {p() : = 4, q() : = 7} ℱ : = □(p() → ◇q()) This specification corresponds to an LTLZinc [ 18 ] problem, where is encoded as MiniZinc [ 20 ] constraints and ℱ is a linear temporal logic formula over finite domains ( ltlf ) [ 21 ]. This framework enables the design of experiments in diferent learning and reasoning scenarios, depending on what kind of knowledge is available at training time, and which element of the tuple ⟨ , , , ℱ ⟩ constitutes the learning objective. For example, in many cases, an SCS is designed with predefined specifications in mind, and it is therefore reasonable to assume prior knowledge about both and ℱ , but not the mapping ↦→ . Within this setting, a sequence classification task corresponds to predict whether a given sequence of perceptual stimuli along a discrete set of timesteps = {1, . . . , } satisfies ℱ or not, and it corresponds to the verification of ℱ within a given sequence , by neuro-symbolic means. In other cases, either Immediate Failure

Liveness Real-Time Response

NeSy Neural Random

NeSy Neural Random

NeSy Neural Random or ℱ could be unknown, and the sequence classification task would thus involve the induction of temporal safety properties directly from system traces: in these settings, the NeSy system is trained to discriminate between positive and negative sequences, without knowing neither ℱ nor .

3. Methodology

We address the sequence classification task exemplified in Section 2 by cascading multiple decisions, following the approach described in [ 18 ]. In particular, we employ a multistage pipeline (Figure 1) composed of the following subtasks: (ic) image classification, mapping data from each to the corresponding ; (cc) constraint classification, leveraging relational knowledge ; (nsp) next state prediction, leveraging temporal knowledge ℱ ; (sc) sequence classification, i.e., the final decision. Each stage is associated with a loss function, weighted by a corresponding hyper-parameter . IC and NSP are trained by means of categorical crossentropy, while CC and SC employ a binary cross-entropy loss.

4. Experiments

Using the LTLZinc framework,1 we generate three tasks, following well-known ltl patterns for safety-critical applications [22]. For each task, we assume three spectrogram 1https://github.com/continual-nesy/LTLZinc images , , , and the following constraint mapping : : p(, , ) : ( + ) ≡ mod 10; q(, , ) : all_different([, , ]); r(, , ) : ( < < ) ∨ ( > > ); s(, , ) : ̸= ∧ ( = ∨ = ).

Each task corresponds to a diferent safety-critical property ℱ : Immediate Failure p is false after r:

□(r → □¬p);

Liveness s always follows p:

□(p → ◇s); Real-Time Response s responds to p between q and r: □((q ∧ ○ ◇r) → (p → (¬r (s ∧ ¬r))) r). Datasets contain 1000 sequences (800 train, 100 validation, 100 test samples) of random length between 10 and 25 timesteps. Each timestep is associated with three RGB images sampled from the UrbanSound-Spectrogram dataset,2 resized to fit into an 224 × 224 image with white background. Images are augmented during training and inference, according to the original ResNet18 transforms [23]. The modular architecture of Figure 1 is initialized in two lfavors: Neural (ResNet18, Multi-layer Perceptron, Gated Recurrent Unit, red dashed blocks), and NeSy (ResNet18, Deep Problog [24], NeSy Automaton [25], green dashed blocks). After selecting optimal hyper-parameters (optimizer: Adam, learning rate: 10− 4, MLP: 64 neurons, GRU: 64 hidden units) on the simplified task (the one introduced in Sec. 2), we initialize the IC module with one epoch of pretraining on image labels only, then supervise every stage ( CC = NSP = SC = 1.0, IC = 0.1) for a maximum of 7 epochs.

Table 1 summarizes the results on the test set, evaluated on the best-performing epoch (selected by average accuracy across all modules, measured on the validation set). In general, it can be observed that, although both Neural and NeSy methods reach similar image classification performance, downstream objectives become increasingly dificult for the Neural-only method. Overall, the NeSy method achieves the best performance across all symbolic objectives for every task, even though there is margin for improvement. Knowledge availability can only partially compensate the challenging nature of this setting, as even

2https://github.com/mashrin/UrbanSound-Spectrogram

NeSy approaches struggle with harder formulae. Training behavior (not shown) indicates that this efect is caused by severe over-fitting at the NSP stage, in spite of good upstream generalization of the CC objective, highlighting optimization challenges of the NeSy Automaton module, in spite of full supervisions available.

These preliminary experiments show that, while significantly outperforming knowledge-agnostic, neural-only methods, in every explored task, and in spite of perfect knowledge availability, NeSy performance quickly degrades as temporal behavior increases in complexity. To successfully deploy NeSy temporal reasoners in safety-critical settings, it is crucial to boost their performance in a way which is not afected by temporal complexity, especially for real-world settings, where full supervisions are not available.

Acknowledgments

L.S.L. scholarship was funded by the Italian Ministry of University and Research (DM 351/2022, PNRR).

L.C. was supported by the European Union under the Italian National Recovery and Resilience Plan (NRRP) of NextGenerationEU, partnership on “Telecommunications of the Future” (PE00000001 - program “RESTART”).

M.L. was supported by CAI4DSA actions (Collaborative Explainable neuro-symbolic AI for Decision Support Assistant), PARTENARIATO ESTESO “Future Artificial Intelligence Research - FAIR”, SPOKE 1 “Human-Centered AI” Università di Pisa, CUP B13C23005640006. The scholarship by L.S.L. was funded by the Italian Ministry of University and Research (DM 351/2022, PNRR).

S.M. was supported by the University of Siena (Piano per lo Sviluppo della Ricerca - PSR 2024, F-NEW FRONTIERS 2024), under the project “TIme-driveN StatEful Lifelong Learning” (TINSELL) and also by the project “CONSTR: a COllectionless-based Neuro-Symbolic Theory for learning and Reasoning”, PARTENARIATO ESTESO “Future Artificial Intelligence Research - FAIR”, SPOKE 1 “HumanCentered AI” Università di Pisa, “NextGenerationEU”, CUP I53C22001380006. 4.1. Declaration on Generative AI The author(s) have not employed any Generative AI tools. [22] M. B. Dwyer, G. S. Avrunin, J. C. Corbett, Property specification patterns for finite-state verification, in: Proceedings of the second workshop on Formal methods in software practice, 1998, pp. 7–15. [23] K. He, X. Zhang, S. Ren, J. Sun, Deep residual learning for image recognition, in: Proceedings of the IEEE conference on computer vision and pattern recognition, 2016, pp. 770–778. [24] R. Manhaeve, S. Dumancic, A. Kimmig, T. Demeester, L. De Raedt, Deepproblog: Neural probabilistic logic programming, Advances in neural information processing systems 31 (2018). [25] E. Umili, R. Capobianco, G. De Giacomo, Grounding ltlf specifications in image sequences, in: Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, 2023, pp. 668–678.

References

[1] A. d. Garcez , L. C. Lamb , Neurosymbolic ai: The 3 rd wave , Artificial Intelligence Review 56 ( 2023 ) 12387 - 12406 .

[2] L. De Raedt , S. Dumančić , R. Manhaeve , G. Marra, From statistical relational to neural-symbolic artificial intelligence , in: Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence , 2021 , pp. 4943 - 4950 .

[3] R. Manhaeve , F. Giannini , M. Ali , D. Azzolini , A. Bizzarri , A. Borghesi , S. Bortolotti , L. De Raedt, D. Dhami , M. Diligenti , et al., Benchmarking in neuro-symbolic ai , in: Proceedings of The 4th International Joint Conference on Learning & Reasoning , 2024 .

[4] J. C. Knight , Safety critical systems: challenges and directions , in: Proceedings of the 24th international conference on software engineering , 2002 , pp. 547 - 550 .

[5] V. Vakhter , B. Soysal , P. Schaumont , U. Guler, Threat modeling and risk analysis for miniaturized wireless biomedical devices , IEEE Internet of Things Journal 9 ( 2022 ) 13338 - 13352 .

[6] A. J. Stolzer , R. L. Sumwalt , J. J. Goglia , Safety management systems in aviation , CRC Press, 2023 .

[7] L. Vessels , K. Hefner , D. Johnson, Cybersecurity risk assessment for space systems , in: 2019 IEEE Space Computing Conference (SCC) , IEEE, 2019 , pp. 11 - 19 .

[8] P. Graydon , I. Bate , Realistic safety cases for the timing of systems , The Computer Journal 57 ( 2014 ) 759 - 774 .

[9] F. M. Favarò , J. H. Saleh , Application of temporal logic for safety supervisory control and model-based hazard monitoring , Reliability Engineering & System Safety 169 ( 2018 ) 166 - 178 .

[10] L. Carnevali , L. Ridi , E. Vicario , A quantitative approach to input generation in real-time testing of stochastic systems , IEEE Transactions on Software Engineering 39 ( 2013 ) 292 - 304 .

[11] G. Giantamidis , S. Basagiannis , S. Tripakis , Eficient translation of safety ltl to dfa using symbolic automata learning and inductive inference , in: International Conference on Computer Safety, Reliability, and Security, Springer, 2020 , pp. 115 - 129 .

[12] W.-g. Ma, X. -h. Hei , An approach for design and formal verification of safety-critical software , in: 2010 International Conference on Computer Application and System Modeling (ICCASM 2010 ), volume 4 , IEEE, 2010 , pp. V4 - 264 .

[13] M. Roth , P. Liggesmeyer , Modeling and analysis of safety-critical cyber physical systems using state/event fault trees , in: SAFECOMP 2013-Workshop DECS (ERCIM/EWICS Workshop on Dependable Embedded and Cyber-physical Systems) of the 32nd International Conference on Computer Safety, Reliability and Security , 2013 , p. NA.

[14] E. Ruijters , M. Stoelinga , Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools , Computer science review 15 ( 2015 ) 29 - 62 .

[15] A. Maurya , D. Kumar , Reliability of safety-critical systems: A state-of-the-art review , Quality and Reliability Engineering International 36 ( 2020 ) 2547 - 2568 .

[16] L. Carnevali , S. Cerboni , L. Montecchi , E. Vicario, FaultFlow: an MDE Library for Dependability Evaluation of Component-Based Systems , IEEE Transactions on Dependable and Secure Computing 22 ( 2025 ) 3431 - 3448 .

[17] L. Carnevali , M. Lippi , Neuro-symbolic artificial intelligence for safety engineering , in: International Conference on Computer Safety, Reliability, and Security, Springer, 2024 , pp. 438 - 445 .

[18] L. S. Lorello , M. Lippi , S. Melacci , A neuro-symbolic framework for sequence classification with relational and temporal knowledge , International Joint Conference on Artificial Intelligence (IJCAI) ( 2025 ).

[19] B. Alpern , F. B. Schneider , Defining liveness, Information processing letters 21 ( 1985 ) 181 - 185 .

[20] N. Nethercote , P. J. Stuckey , R. Becket , S. Brand , G. J. Duck , G. Tack, Minizinc: Towards a standard cp modelling language , in: International Conference on Principles and Practice of Constraint Programming , Springer, 2007 , pp. 529 - 543 .

[21] G. De Giacomo , M. Y. Vardi , Linear temporal logic and linear dynamic logic on finite traces ., in: Ijcai , volume 13 , 2013 , pp. 854 - 860 .