Abstract
This article presents Pardinus, an extension of the popular Kodkod relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. Pardinus includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.

Abstract
Robotic applications are often designed to be reusable and configurable. Sometimes, due to the different supported software and hardware components, as well as the different implemented robot capabilities, the total number of possible configurations for a single system can be extremely large. In these scenarios, understanding how different configurations coexist and which components and capabilities are compatible with each other is a significant time sink both for developers and end users alike. In this paper, we present a static analysis tool, specifically designed for robotic software developed for the Robot Operating System (ROS), that is capable of presenting a graphical and interactive overview of the system's runtime variability, with the goal of simplifying the deployment of the desired robot configuration.

Abstract
This work introduces a new fuzzy epistemic logic with public announcement with fuzzyness on both transitions and propositions. The interpretation of the connectives is done over the Godel algebra and the interpretation of public announcements in this logic generalises the traditional update one. The core idea is that, the effect of a public announcement is reflected on the transitions degrees of the models. The update takes in account not only the truth degree of the announcement, at a target state, but also the degree of the transitions reaching that state. We prove the soundness of all axioms of the multi-agent epistemic logic with public announcements with respect to this graded semantics. Finally, we introduce the notion of bisimulation and prove the modal invariance property for our logic.

Abstract
This paper explores a strict relation between two core notions of the semantics of programs and of fuzzy logics: Kleene Algebras and (pseudo) uninorms. It shows that every Kleene algebra induces a pseudo uninorm, and that some pseudo uninorms induce Kleene algebras. This connection establishes a new perspective on the theory of Kleene algebras and provides a way to build (new) Kleene algebras. The latter aspect is potentially useful as a source of formalism to capture and model programs acting with fuzzy behaviours and domains. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
We present MONARCH, a framework-agnostic storage middleware that transparently employs storage tiering to accelerate Deep Learning (DL) training. It leverages existing storage tiers of modern supercomputers (i.e., compute node's local storage and shared parallel file system (PFS)), while considering the I/O patterns of DL frameworks to improve data placement across tiers. MONARCH aims at accelerating DL training and decreasing the I/O pressure imposed over the PFS. We apply MONARCH to TensorFlow and PyTorch, while validating its performance and applicability under different models and dataset sizes. Results show that, even when the training dataset can only be partially stored at local storage, MONARCH reduces TensorFlow's and PyTorch's training time by up to 28% and 37% for I/O-intensive models, respectively. Furthermore, MONARCH decreases the number of I/O operations submitted to the PFS by up to 56%.

Abstract
Modern large-scale I/O applications that run on HPC infrastructures are increasingly becoming metadata-intensive. Unfortunately, having multiple concurrent applications submitting massive amounts of metadata operations can easily saturate the shared parallel file system's metadata resources, leading to unresponsiveness of the storage backend and overall performance degradation. To address these challenges, we present PADLL, a storage middleware that enables system administrators to proactively control and ensure QoS over metadata workflows in HPC storage systems. We demonstrate its performance and feasibility by controlling the rate of both synthetic and realistic I/O workloads. Results show that PADLL can dynamically control metadata-aggressive workloads, prevent I/O burstiness, and ensure I/O fairness and prioritization.