We present a compositional approach to controller synthesis of discrete event system controllers with linear temporal logic (LTL) goals. We exploit the modular structure of the plant to be controlled, given as a set of labelled transition systems (LTS), to mitigate state explosion that monolithic approaches to synthesis are prone to. Maximally permissive safe controllers are iteratively built for subsets of the plant LTSs by solving weaker control problems. Observational synthesis equivalence is used to reduce the size of the controlled subset of the plant by abstracting away local events. The result of synthesis is also compositional, a set of controllers that when run in parallel ensure the LTL goal. We implement synthesis in the MTSA tool for an expressive subset of LTL, GR(1), and show it computes solutions to that can be up to 1000 times larger than those that the monolithic approach can solve.

Ensuring the reliability and verifiability of large language model (LLM)-enabled systems remains a significant challenge in software engineering. We propose a probabilistic framework for systematically analyzing and improving these systems by modeling and refining distributions over clusters of semantically equivalent outputs. This framework facilitates the evaluation and iterative improvement of Transference Models--key software components that utilize LLMs to transform inputs into outputs for downstream tasks. To illustrate its utility, we apply the framework to the autoformalization problem, where natural language documentation is transformed into formal program specifications. Our case illustrates how distribution-aware analysis enables the identification of weaknesses and guides focused alignment improvements, resulting in more reliable and interpretable outputs. This principled approach offers a foundation for addressing critical challenges in the development of robust LLM-enabled systems.

We introduce a novel verification problem that exploits common code fragments between two programs. We discuss a solution based on Mimicry Monitors that anticipate if the execution of a Program Under Analysis has a counterpart in an Oracle Program without executing the latter. We discuss how such monitors can be leveraged in different software engineering tasks.

The emergence of prompting as the dominant paradigm for leveraging Large Language Models (LLMs) has led to a proliferation of LLM-native software, where application behavior arises from complex, stochastic data transformations. However, the engineering of such systems remains largely exploratory and ad-hoc, hampered by the absence of conceptual frameworks, ex-ante methodologies, design guidelines, and specialized benchmarks. We argue that a foundational step towards a more disciplined engineering practice is a systematic understanding of the core functional units–generative transformations–and their compositional patterns within LLM-native applications. Focusing on the rich domain of software verification and falsification, we conduct a secondary study of over 100 research proposals to address this gap. We first present a fine-grained taxonomy of generative transformations, abstracting prompt-based interactions into conceptual signatures. This taxonomy serves as a scaffolding to identify recurrent transformation relationship patterns–analogous to software design patterns–that characterize solution approaches in the literature. Our analysis not only validates the utility of the taxonomy but also surfaces strategic gaps and cross-dimensional relationships, offering a structured foundation for future research in modular and compositional LLM application design, benchmarking, and the development of reliable LLM-native systems.

We study directed control of discrete event system expressed as the parallel composition of interacting automata. Solutions that first compose the automata and then compute a controller may result in an exponential blow up. We present a technique that builds the composition on-the-fly guided by a novel domain-independent heuristic, which attempts to discover relevant dependencies between the intervening components. We obtain safe and non-blocking directed controllers, or directors, exploring a reduced portion of the state space. We present the first experimental results on directed control comparing on-the-fly composition with informed search against the original monolithic approach to directed control.

Directed Controller Synthesis technique finds solutions for the non-blocking property in discrete event systems by exploring a reduced portion of the exponentially big state space, using best-first search. Aiming to minimize the explored states, it is currently guided by a domain- independent handcrafted heuristic, with which it reaches state-of-the-art performance. In this work, we propose a new method for obtaining heuristics based on Reinforcement Learning. The synthesis algorithm is 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, we show that it is possible to learn heuristics on small versions of a problem in a way that generalizes to the larger instances. Our agents learn from scratch and outperform the existing heuristic overall, in instances unseen during training.

An important ability of self-adaptive systems is to be able to autonomously understand the environment in which they operate and use this knowledge to control the environment behaviour in such a way that system goals are achieved. How can this be achieved when the environment is unknown? Two phase solutions that require a full discovery of environment behaviour before computing a strategy that can guarantee the goals or report the non-existence of such a strategy (i.e., unrealisability) are impractical as the environment may exhibit adversarial behaviour to avoid full discovery. In this paper we formalise a control and discovery problem for reactive system environments. In our approach a strategy must be produced that will, for every environment, guarantee that unrealisablity will be correctly concluded or system goals will be achieved by controlling the environment behaviour. We present a solution applicable to environments characterisable as labeled transition systems (LTS). We use modal transition systems (MTS) to represent partial knowledge of environment behaviour, and rely on MTS controller synthesis to make exploration decisions. Each decision either contributes more knowledge about the environment's behaviour or contributes to achieving the system goals. We present an implementation restricted to GR(1) goals and show its viability.

A controller for a Discrete Event System must achieve its goals despite its environment being capable of resolving race conditions between controlled and uncontrolled events. Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem.

We show how reactive synthesis and automated planning can be leveraged effectively to find nonmaximal solutions to deterministic supervisory control problems of discrete event systems. To do so, we propose efficient translations of the supervisory control problem into the reactive synthesis and planning frameworks. Notably, our translation methods capture the compositional and reactive nature of control specifications, avoiding a potential exponential explosion found in alternative translation approaches. Additionally, we report on experimental results comparing the efficacy of different tools from the three disciplines, for a particular supervisory control benchmark.

We propose an approach for rapid detection of performance regressions using a simulator built from the original program by dynamic slicing and a certificate built using static analysis that generalizes its correctness. We discuss two case-studies that illustrate the potential benefits of the proposal.

Organisations require that their business processes reflect their evolving practices by maintaining compliance with their policies, strategies and regulations. Designing workflows which satisfy these requirements is complex and error-prone. Business process reconfiguration is even more challenging as not only a new workflow must be devised but also an understanding of how the transition between the old and new workflow must be managed. Transition requirements can include both domain independent, such as delayed and immediate change, or user-defined domain specific requirements. In this paper we present a fully automated technique which uses control synthesis to not only produce correct-by-construction workflows from business process requirements but also to compute a reconfiguration process that guarantees the evolution from an old workflow to a new one while satisfying any user-defined transition requirements. The approach is validated using three examples from the BPM Academic Initiative described as Dynamic Condition Response Graphs which we reconfigured for a variety of transitions requirements.

Discrete event controllers are at the heart of many software systems that require continuous operation. Changing these controllers at runtime to cope with changes in its execution environment or system requirements change is a challenging open problem. In this paper we address the problem of dynamic update of controllers in reactive systems. We present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur and in which the underlying system architecture can reconfigure. Our solution uses discrete event controller synthesis to automatically build a controller that guarantees both progress towards update and safe update.

This index covers all technical items—papers, correspondence, reviews, etc.—that appeared in this periodical during 2017, and items from previous years that were commented upon or corrected in 2017. Departments and other items may also be covered if they have been judged to have archival value. The Author Index contains the primary entry for each item, listed under the first author’s name. The primary entry includes the coauthors’ names, the title of the paper or other item, and its location, specified by the publication abbreviation, year, month, and inclusive pagination. The Subject Index contains entries describing the item under all appropriate subject headings, plus the first author’s name, the publication abbreviation, month, and year, and inclusive pages. Note that the item title is found only under the primary entry in the Author Index.

Behavior needs to be understood from early stages of software development. In this context, incremental and declarative modeling seems an attractive approach for closely capturing and analyzing requirements without early operational commitment. A traditional choice for such a kind of modeling is a logic-based approach. Unfortunately, in many cases, the formal description and validation of properties result in a daunting task, even for trained people. Moreover, some authors established some practical limitations with temporal logics expressive power. In this work, we present omega-feather weight visual scenarios ($$\omega$$ź-FVS) a declarative language, not founded on temporal logics, but on simple graphical scenarios, powerful enough to express $$\omega$$ź-regular properties. The notation is equipped with declarative semantics based on morphisms, and a tableau procedure is given enabling the possibility of automatic analysis.

This index covers all technical items - papers, correspondence, reviews, etc. - that appeared in this periodical during the year, and items from previous years that were commented upon or corrected in this year. Departments and other items may also be covered if they have been judged to have archival value. The Author Index contains the primary entry for each item, listed under the first author's name. The primary entry includes the co-authors' names, the title of the paper or other item, and its location, specified by the publication abbreviation, year, month, and inclusive pagination. The Subject Index contains entries describing the item under all appropriate subject headings, plus the first author's name, the publication abbreviation, month, and year, and inclusive pages. Note that the item title is found only under the primary entry in the Author Index.

We introduce a new class of 21/2-player games, the 21/2-player GR(1) games, that allows for solving problems of stochastic nature by adding a probabilistic component to simple 2-player GR(1) games. Further, we present an efficient approach for solving qualitative 21/2-player GR(1) games with polynomial-time complexity. Our approach is based on a reduction from 21/2-player GR(1) games to 2-player GR(1) games that allows for solving the game and constructing, from a sure winning strategy for player 2 (resp. 3) in a 2-player GR(1) game, an almost-sure (resp. positively) winning strategy for its corresponding 21/2-player GR(1) game. Key to the effectiveness of the proposed approach is the fact that the reduction generates a 2-player game that is linearly larger than the original 21/2player game, more precisely, it is linear with respect to the number of probabilistic states in the 21/2-player GR(1) game.

We introduce a new class of 21/2-player games, the 21/2-player GR(1) games, that allows for solving problems of stochastic nature by adding a probabilistic component to simple 2-player GR(1) games. Further, we present an efficient approach for solving qualitative 21/2-player GR(1) games with polynomial-time complexity. Our approach is based on a reduction from 21/2-player GR(1) games to 2-player GR(1) games that allows for solving the game and constructing, from a sure winning strategy for player square (resp. lozenge) in a 2-player GR(1) game, an almost-sure (resp. positively) winning strategy for its corresponding 21/2-player GR(1) game. Key to the effectiveness of the proposed approach is the fact that the reduction generates a 2-player game that is linearly larger than the original 21/2-player game, more precisely, it is linear with respect to the number of probabilistic states in the 21/2-player GR(1) game.

Model-based reliability estimation of systems can provide useful insights early in the development process. However, computational complexity of estimating metrics such as mean time to first failure (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, we present an alternative to exhaustive model exploration, as in probabilistic model checking, and partial random exploration, as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost. We present a novel automated technique for metric estimation that combines simulation, invariant inference, and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant characterises a partial model, which is then exhaustively explored using probabilistic model checking. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare.