Abstract
Effective testing of message-oriented software requires describing the expected behaviour of the system and the causality relations between messages. This is often achieved with formal specifications based on temporal logics that require both first-order and metric temporal constructs - to specify constraints over data and real time. This paper proposes a technique to automatically generate tests for metric first-order temporal specifications that match well-understood specification patterns. Our approach takes in properties in a high-level specification language and identifies test schemas (strategies) that are likely to falsify the property. Schemas correspond to abstract classes of execution traces, that can be refined by introducing assumptions about the system. At the low level, concrete traces are successively produced for each schema using property-based testing principles. We instantiate this approach for a popular robotic middleware, ROS, and evaluate it on two systems, showing that schema-based test generation is effective for message-oriented software.

Abstract
This paper proposes the first mutation-based technique for the repair of Alloy 6 first-order temporal logic specifications. This technique was developed with the educational context in mind, in particular, to repair submissions for specification challenges, as allowed, for example, in the Alloy4Fun web-platform. Given an oracle and an incorrect submission, the proposed technique searches for syntactic mutations that lead to a correct specification, using previous counterexamples to quickly prune the search space, thus enabling timely feedback to students. Evaluation shows that, not only is the technique feasible for repairing temporal logic specifications, but also outperforms existing techniques for non-temporal Alloy specifications in the context of educational challenges.

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.