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.

The ability of determining and dealing with the trajectories followed by an object in a given (concrete or abstract) space turns out to be quite useful in a variety of contexts. This is the case, in particular, in positioning, where it can be exploited, for instance, for traffic control and user profiling. A key step in trajectory management is the evaluation of trajectory similarity. In many positioning applications, trajectories are built from Global Navigation Satellite System (GNSS) readings; however, in various scenarios, these coordinates are not available. In this paper, we focus on fingerprint positioning systems characterised by a low sampling frequency and a high heterogeneity of the observations. We start with a comprehensive analysis of well-known GNSS-based trajectory similarity measures, and show how some of them can actually be adapted to the fingerprinting setting. Then, we outline a novel approach that exploits multiple information, including both spatial and cellular identifiers with received signal strength. Finally, we make an extensive, experimental comparative evaluation of the various measures (adapted and novel ones) over a real-world fingerprint dataset.

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.