Sebastián Uchitel

Tomás Delgado, Marco Sánchez Sorondo, Víctor Braberman et al.

Controller synthesis is in essence a case of model-based planning for non-deterministic environments in which plans (actually ''strategies'') are meant to preserve system goals indefinitely. In the case of supervisory control environments are specified as the parallel composition of state machines and valid strategies are required to be ''non-blocking'' (i.e., always enabling the environment to reach certain marked states) in addition to safe (i.e., keep the system within a safe zone). Recently, On-the-fly Directed Controller Synthesis techniques were proposed to avoid the exploration of the entire -and exponentially large-environment space, at the cost of non-maximal permissiveness, to either find a strategy or conclude that there is none. The incremental exploration of the plant is currently guided by a domain-independent human-designed heuristic. In this work, we propose a new method for obtaining heuristics based on Reinforcement Learning (RL). The synthesis algorithm is thus framed as an RL task with an unbounded action space and a modified version of DQN is used. With a simple and general set of features that abstracts both states and actions, we show that it is possible to learn heuristics on small versions of a problem that generalize to the larger instances, effectively doing zero-shot policy transfer. Our agents learn from scratch in a highly partially observable RL task and outperform the existing heuristic overall, in instances unseen during training.

Tim Menzies, Paris Avgeriou, Robert Feldt et al.

In 2025, SE publishing faces an existential crisis of scalability. As our communities swell globally and integrate fast-moving methodologies like LLMs, traditional peer-review practices are collapsing under the strain. The "bureaucratic anomaly" of monolithic review has become mathematically unsustainable, creating a stochastic "lottery" that punishes novelty and exhausts researchers. This paper, written from the perspective of 2036, documents potential solutions. Here, the editors of ASE, EMSE, IST, JSS, TOSEM and TSE dream a collective dream of a brighter future. In summary first we stopped fighting (The Journal Alliance). Then we fixed the process (The Lottery / Unbundling / Fixing the Benchmark Graveyard). And then we fixed the culture (Cathedrals/Bazaars).

Man Zhang, Tao Yue, Nazareno M. Aguirre et al.

Complex software systems such as autonomous vehicles, robotics increasingly interact with dynamic physical, cyber, and social environments. Reasoning about their behavior, maintaining them under continuous change, and evolving them safely require trustworthy knowledge about the system, its assumptions, and its operating context. Knowledge models (KMs) provide a practical basis for such reasoning, but they may themselves become incomplete, inconsistent, or outdated as systems evolve. This paper presents TrustModel, a vision for the agentic generation and evolution of living KMs. TrustModel comprises three agentic subsystems: Modeling, for constructing and updating KMs; Conformance, for assessing their alignment with the system and its environment; and Evolution, for generating guidance to keep KMs synchronized with emerging changes. We demonstrate how TrustModel can be instantiated for model-based testing and discuss its potential for supporting other MDE activities, such as requirements and assumption monitoring, architectural drift tracking, and change impact assessment. Overall, TrustModel positions living KMs as a foundation for dependable engineering of continuously evolving software systems.

Tiberiu-Andrei Georgescu, Alexander W. Goodall, Dalal Alrajeh et al.

Shielding is widely used to enforce safety in reinforcement learning (RL), ensuring that an agent's actions remain compliant with formal specifications. Classical shielding approaches, however, are often static, in the sense that they assume fixed logical specifications and hand-crafted abstractions. While these static shields provide safety under nominal assumptions, they fail to adapt when environment assumptions are violated. In this paper, we develop the first adaptive shielding framework - to the best of our knowledge - based on Generalized Reactivity of rank 1 (GR(1)) specifications, a tractable and expressive fragment of Linear Temporal Logic (LTL) that captures both safety and liveness properties. Our method detects environment assumption violations at runtime and employs Inductive Logic Programming (ILP) to automatically repair GR(1) specifications online, in a systematic and interpretable way. This ensures that the shield evolves gracefully, ensuring liveness is achievable and weakening goals only when necessary. We consider two case studies: Minepump and Atari Seaquest; showing that (i) static symbolic controllers are often severely suboptimal when optimizing for auxiliary rewards, and (ii) RL agents equipped with our adaptive shield maintain near-optimal reward and perfect logical compliance compared with static shields.

Sebastián Zudaire, Leandro Nahabedian, Sebastián Uchitel

The design of systems that can change their behaviour to account for scenarios that were not foreseen at design time remains an open challenge. In this paper we propose an approach for adaptation of mobile robot missions that is not constrained to a predefined set of mission evolutions. We propose applying the MORPH adaptive software architecture to UAVs and show how controller synthesis can be used both to guarantee correct transitioning from the old to the new mission goals while architectural reconfiguration to include new software actuators and sensors if necessary. The architecture brings together architectural concepts that are commonplace in robotics such as temporal planning, discrete, hybrid and continuous control layers together with architectural concepts from adaptive systems such as runtime models and runtime synthesis. We validate the architecture flying several missions taken from the robotic literature for different real and simulated UAVs.

Sebastián Zudaire, Martín Garrett, Sebastián Uchitel

Temporal logic task planning for robotic systems suffers from state explosion when specifications involve large numbers of discrete locations. We provide a novel approach, particularly suited for tasks specifications with universally quantified locations, that has constant time with respect to the number of locations, enabling synthesis of plans for an arbitrary number of them. We propose a hybrid control framework that uses an iterator to manage the discretised workspace hiding it from a plan enacted by a discrete event controller. A downside of our approach is that it incurs in increased overhead when executing a synthesised plan. We demonstrate that the overhead is reasonable for missions of a fixed-wing Unmanned Aerial Vehicle in simulated and real scenarios for up to 700000 locations.

Rodrigo Castaño, Victor Braberman, Diego Garbervetsky et al.

Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success stories. However, widespread adoption remains unlikely in the short term and one of the remaining obstacles in that direction is the vast number of instances which software model checkers cannot fully analyze within reasonable memory and CPU bounds. The majority of verification tools fail to provide a measure of progress or any intermediate verification result when such situations occur. Inspired in the success that coverage metrics have achieved in industry, we propose to adapt the definition of coverage to the context of verification. We discuss some of the challenges in pinning down a definition that resembles the deeply rooted semantics of test coverage. Subsequently we propose a definition for a broad family of verification techniques: those based on Abstract Reachability Trees. Moreover, we discuss a general approach to computing an under-approximation of such metric and a specific heuristic to improve the performance. Finally, we conduct an empirical evaluation to assess the viability of our approach.

Rodrigo Castaño, Victor Braberman, Diego Garbervetsky et al.

Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe cones, and present the notion of execution reports, which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the execution reports produced and the information that can be extracted.

Daniel Ciolek, Victor Braberman, Nicolás D'Ippolito et al.

This paper presents a Directed Controller Synthesis (DCS) technique for discrete event systems. The DCS method explores the solution space for reactive controllers guided by a domain-independent heuristic. The heuristic is derived from an efficient abstraction of the environment based on the componentized way in which complex environments are described. Then by building the composition of the components on-the-fly DCS obtains a solution by exploring a reduced portion of the state space. This work focuses on untimed discrete event systems with safety and co-safety (i.e. reachability) goals. An evaluation for the technique is presented comparing it to other well-known approaches to controller synthesis (based on symbolic representation and compositional analyses).