This article explores an enhanced method for solving high-frequency forward problem Partial Differential Equations (PDEs) using Physics-Informed Neural Networks (PINNs). While PINNs have demonstrated success across multiple domains, they often face challenges in accurately capturing high-frequency components due to the inherent "spectral bias" of neural networks, where the network tends to focus on low-frequency features. To overcome these limitations, we introduce a novel approach that utilizes spline interpolation for signal augmentation and frequency decomposition, followed by transfer learning to progressively incorporate higher-frequency components into the learning process. The proposed method ensures smoother loss landscapes, making it easier for the network to learn high-frequency components. The proposed method is evaluated using a well-known forced mass-spring system, demonstrating the enhanced ability to capture high-frequency dynamics compared to conventional PINN methods.

Formal verification of PLC programs requires transforming control logic into a mathematical model. Since PLC languages lack a formal semantics, multiple transformation methods exist, based on various code interpretations. This work introduces a novel approach leveraging Single Static Assignments (SSA) to ensure a faithful PLC code transformation while enhancing model checking scalability. By systematically tracking variable assignments, the method accurately captures execution dependencies and preserves control logic. Experimental results demonstrate promising improvements in verification efficiency.

PLC programs play a major role in the operation of automated systems, controlling and monitoring various industrial processes. Formal verification methods, notably model checking, have been extensively studied to ensure the proper functioning of PLC programs. To implement this verification method, various formal modeling approaches have been proposed. However, most of them are often complex and require extensive expertise for implementation. An alternative is proposed, aimed at simplifying the formalization process.

Despite advancements in their performance, cyber-physical systems remain susceptible to cyberattacks. This paper focuses on the turnout system in railway transportation infrastructure. For such systems, the data monitored is geographically dispersed, which makes it vulnerable: attackers may either conceal failures or trigger unnecessary maintenance decisions. To address this issue, a threat assessment paradigm is proposed in order to provide maintenance operators with a threat indicator based on field data. The method is developed and validated over a real railway turnout data set.

The Supervisory Control Theory (SCT) provides a formal framework for modeling Discrete-Event Systems (DES) and for controller synthesis, by distinguishing explicitly the non-controlled system from its specifications. Many extensions have been built on top of SCT, which continues to be extensively applied in the domain of DES design, and has given rise worldwide to many research projects. The events used as a central modeling artefact are the key to this success. However, the dynamics that can be modeled using SCT can only be designed in terms of event successions. This does not set a limit, in theory, but has leads to a practical drawback: expressing some specifications can become tedious. In this article we propose a new type of automata, meant to ease the expression of these specifications, while rigorously remaining within the discrete-event system control framework, relying on automata such as used by the Ramadge-Wonham theory.

This paper addresses the problem of scheduling through a visual, expressive and formal modeling approach, based on Timed Game Automata (TGA). The originality of the proposed approach lies in integrating various kinds of uncontrollability in the scheduling problem and also the ability of handling the sharing of multiple resources. This uncontrollable behaviors consist of the start time, the duration of the task and the failure occurrence in a schedule which are modeled by TGA. The models have the advantage of being directly exploitable by means of synthesis tools. To obtain the minimum makespan and optimal schedules as the result, a time-optimal reachability game is performed through Tiga tool. The obtained result for a scheduling example shows the huge difference in the obtained schedule with and without considering uncontrollable behaviors.

In this paper, the Optimal Discrete Controller Synthesis technique is applied in order to obtain an optimal routing scheme for Wireless Sensor Networks (WSNs). A centralized controller is automatically computed and it is then distributed in such the way to provide a local choice elements to each node to select its next-hop that can provide shortest, and more energy efficient routing paths towards the sink based in two criteria: minimizing the intermediate hop count and balancing the energy consumption over the entire network.

We investigate the implementation of supervisors generated by symbolic BDD-based Discrete Controller Synthesis (DCS). The implementation technique proposed is able to solve both control non-determinism and the structural incompatibility introduced by symbolic DCS. We highlight and illustrate interesting structural properties of the supervisor implementation. Our technique is illustrated on a reallife example modeling a System-on-chip component: a serial to parallel converter.