Publications

2023

• Enumerating Regular Languages with Bounded Delay
  
  • Amarilli Antoine
  • Monet Mikaël
  , 2023. We study the task, for a given language $L$, of enumerating the (generally infinite) sequence of its words, without repetitions, while bounding the delay between two consecutive words. To allow for delay bounds that do not depend on the current word length, we assume a model where we produce each word by editing the preceding word with a small edit script, rather than writing out the word from scratch. In particular, this witnesses that the language is orderable, i.e., we can write its words as an infinite sequence such that the Levenshtein edit distance between any two consecutive words is bounded by a value that depends only on the language. For instance, $(a+b)^*$ is orderable (with a variant of the Gray code), but $a^* + b^*$ is not. We characterize which regular languages are enumerable in this sense, and show that this can be decided in PTIME in an input deterministic finite automaton (DFA) for the language. In fact, we show that, given a DFA $A$, we can compute in PTIME automata $A_1, \ldots, A_t$ such that $L(A)$ is partitioned as $L(A_1) \sqcup \ldots \sqcup L(A_t)$ and every $L(A_i)$ is orderable in this sense. Further, we show that the value of $t$ obtained is optimal, i.e., we cannot partition $L(A)$ into less than $t$ orderable languages. In the case where $L(A)$ is orderable (i.e., $t=1$), we show that the ordering can be produced by a bounded-delay algorithm: specifically, the algorithm runs in a suitable pointer machine model, and produces a sequence of bounded-length edit scripts to visit the words of $\L(A)$ without repetitions, with bounded delay -- exponential in $|A|$ -- between each script. In fact, we show that we can achieve this while only allowing the edit operations push and pop at the beginning and end of the word, which implies that the word can in fact be maintained in a double-ended queue. By contrast, when fixing the distance bound $d$ between consecutive words and the number of classes of the partition, it is NP-hard in the input DFA $A$ to decide if $L(A)$ is orderable in this sense, already for finite languages. Last, we study the model where push-pop edits are only allowed at the end of the word, corresponding to a case where the word is maintained on a stack. We show that these operations are strictly weaker and that the slender languages are precisely those that can be partitioned into finitely many languages that are orderable in this sense. For the slender languages, we can again characterize the minimal number of languages in the partition, and achieve bounded-delay enumeration. (10.4230/LIPIcs.STACS.2023.8)
  DOI : 10.4230/LIPIcs.STACS.2023.8
• Program Semantics and Verification Technique for AI-Centred Programs
  
  • Rajaona Fortunat
  • Boureanu Ioana
  • Malvone Vadim
  • Belardinelli Francesco
  , 2023, 14000, pp.473-491. We give a general-purpose programming language in which programs can reason about their own knowledge. To specify what these intelligent programs know, we define a “program epistemic” logic, akin to a dynamic epistemic logic for programs. Our logic properties are complex, including programs introspecting into future state of affairs, i.e., reasoning now about facts that hold only after they and other threads will execute. To model aspects anchored in privacy, our logic is interpreted over partial observability of variables, thus capturing that each thread can “see” only a part of the global space of variables. We verify program-epistemic properties on such AI-centred programs. To this end, we give a sound translation of the validity of our program-epistemic logic into first-order validity, using a new weakest-precondition semantics and a book-keeping of variable assignment. We implement our translation and fully automate our verification method for well-established examples using SMT solvers. (10.1007/978-3-031-27481-7_27)
  DOI : 10.1007/978-3-031-27481-7_27
• Field Trial of High-Resolution Distributed Fiber Sensing over Multicore Fiber in Metropolitan Area with Construction Work Detection using Advanced MIMO-DAS
  
  • Guerrier Sterenn
  • Mecozzi Antonio
  • Dorize Christian
  • Antonelli Cristian
  • Dallachiesa Lauren
  • Mardoyan Haïk
  • Awwad Élie
  • Orsuti Daniele
  • Palmieri Luca
  • Mazur Mikael
  • Hayashi Tetsuya
  • Ryf Roland
  • Renaudier Jérémie
  , 2023, pp.W1J.5. We demonstrate a successful field trial of MIMO-DAS over multicore fiber (MCF) allowing for accurate localization of acoustic events in the city of L’Aquila, Italy. We show a 2m spatial resolution and 1mHz-380Hz acoustic bandwidth. (10.1364/OFC.2023.W1J.5)
  DOI : 10.1364/OFC.2023.W1J.5
• Jitter Compensation Mechanism for Dynamic Deterministic Networks
  
  • Soudais Guillaume
  • Graba Tarik
  • Mathieu Yves
  • Bigo Sebastien
  , 2023, pp.Th3D.2. We compensate jitter between any two unsynchronized endpoints by tracking their clocks and re-creating flows by retiming packets. After implementation over FPGA, we achieve ~10ms synchronization setup time with no more than 70ns jitter. (10.1364/OFC.2023.Th3D.2)
  DOI : 10.1364/OFC.2023.Th3D.2
• MIMO Coding Technique for PDL and Crosstalk Mitigation in Optical Transmission Systems
  
  • Abouseif Akram
  • Rekaya Ben Othman Ghaya
  • Jaouën Yves
  , 2023, pp.W3E.3. We propose a new coding technique, called IQ-code, to mitigate PDL and inter-channel crosstalk on optical fiber transmission. We obtain 0.3-0.5 dB OSNR gain at FEC limit for any number of sub-carrier by simple ZF decoding. (10.1364/OFC.2023.W3E.3)
  DOI : 10.1364/OFC.2023.W3E.3
• Reconstruction of trajectories of athletes using computer vision models and kinetic analysis
  
  • Gan Qi
  • Nguyen Sao Mai
  • Fenaux Eric
  • Clémençon Stéphan
  • El Yacoubi Mounim
  • Jelassi Ons
  , 2023, pp.443997. Athlete's pose acquisition and analysis is promising to provide coaches with details of athletes performance and thus help to improve athletes' performances with more detailed supervision from coaches. Compared with traditional ways of acquiring an athlete's gesture, such as using wearable sensors, computer vision technology has advantages of low-cost, high-efficient and non-intrusive. This paper aims to bridge these two fields, by reconstructing athletes' trajectory using monocular (i.e. single-camera-shot) videos. Under a few assumptions that are applicable to most of the sports of athletics, we proposed a method combining computer vision techniques and physics laws to reconstruct athletes' trajectories from monocular videos. The method first estimates 3D pose of athletes from video inputs, then performs kinematic analysis on estimated poses to reconstruct the trajectories of athletes. We tested this algorithm on videos from the triple jump finals of the 2016 Olympics in Rio de Janeiro. We achieved a best performance with 9.1% mean average error when using ground-truth foot-ground contact signal and 21.4% mean average error when using predicted foot-ground contact signal.
• Reconstruction of trajectories of athletes using computer vision models and Kinetic analysis
  
  • Gan Qi
  • Nguyen Sao Mai
  • Clémençon Stéphan
  • El Yacoubi Mounim
  • Jelassi Ons
  , 2023. Athlete's pose acquisition and analysis is promising to provide coaches with details of athletes performance and thus help to improve athletes' performances with more detailed supervision from coaches. Compared with traditional ways of acquiring an athlete's gesture, such as using wearable sensors, computer vision technology has advantages of low-cost, high-efficient and non-intrusive. This paper aims to bridge these two fields, by reconstructing athletes' trajectory using monocular (i.e. single-camera-shot) videos. Under a few assumptions that are applicable to most of the sports of athletics, we proposed a method combining computer vision techniques and physics laws to reconstruct athletes' trajectories from monocular videos. The method first estimates 3D pose of athletes from video inputs, then performs kinematic analysis on estimated poses to reconstruct the trajectories of athletes. We tested this algorithm on videos from the triple jump finals of the 2016 Olympics in Rio de Janeiro. We achieved a best performance with 9.1% mean average error when using ground-truth foot-ground contact signal and 21.4% mean average error when using predicted foot-ground contact signal.
• Abstract Categorical Logic
  
  • Aiguier Marc
  • Bloch Isabelle
  Logica Universalis, Springer Verlag, 2023, 17 (1), pp.23-67. (10.1007/s11787-022-00320-w)
  DOI : 10.1007/s11787-022-00320-w
• Unsupervised Music Source Separation Using Differentiable Parametric Source Models
  
  • Schulze-Forster Kilian
  • Richard Gaël
  • Kelley Liam
  • Doire Clement
  • Badeau Roland
  IEEE/ACM Transactions on Audio, Speech and Language Processing, Institute of Electrical and Electronics Engineers, 2023, 31, pp.1276-1289. Supervised deep learning approaches to underdetermined audio source separation achieve state-of-the-art performance but require a dataset of mixtures along with their corresponding isolated source signals. Such datasets can be extremely costly to obtain for musical mixtures. This raises a need for unsupervised methods. We propose a novel unsupervised model-based deep learning approach to musical source separation. Each source is modelled with a differentiable parametric source-filter model. A neural network is trained to reconstruct the observed mixture as a sum of the sources by estimating the source models' parameters given their fundamental frequencies. At test time, soft masks are obtained from the synthesized source signals. The experimental evaluation on a vocal ensemble separation task shows that the proposed method outperforms learning-free methods based on nonnegative matrix factorization and a supervised deep learning baseline. Integrating domain knowledge in the form of source models into a data-driven method leads to high data efficiency: the proposed approach achieves good separation quality even when trained on less than three minutes of audio. This work makes powerful deep learning based separation usable in scenarios where training data with ground truth is expensive or nonexistent (10.1109/TASLP.2023.3252272)
  DOI : 10.1109/TASLP.2023.3252272
• A stochastic Gauss-Newton algorithm for regularized semi-discrete optimal transport
  
  • Bercu Bernard
  • Bigot Jérémie
  • Gadat Sébastien
  • Siviero Emilia
  Information and Inference: A Journal of the IMA, 2023, Vol. 12 (n° 1), pp.390-447. We introduce a new second order stochastic algorithm to estimate the entropically regularized optimal transport cost between two probability measures. The source measure can be arbitrary chosen, either absolutely continuous or discrete, while the target measure is assumed to be discrete. To solve the semi-dual formulation of such a regularized and semi-discrete optimal transportation problem, we propose to consider a stochastic Gauss-Newton algorithm that uses a sequence of data sampled from the source measure. This algorithm is shown to be adaptive to the geometry of the underlying convex optimization problem with no important hyperparameter to be accurately tuned. We establish the almost sure convergence and the asymptotic normality of various estimators of interest that are constructed from this stochastic Gauss-Newton algorithm. We also analyze their non-asymptotic rates of convergence for the expected quadratic risk in the absence of strong convexity of the underlying objective function. The results of numerical experiments from simulated data are also reported to illustrate the nite sample properties of this Gauss-Newton algorithm for stochastic regularized optimal transport, and to show its advantages over the use of the stochastic gradient descent, stochastic Newton and ADAM algorithms. (10.1093/imaiai/iaac014)
  DOI : 10.1093/imaiai/iaac014
• An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
  
  • Belardinelli Francesco
  • Ferrando Angelo
  • Malvone Vadim
  Artificial Intelligence (AIJ), Elsevier, 2023, 316, pp.103847. We investigate the verification of Multi-Agent Systems against strategic properties expressed in Alternating-time Temporal Logic under the assumptions of imperfect information and perfect recall. To this end, we develop a three-valued semantics for concurrent game structures upon which we define an abstraction method. We prove that concurrent game structures with imperfect information admit perfect information abstractions that preserve three-valued satisfaction. Furthermore, to deal with cases in which the value of a specification is undefined, we develop a novel automata-theoretic technique for the linear-time logic (LTL), then apply it to finding “failure” states. The latter can then be fed into a refinement procedure, thus providing a sound, albeit incomplete, verification method. We illustrate the overall procedure in a variant of the Train Gate Controller scenario and a simple voting protocol under imperfect information and perfect recall. We also present an implementation of our procedure and provide preliminary experimental results. (10.1016/j.artint.2022.103847)
  DOI : 10.1016/j.artint.2022.103847
• Superpouvoirs
  
  • Zayana Karim
  • Braun Nathalie
  CultureMath, ENS, 2023. On prête volontiers des pouvoirs aux fleurs, à l'argent, à l'amour-ô combien, ou aux super-héros de notre enfance. Mais n'oublions pas les mathématiques ! Elles aussi en sont dotées, et de surnaturels. Il n'est point besoin de savoir qu'elles détiennent, à travers l'ensemble R des réels, la puissance du continu pour s'en apercevoir. Dès le cycle 3 en effet, l'élève se frotte à ses premières puissances, puis il découvre un peu plus tard (et nous reverrons comment ci-après), au lycée, qu'il peut ainsi transformer le chiffre 0 en 1 comme un alchimiste changerait du plomb en or. Tour d'horizon des définitions et propriétés de l'exponentiation, et quelques petits trucs pour les retenir...
• The multichannel maximum-likelihood (MCML) method: a new approach for infrasound detection and wave parameter estimation
  
  • Poste B.
  • Charbit M.
  • Le Pichon A.
  • Listowski C.
  • Roueff François
  • Vergoz J.
  Geophysical Journal International, Oxford University Press (OUP), 2023, 232 (2), pp.1099-1112. We are presenting a new and novel approach to the detection and parameter estimation of infrasonic signals. Our approach is based on the likelihood function derived from a multisensor stochastic model expressed in different frequency channels. Using the likelihood function, we determine, for the detection problem, the generalized likelihood ratio (GLR) and for the estimation of the slowness vector, the maximum likelihood estimation (MLE). We establish new asymptotic results (i) for the GLR under the null hypothesis leading to the computation of the corresponding p-value and (ii) for the MLE by focusing on the two wave parameters: backazimuth and horizontal trace velocity. The multichannel maximum-likelihood (MCML) detection and estimation method is implemented in the time–frequency domain in order to avoid the presence of interfering signals. Extensive simulations with synthetic signals show that MCML outperforms the state-of-the-art multichannel correlation detector algorithms like the progressive multichannel correlation in terms of detection probability and false alarm rate in poor signal-to-noise ratio scenarios. We also illustrate the use of the MCML on real data from the International Monitoring System and show how the improved performances of this new method lead to a refined analysis of events in accordance with expert knowledge. (10.1093/gji/ggac377)
  DOI : 10.1093/gji/ggac377
• Character Recognition in Byzantine Seals with Deep Neural Networks
  
  • Rageau Théophile
  • Likforman-Sulem Laurence
  • Fiandrotti Attilio
  • Eyharabide Victoria
  • Caseau Béatrice
  • Cheynet Jean-Claude
  , 2024. Seals are small coin-shaped artifacts, mostly made of lead, held with strings to seal letters. This work presents the first attempt towards automatic reading of text on Byzantine seal images. Byzantine seals are generally decorated with iconography on the obverse side and Greek text on the reverse side. Text may include the sender’s name, position in the Byzantine aristocracy, and elements of prayers. Both text and iconography are precious literary sources that wait to be exploited electronically, so the development of computerized systems for interpreting seals images is of paramount importance. This work’s contribution is hence a deep, two-stages, character reading pipeline for transcribing Byzantine seal images. A first deep convolutional neural network (CNN) detects characters in the seal (character localization). A second convolutional network reads the localized characters (character classification). Finally, a diplomatic transcription of the seal is provided by post-processing the two network outputs. We provide an experimental evaluation of each CNN in isolation and both CNNs in combination. All performances are evaluated by cross-validation. Character localization achieves a mean average precision (mAP@0.5) greater than 0.9. Classification of characters cropped from ground truth bounding boxes achieves Top-1 accuracy greater than 0.92. End-to-end evaluation shows the efficiency of the proposed approach when compared to the SoTA for similar tasks.
• Tail Inverse Regression: dimension reduction for prediction of extremes
  
  • Aghbalou Anass
  • Portier François
  • Sabourin Anne
  • Zhou Chen
  , 2023. We consider the problem of supervised dimension reduction with a particular focus on extreme values of the target Y ∈ R to be explained by a covariate vector X ∈ R p. The general purpose is to define and estimate a projection on a lower dimensional subspace of the covariate space which is sufficient for predicting exceedances of the target above high thresholds. We propose an original definition of Tail Conditional Independence which matches this purpose. Inspired by Sliced Inverse Regression (SIR) methods, we develop a novel framework (TIREX, Tail Inverse Regression for EXtreme response) in order to estimate an extreme sufficient dimension reduction (SDR) space of potentially smaller dimension than that of a classical SDR space.We prove the weak convergence of tail empirical processes involved in the estimation procedure and we illustrate the relevance of the proposed approach on simulated and real world data. (10.48550/arXiv.2108.01432)
  DOI : 10.48550/arXiv.2108.01432
• Automated design of photonic quantum circuits
  
  • Yao Yuan
  , 2023. Quantum computing is based on quantum physics phenomena, such assuperposition and entanglement and it promises to revolutionize the world of computing. Photonics is a prominent platform for realizing fault-tolerant quantum computing. It has various qualities: working at room temperature, large-scale manufacturability using existing foundries for silicon chips, and compatibility with optical communication to interconnect different quantum computers.Our main goal is to automate the design of photonic quantum circuits and of their interconnects. Before a real photonic quantum computer can be manufactured, it is essential to numerically simulate and optimize the corresponding circuits, which in practice are built out of Gaussian components such as squeezers, beam-splitters, phase shifters, and homodyne detectors. To achieve universality, we also need non-Gaussian effects, which can be supplied by photon-number-resolving detectors. We design circuits from this toolbox and optimize them for various applications using various gradient descent algorithms, some of which we adapted to our purpose.The main contributions are:1. In photonics, Fock space and phase space representations are both useful formalisms to describe quantum states and transformations. We introduce a unified Fock space representation of all Gaussian objects in terms of a single linear recurrence relation that can recursively generate their Fock space amplitudes.2. We find the composition rule of Gaussian operations in Fock space, which allows us to obtain the correct global phase when composing Gaussian operations (normally absent from the phase space description), and therefore to extend our model to states that can be written as linear combinations of Gaussians.3. Our recursive representation is differentiable, allowing for a straightforward computation of the gradients of a Gaussian object with respect to any parametrization. We then adapt gradient-based optimization to the problem of circuit optimization. We implement a Euclidean optimizer (i.e. which doesn't take the geometry of parameter space unto account) in order to optimize each parametrized component of a circuit. Then we study two ways to account for geometry: first we apply Riemannian optimization, by combining all the Gaussian operations into a global transformation and following a geodesic on the manifold of symplectic matrices to find the optimized transformation, at which point we can decompose it back into fundamental optical components. Second, we generalize a complex version of the natural gradient for optical quantum circuits to accelerate the convergence of the training process.4. We also give some optimal task-based strategies for using our recurrence relations. New algorithms are proposed to calculate, for instance, the amplitudes of a mixed state and the transformation matrix of interferometers. In addition, we derive a fast contraction algorithm for Gaussian transformations, which allows us to "fuse" the computation of the amplitudes of a Gaussian transformation and its action on any state.5. With the simulation on differentiable photonic quantum circuits built from the recurrence relation, we can design photonic quantum circuits automatically. We give state preparation as the first example; we find circuits that can produce high-fidelity states in a reasonable time, such as cat states with mean photon number 4, fidelity 99.38%, and success probability 7.3%. We can also optimize a 216-mode interferometer to make a Gaussian Boson Sampling experiment harder to spoof.6. We made this work available in various open-source libraries: TheWalrus, StrawberryFields, Poenta, and MrMustard.
• How to Find Good Coalitions to Achieve Strategic Objectives
  
  • Ferrando Angelo
  • Malvone Vadim
  , 2023, 1, pp.105-113. Alternating-time Temporal Logic (ATL) is an extension of the temporal logic CTL in which we can quantify over coalition of agents. In the model checking process, the coalitions in a given formula are fixed, so it is assumed that the user knows the specific coalitions to be checked. Unfortunately, this is not true in general. In this paper, we present an extension of MCMAS, a well-known tool that handles ATL model checking, in which we give the ability to a user to characterise the coalition quantifiers with respect to two main features: the number of agents involved in the coalitions and how to group such agents. Moreover, we give details of such extensions and provide experimental results. (10.5220/0011778700003393)
  DOI : 10.5220/0011778700003393
• A Game Theoretic Approach to Attack Graphs
  
  • Catta Davide
  • Di Stasio Antonio
  • Leneutre Jean
  • Malvone Vadim
  • Murano Aniello
  , 2023, 1, pp.347-354. An attack graph is a succinct representation of all the paths in an open system that allow an attacker to enter a forbidden state (e.g., a resource), besides any attempt of the system to prevent it. Checking system vulnerabil- ity amounts to verifying whether such paths exist. In this paper we reason about attack graphs by means of a game-theoretic approach. Precisely, we introduce a suitable game model to represent the interaction between the system and the attacker and an automata-based solution to show the absence of vulnerability. (10.5220/0011776900003393)
  DOI : 10.5220/0011776900003393
• Look At Me, No Replay! SurpriseNet: Anomaly Detection Inspired Class Incremental Learning
  
  • Lee Anton
  • Zhang Yaqian
  • Gomes Heitor Murilo
  • Bifet Albert
  • Pfahringer Bernhard
  , 2023, pp.4038--4042. Continual learning aims to create artificial neural networks capable of accumulating knowledge and skills through incremental training on a sequence of tasks. The main challenge of continual learning is catastrophic interference, wherein new knowledge overrides or interferes with past knowledge, leading to forgetting. An associated issue is the problem of learning "cross-task knowledge," where models fail to acquire and retain knowledge that helps differentiate classes across task boundaries. A common solution to both problems is "replay," where a limited buffer of past instances is utilized to learn cross-task knowledge and mitigate catastrophic interference. However, a notable drawback of these methods is their tendency to overfit the limited replay buffer. In contrast, our proposed solution, SurpriseNet, addresses catastrophic interference by employing a parameter isolation method and learning cross-task knowledge using an auto-encoder inspired by anomaly detection. SurpriseNet is applicable to both structured and unstructured data, as it does not rely on image-specific inductive biases. We have conducted empirical experiments demonstrating the strengths of SurpriseNet on various traditional vision continual-learning benchmarks, as well as on structured data datasets. Source code made available at https://doi.org/10.5281/zenodo.8247906 and https://github.com/tachyonicClock/SurpriseNet-CIKM-23 (10.1145/3583780.3615236)
  DOI : 10.1145/3583780.3615236
• On Line Secure Elements: Deploying High Security Keystores and Personal HSMs
  
  • Urien Pascal
  , 2023, pp.450-455. This paper presents innovative approach to deploy secure elements providing cryptographic resources in TCP/IP environment. The main idea is to execute in secure element, TLS1.3 server, secured by 256 bits pre-shared-key. All cryptographic resources are protected by TLS-PSK sessions. In the user plane the secure element is a TLS server, what enables to define uniform resource identifier (URI) for embedded resources. The user is optionally equipped with access card (TLS identity module) that stores procedures working with PSK. The security level may be increased by the use of dedicated terminal, similar to payment terminal, which protects dual factor authentication. We present two open platforms: keystore devices hosting preconfigured TLS-SE secure elements, and personal HSM supporting on-demand TLS-SE applications. Finally we detail some performance elements. (10.1109/ICNC57223.2023.10074066)
  DOI : 10.1109/ICNC57223.2023.10074066
• On Line Secure Elements: Deploying High Security Keystores and Personal HSMs
  
  • Urien Pascal
  , 2023, pp.450-455. This paper presents innovative approach to deploy secure elements providing cryptographic resources in TCP/IP environment. The main idea is to execute in secure element, TLS1.3 server, secured by 256 bits pre-shared-key. All cryptographic resources are protected by TLS-PSK sessions. In the user plane the secure element is a TLS server, what enables to define uniform resource identifier (URI) for embedded resources. The user is optionally equipped with access card (TLS identity module) that stores procedures working with PSK. The security level may be increased by the use of dedicated terminal, similar to payment terminal, which protects dual factor authentication. We present two open platforms: keystore devices hosting preconfigured TLS-SE secure elements, and personal HSM supporting on-demand TLS-SE applications. Finally we detail some performance elements. (10.1109/ICNC57223.2023.10074066)
  DOI : 10.1109/ICNC57223.2023.10074066
• It’s not Just What You Do but also When You Do It: Novel Perspectives for Informing Interactive Public Speaking Training
  
  • Biancardi Beatrice
  • Duan Yingjie
  • Chollet Mathieu
  • Clavel Chloé
  , 2023, pp.193-200. Most of the emerging public speaking training systems, while very promising, leverage temporal-aggregate features, which do not take into account the structure of the speech. In this paper, we take a different perspective, testing whether some well-known socio-cognitive theories, like first impressions or primacy and recency effect, apply in the distinct context of public speaking perception. We investigated the impact of the temporal location of speech slices (i.e., at the beginning, middle or end) on the perception of confidence and persuasiveness of speakers giving online movie reviews (the Persuasive Opinion Multimedia dataset). Results show that, when considering multi-modality, usually the middle part of speech is the most informative. Additional findings also suggest the interest to leverage local interpretability (by computing SHAP values) to provide feedback directly, both at a specific time (what speech part?) and for a specific behaviour modality or feature (what behaviour ?). This is a first step towards the design of more explainable and pedagogical interactive training systems. Such systems could be more efficient by focusing on improving the speaker’s most important behaviour during the most important moments of their performance, and by situating feedback at specific places within the total speech. (10.5220/0011680400003417)
  DOI : 10.5220/0011680400003417
• Hierarchical Design of Cyber-Physical Systems
  
  • Genius Daniela
  • Apvrille Ludovic
  , 2023, pp.117-124. Cyber-physical systems are based upon analog / digital hardware and software components. The splitting into functionalities and interaction between analog and digital parts should be considered as early as possible in the design phase, relying on formal verification or simulation. While many papers pretend to propose a modeling environment supporting them, only a few of them really address the different Models of Computation of these systems because they strongly differ. The paper explains how to generate a combined SystemC/SystemC AMS virtual prototype of the analog and mixed-signal parts of CPS directly from a SysML model featuring whole parts of CPS, thus reconciling near-circuit precision with more abstract analog and digital models. (10.5220/0011654400003402)
  DOI : 10.5220/0011654400003402
• A Hierarchical Design Tool for SystemC AMS
  
  • Genius Daniela
  • Apvrille Ludovic
  , 2024, 2106, pp.3-28. The splitting into functionalities and interaction between analog and digital parts should be considered as early as possible in the design phase. We extended this methodology in former work, in order to take cyber-physical systems, based upon analog / digital hardware and software components, into account. The Models of Computation in these systems are not frequently tackled by many researchers due to their significant differences. However, as we show in this article, a SysML model can be directly used to generate a virtual prototype representing both the analog and mixed-signal parts of cyber-physical systems. For this, we rely on a hierarchical methodology, as certain analog components demand highly detailed designs. In this study, we introduce the capability to perform extensive semi-automatic design space exploration for these parts as well. A way to achieve this is to use parameters to automatically adapt the number of subsystems considered in the prototype. (10.1007/978-3-031-66339-0_1)
  DOI : 10.1007/978-3-031-66339-0_1
• Mutation of Formally Verified SysML Models
  
  • Apvrille Ludovic
  • Sultan Bastien
  • Hotescu Oana
  • de Saqui-Sannes Pierre
  • Coudert Sophie
  , 2023. Model checking of SysML models contributes to detect design errors and to check design decisions against user requirements. Yet, each time a model is modified, formal verification must be performed again, which makes model evolution costly and hampers the use of agile development methods. Based on former contributions on dependency graphs, the paper proposes to facilitate updates (also called mutations) on models: whenever a mutation is performed on a model, the algorithms introduced in this paper can determine which proofs remain valid and which ones must be performed again. The main idea to reduce the proof obligation is to identify new paths that need to be re-verified. Our algorithm reuses the results of previous proofs as much as possible in order to lower the complexity of the proof. The paper focuses on reachability proofs. A real-time communication architecture based on TSN (Time Sensitive Networking) illustrates the approach and performance results are presented.