Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g., for specifying and verifying desired system properties. While translating FOL into human-readable English is relatively straightforward, the inverse problem, converting NL to FOL (NL-FOL translation), has remained a longstanding challenge, for both humans and machines. Although the emergence of Large Language Models (LLMs) promised a breakthrough, recent literature provides contrasting results on their ability to perform NL-FOL translation. In this work, we provide a threefold contribution. First, we critically examine existing datasets and protocols for evaluating NL-FOL translation performance, revealing key limitations that may cause a misrepresentation of LLMs' actual capabilities. Second, to overcome these shortcomings, we propose a novel evaluation protocol explicitly designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization, and dataset contamination. Third, using this new approach, we show that state-of-the-art, dialogue-oriented LLMs demonstrate strong NL-FOL translation skills and a genuine grasp of sentence-level logic, whereas embedding-centric models perform markedly worse.

In runtime verification, monitoring consists of analyzing the current execution of a system and determining, on the basis of the observed finite trace, whether all its possible continuations satisfy or violate a given specification. This is typically done by synthesizing a monitor–often a Deterministic Finite State Automaton (DFA)–from logical specifications expressed in Linear Temporal Logic (LTL) or in its finite-word variant (LTLf). Unfortunately, the size of the resulting DFA may incur a doubly exponential blow-up in the size of the formula. In this paper, we identify some conditions under which monitoring can be done without constructing such a DFA. We build on the notion of intentionally safe and cosafe formulas to show that monitoring of these formulas can be carried out through trace-checking, that is, by directly evaluating them on the current system trace, with a polynomial complexity in the size of both the trace and the formula. In addition, we investigate the complexity of recognizing intentionally safe and cosafe formulas for the safety and cosafety fragments of LTL and LTLf. As for LTLf, we show that all formulas in these fragments are intentionally safe and cosafe, thus removing the need for the check. As for LTL, we prove that the problem is in PSPACE, significantly improving over the EXPSPACE complexity of full LTL.

Monitoring is a runtime verification technique that allows one to check whether an ongoing computation of a system (partial trace) satisfies a given formula. It does not need a complete model of the system, but it typically requires the construction of a deterministic automaton doubly exponential in the size of the formula (in the worst case), which limits its practicality. In this paper, we show that, when considering finite, discrete traces, monitoring of pure past (co)safety fragments of Signal Temporal Logic (STL) can be reduced to trace checking, that is, evaluation of a formula over a trace, that can be performed in time polynomial in the size of the formula and the length of the trace. By exploiting such a result, we develop a GPU-accelerated framework for interpretable early failure detection based on vectorized trace checking, that employs genetic programming to learn temporal properties from historical trace data. The framework shows a 2–10% net improvement in key performance metrics compared to the state-of-the-art methods.

Fingerprinting is a common localisation approach that often estimates a device's position by comparing an observed vector to a set of prior vectors labelled with a ground truth location, typically using methods like k-NN. In Wi-Fi fingerprinting, these vectors represent visible access points and their signal strength. Thus, the choice of metric to compare the fingerprints is crucial. In this work, we discuss our main findings regarding the extent to which metrics in the fingerprint vector space preserve relationships among locations in the 2D/3D geometric/real world. In summary, traditional metrics are not optimal on their own, and while combining them into a learned meta-metric offers slight improvements, deep metric learning, i.e., learning similarities in an end-to-end fashion with deep neural networks, appears much more effective. However, this approach has its challenges given that in the literature the problem has only been formulated for binary similarities rather than continuous ones.

In a world increasingly pervaded by mobile and IoT devices, position-related information is gaining more and more importance. Highly accurate and standardized positioning techniques are not yet available for indoor scenarios, unlike for the outdoor case. The most commonly used method for indoor positioning is WiFi fingerprinting, which, despite its well-recognized advantages, still suffers from some notable limitations. Recently, approaches relying on deep learning showed promising results even though their lack of interpretability is still a significant drawback. In this paper, for the first time, we propose a domain-specific concept of interpretability, based on identifying the access points that are most relevant to a position estimate. The goal is to enhance the positioning process by gaining novel scientific knowledge and operational insights, without worsening the performance of the task. We show how it is possible to practically achieve both a local and a global notion of interpretability by means of a deep learning model equipped with an attention module, applied to a ranking based fingerprint representation. Since off-the-shelf application of attention does not guarantee to achieve a faithful nor plausible interpretation, we verified through a series of thoroughly designed quantitative and qualitative clustering based experiments the existence of a strong relationship between the obtained interpretations and the positioning domain. Finally, as by-product, we showed an example of how the new knowledge can be used in principle to improve positioning performance.

Positioning is a key task in many different contexts. In the last decades, it has considerably evolved, but, while there are a lot of systems that offer a quite good performance in outdoor scenarios, the indoor realm is still under exploration. Among existing technologies and techniques for indoor positioning, the most popular one makes use of WiFi fingerprints. Such an approach has many advantages; however, its adoption as a standard for everyday life is limited due to issues like the (time) costly radio map construction, and radio signal strength fluctuations in indoor environments. In this paper, we present a novel solution for indoor positioning based on deep learning, that ignores as much as possible signal strengths, in order to reduce the adverse effects associated with their usage. It exploits signal strength only to generate a ranking-based representation of the access points associated with a fingerprint. By developing and testing two recurrent neural network models, we show that the proposed approach is able to achieve a positioning performance, based on access point ranking, comparable to the one achieved by state-of-the-art algorithms on multiple publicly available indoor datasets. As additional benefits, compared to existing ones, the developed solution is considerably more robust to signal fluctuations and simpler in terms of the considered data.

Recently proposed methods allow the generation of simulated scores representing the values of an effectiveness metric, but they do not investigate the generation of the actual lists of retrieved documents. In this paper we address this limitation: we present an approach that exploits an evolutionary algorithm and, given a metric score, creates a simulated relevance profile (i.e., a ranked list of relevance values) that produces that score. We show how the simulated relevance profiles are realistic under various analyses.

Linear temporal logic (LTL) is commonly used in model checking tasks; moreover, it is well-suited for the formalization of technical requirements. However, the correct specification and interpretation of temporal logic formulas require a strong mathematical background and can hardly be done by domain experts, who, instead, tend to rely on a natural language description of the intended system behaviour. In such situations, a system that is able to automatically translate English sentences into LTL formulas, and vice versa, would be of great help. While the task of rendering an LTL formula into a more readable English sentence may be carried out in a relatively easy way by properly parsing the formula, the converse is still an open problem, due to the inherent difficulty of interpreting free, natural language texts. Although several partial solutions have been proposed in the past, the literature still lacks a critical assessment of the work done. We address such a shortcoming, presenting the current state of the art for what concerns the English-to-LTL translation problem, and outlining some possible research directions.

Abstract In this work, a data set describing phone interactions arising in a multichannel and multiskill contact centre is considered with the aim of classifying inbound sessions into those that will be eventually managed by an agent and those that, instead, will be abandoned before. More precisely, the goal of the work is to extract interpretable pieces of information that allow us to predict whether a user will or will not abandon a call, which may turn out to be very useful for the purpose of contact centre managing. To this end, the performance of two well‐known, state‐of‐the‐art evolutionary algorithms for feature selection (evolutionary nondominated radial slots based algorithm and nondominated sorted genetic algorithm) is compared for the task of feature selection, under the criteria of accuracy and cardinality of the selection, as well as for the task of fuzzy rule extraction, under the criteria of interpretability, accuracy, and hypervolume test. The best obtained fuzzy classifier, chosen after a decision making process, is validated and interpreted by domain experts.

Evaluating in a correct, fair, systematic and reliable way the quality of the work is a central problem in modern business. Both from the psychological and the social point of view, this problem is very far away from being solved, let alone from being managed by a (semi-) automatic decision support system. In this paper we consider the case study of evaluating the operators’ work quality in a medium-sized contact center, and, in particular, the problem of selecting the correct variables to be used in such an evaluation. Starting from a data set representative of the company’s range and size of activities, that allowed no usable predictive model for evaluating the skills of the agents, we were able to devise a reproducible methodology, along with an a posteriori optimization process, to select the essential variables that should be used to objectively evaluate the quality of the agents’ work. These results may be used in a support system helping the supervisors in evaluating the agents’ performances. Moreover, we believe that our methodology may be extrapolated and reused in other comparable contexts characterized by the measurability of the human operators’ performance.