In this study, we elaborate on the idea of parametric group consensus measures. Here, we employ the additive generators of Dombi t-norms to construct fuzzy entropies, which are then utilized to generate group consensus measures. Since these additive generators are single-parameter functions, the resulting group consensus measures are also single-parameter mappings. We demonstrate that, given a set of inputs from decision-makers, the group consensus measure behaves as a bounded and non-decreasing function of its parameter. With this in mind, we address the question of which parameter value yields a group consensus measure that most accurately reflects the average perceived consensus level of the group. Next, we present a necessary and sufficient condition for the existence of an optimal value of the parameter in question, and provide algorithmic procedures to find it.
The Search and Rescue Problem (SARP) can be formulated in an environment subject to both objective uncertainty (randomness inherent to nature) and subjective uncertainty (lack of knowledge about the state of the world). In this paper, we present an interval arithmetic interpretation of the uncertainty problem. A crisis scenario is modeled as an assignment and optimization problem with interval-valued parameters and constraints. These intervals capture uncertainty over the problem data. A branch and bound algorithm is used to explore the solution space. Interval arithmetic is employed to compute bounds and obtain feasible assignments. From the resulting assignments, residual injury intervals are derived to assess the impact of uncertainty on each wounded person. Parallel computing techniques are also investigated to reduce execution times in the solution process.
Verifying timed systems is essential in safety-critical applications and poses significant challenges due to the huge number of possible behaviors. Model checking is a powerful tool of verification exploring the possible behaviors of systems, but it struggles with industrial applications, particularly when time is involved. Abstraction-based techniques are often used for the model checking of complex systems, as they can simplify the representation of the state space. Lazy abstraction is such a technique that incrementally adjusts (refines) abstractions only as needed, thus offering a promising solution by balancing precision and efficiency. This paper explores both sequential and parallel implementations of lazy abstraction strategies for timed systems. The sequential approach generalizes former implementations, while parallel implementations aim to leverage modern multi-core architectures for improved scalability and efficiency. Through empirical evaluation of benchmark systems, the research compares the various approaches, identifying key factors influencing parallelization effectiveness. The findings offer insights into lazy abstraction and opens new directions to further enhance the verification of complex timed systems.
Interval observers typically rely on performance criteria that specify the estimation accuracy. Inappropriately parameterized performance criteria can lead to linear matrix inequalities (LMIs) that do not yield feasible solutions. Retuning the output specification of the error dynamics allows for exploiting structural feasibility. The overall goal of this paper is to design a TNL interval observer for systems for which the LMIs do not yield a feasible solution with the standard specification of the performance criteria. As an example, the proposed tuning methods are applied to the state estimation of a lithium-ion battery cell. The LMIs introduced together with this observer structure initially do not have a feasible solution for the investigated battery model. To obtain feasible solutions, we propose extended design conditions for the TNL interval observer based on a virtual output equation for the error dynamics that is utilized to reduce the influence of uncertainties on the estimation results. Additionally, we present two techniques to enforce interpretable structures in the observer gains to enhance the estimation accuracy. The first technique enforces a desired ratio between the elements of selected observer gains, the second technique influences the estimation accuracy by specifying the eigenvalues of the scaled observer system matrix. To demonstrate the fundamental application of the tuning methods, the proposed techniques are initially applied to the state estimation of a mass-spring-damper system. Subsequently, the effectiveness of the proposed techniques is shown for the state estimation of the lithium-ion battery cell. With both techniques, the estimation accuracy can be significantly enhanced. Furthermore, they provide a framework for systematically designing TNL interval observers.
In language technology, clean data is fundamental for training high-quality models, yet large corpora often contain substantial noise due to OCR errors, missing diacritics, and various user-generated inconsistencies. This paper presents a comprehensive text cleaning pipeline tailored for Hungarian, leveraging transformer-based language models optimized for three key tasks: OCR error correction, diacritic restoration, and filtering grammatically incorrect sentences. We introduce huT5, a Hungarian adaptation of the mT5 model, which reduces model parameters and resource demands while maintaining strong performance on Hungarian-specific text cleaning tasks. The huT5 models were fine-tuned on carefully constructed Hungarian corpora for each task and benchmarked against state-of-the-art methods, demonstrating competitive results, particularly in OCR error correction and diacritic restoration. Our pipeline offers an efficient, freely accessible solution to enhance data quality for Hungarian NLP applications, setting a new standard in resource-efficient, language-specific text cleaning.
Given the advantages observed with Reinforcement Learning from Human Feedback (RLHF) and Direct Preference Optimization (DPO) in English, it is promising to explore their effectiveness for abstractive summarization in languages with complex morphological and syntactic features, such as Arabic. In this study, we fine-tune the Llama~2 model, which demonstrates a significant capability to enhance summarization results. We highlight how Llama 2, combined with advanced techniques like RLHF and DPO, markedly improves the quality of Abstractive Arabic summarization, showcasing the model's superior performance in this challenging task. Furthermore, the AraSum corpus plays a critical role in achieving outstanding results, highlighting its effectiveness in improving the performance of summarization models. While this work focuses on Arabic, the techniques and insights presented are language-agnostic, offering broader applications for abstractive summarization in other languages.
This paper presents an approach to deal with the prediction of dynamical systems in case of interval uncertainties. These uncertainties can be both on the initial state vector, on the time-dependent inputs and on the evolution function. The approach is based on the Muller theorem often used in an interval context to perform the prediction of cooperative systems. We show here that the Muller approach can be used for general non-cooperative systems. We also show the benefit we can obtain by using a conditioning approach in order to reduce the overestimation.
Calculating directly the inner and outer approximation of the image of a set by a function can be challenging. Then, it is sometimes preferred to compute the image of the boundary of the set instead. However, boundary-based methods are subject to the apparition of fake boundaries in the image set. These fake boundaries add pessimism when characterizing the inner approximation of the image set. This paper then introduces the notion of Box Chains to simplify the detection and the suppression of the fake boundaries. The characterization of the inner and outer approximation of the image set in the case of a function from the unit disk D to R2 will be considered, with two examples.
Complex interval arithmetic is a powerful tool for the analysis of computational errors. The naturally arising rectangular, polar, and circular interval types yield overly relaxed bounds. The later introduced polygonal type allows for arbitrarily precise representation for a higher computational cost. We propose the polyarc interval type as an effective generalization of the above-mentioned types. The polyarc interval can represent all types and most of their arithmetic combinations precisely and has a better approximation capability with that of the polygonal interval. In particular, in specific cases of antenna tolerance analysis and robot localization it can achieve perfect accuracy for lower computational cost then the polygonal type, which we show in a relevant case study.
We present a new uncertainty propagation algorithm based on interval arithmetic. The goal is to explore the benefits of a set-based approach for estimation and data association using validated simulation. The presented algorithm capitalises on the measures of a dynamical system to improve its estimation and reduce uncertainties on its trajectory. Our approach also contributes to data association by computing the precision required for a measure to belong to a given track with confidence levels. Mainly interested in space surveillance, we illustrate the contributions of this new algorithm with several scenarios of orbit determination and satellite tracking and their numerical simulations.
A local path planning algorithm aims to provide a global, deterministic and safe solution for the dynamic navigation of wheeled robots with limited visibility. To this end, a novel approach based on open interval B-spline curves computed over a receding horizon is exposed in this paper. Real-time performances are ensured by using an interval branch and bound algorithm. The resulting path is smooth, obstacle-avoidant, and continuously connects local paths without requiring additional computation. Furthermore, this approach offers a guaranteed understanding of the solution's state. A large set of simulations, adapted for a wheeled differential robot on several scenarios, is finally carried out to assess parameters impact and performances.
This paper presents an efficient online method to simulate a dynamical system with interval uncertainties. These uncertainties can be either on the initial state vector, on the time-dependent inputs, or on the evolution function. Compared to other techniques used for the guaranteed integration of differential inclusion, the presented approach is online and requires a small and fixed number of operations at each sampling time. An illustration related to underwater robotics will be provided. The application involves a robot with a ballast that can move from the surface to the sea floor. We would like to guarantee that the robot will reach a given depth at a given time.
In this paper, we introduce a reliable positioning method for a smart wheelchair by using ultra-wideband (UWB) technology. This method provides confidence domains of the pose by assuming bounded measurement errors and proprioceptive information, without any assumptions of independence. Exploiting interval analysis and constraint propagation techniques, we characterize the sets of all feasible poses that are consistent with the measurements. Our method has been validated through experiments with a smart power wheelchair equipped with UWB sensors in realistic conditions. The results demonstrate that our approach consistently provides guaranteed uncertainty domains with 100% integrity across the tested dataset, even when faced with inconsistent measurements. In addition, we compare our interval-based method with M-estimator approaches, and show that while achieving slightly worse positioning accuracy, our method offers superior consistency.
This paper considers the issue of how to deal with Signal Temporal Logic (STL) when taking into account uncertainties. The STL is a formalism with a large expressiveness to describe real-time properties on real-value signals. It is particularly used for system verification. This work focuses on extensions of STL that handle bounded uncertainties on predicates or on the signal itself, by using tubes to represent the sets of signals. In this way, it becomes possible to robustly check the satisfaction of specifications for a noisy system. However, some cases are undecidable due to uncertainty, and other ones are too complex to determine. Mainly, this paper provides a literature review and compares the few state-of-the-art STL monitors able to deal with tubes. In addition, it proposes to go further by introducing Boolean intervals to formalize undecidable cases, and by implementing a new STL formalism applied to sets in DynIbex, a guaranteed integration tool. Thus, STL specifications can be validated in a guaranteed way for a simulated system. As a result, we obtain the same reliable result as the state-of-the-art, but faster. A robotic application with a drone is proposed to illustrate the concept.
This paper explores the problem of the paving of the union of adjacent contractors. The focus is first put on the analysis of the topology of a set operator, which can be stable or not stable. Then, depending on the stability of the union operator, solutions are proposed to avoid fake boundaries in stable and non-stable union of sets. For stable unions of sets, a boundary preserving form will be developed to add a set overlapping the fake boundary in the expression of the union, whereas for non-stable union of sets, a boundary approach will be developed to avoid fake boundaries. Some problem-specific solutions are also developed to avoid fake boundaries. As an example, an enhancement of the separator on the visibility constraint is proposed. This avoids fake boundaries while characterizing the set of non-visible points from an observation point relative to a polygon.
Ensuring thread safety in applications is crucial for preventing subtle and challenging bugs in concurrent programming. This paper presents two algorithmic approaches to improve thread safety through static analysis and to demonstrate their benefits in real life, the authors also implemented them as two detectors in SpotBugs static analyzer. These checkers are designed to identify unsafe usages of shared resources and improper atomic operations in concurrent Java programming, aiming to mitigate common multithreading issues such as race conditions. By emphasizing consistent locking strategies and the correct use of atomic types, the study offers insight into how to improve the reliability of multithreaded applications.
Due to their decentralized and trustless nature, blockchain and distributed ledger technologies are increasingly used in several domains, including critical applications. The behavior of such blockchain-integrated systems is typically driven by smart contracts. However, smart contracts are application-specific software and may contain faults with severe system-level impacts. This is especially true in the case of the extensively used Hyperledger Fabric (HLF) platform, where smart contracts are written in general-purpose languages (Java, among others), and applications can go far beyond handling virtualcurrency-like assets. In this work, we present a novel formal-verification-based approach to smart contract verification and a high-level empirical model of the HLF platform. Our Smart Contract in the Loop (SCIL) method uses a model checker (Java Pathfinder) to check whether specific error properties hold for a given smart contract, while a predefined combination of platform-level fault modes is active. We facilitate the checking of HLF smart contracts without modification and enable the propagation or non-propagation of platform faults through the smart contracts to the system failure level.
Ensuring thread safety in applications is crucial for preventing subtle and challenging bugs in concurrent programming. This paper presents two algorithmic approaches to improve thread safety through static analysis and to demonstrate their benefits in real life, the authors also implemented them as two detectors in SpotBugs static analyzer. These checkers are designed to identify unsafe usages of shared resources and improper atomic operations in concurrent Java programming, aiming to mitigate common multithreading issues such as race conditions. By emphasizing consistent locking strategies and the correct use of atomic types, the study offers insight into how to improve the reliability of multithreaded applications.
Time series analysis and prediction is a difficult and complex problem. Many machine- and deep-learning methods exist with better and better results. This paper proposes a strategy called Multi Model Recursion. It uses separate deep-learning models per feature that needs predicting. Another improvement is not predicting features which are easily calculated. Having extra models per feature helps in "simulating" a future environment since it predicts external variables otherwise unknown. The Multi Model Recursion developed is an improvement of the commonly used Recursive strategy. The paper compares this method with models and strategies frequently used in the field. The testing dataset is put together from publicly available Hungarian electricity load and weather data. The task was to predict the country's net electricity load for the next 3 hours.
Due to their decentralized and trustless nature, blockchain and distributed ledger technologies are increasingly used in several domains, including critical applications. The behavior of such blockchain-integrated systems is typically driven by smart contracts. However, smart contracts are application-specific software and may contain faults with severe system-level impacts. This is especially true in the case of the extensively used Hyperledger Fabric (HLF) platform, where smart contracts are written in general-purpose languages (Java, among others), and applications can go far beyond handling virtual-currency-like assets. In this work, we present a novel formal-verification-based approach to smart contract verification and a high-level empirical model of the HLF platform. Our Smart Contract in the Loop (SCIL) method uses a model checker (Java Pathfinder) to check whether specific error properties hold for a given smart contract, while a predefined combination of platform-level fault modes is active. We facilitate the checking of HLF smart contracts without modification and enable the propagation or non-propagation of platform faults through the smart contracts to the system failure level.
