Effective crime linkage analysis is crucial for identifying serial offenders and enhancing public safety. To address the limitations of traditional crime linkage methods when handling high-dimensional, sparse, and heterogeneous data, this paper proposes a Siamese Autoencoder framework to learn meaningful latent representations and uncover correlations in highly complex data. Using a dataset from the Violent Crime Linkage Analysis System—a database maintained by the Serious Crime Analysis Section of the UK’s National Crime Agency—our approach mitigates signal dilution in high-dimensional sparse data through decoder-stage integration of geographic-temporal features. This integration amplifies learned behavioral representations rather than allowing them to be overwhelmed at the input stage, leading to consistent improvements over baseline methods across multiple metrics. We further examine how different data reduction strategies based on domain-expert can impact model performance, offering practical insights into preprocessing for crime linkage. Our solution shows that advanced machine learning approaches can enhance linkage accuracy, improving AUC by up to 9% over traditional methods and providing insights to support human decision-making in crime investigation.

Reactive systems, which maintain ongoing interactions with their environment, are typically modeled using ω-regular languages. These languages characterize system behavior with infinite-length execution traces and are represented as nondeterministic Büchi automata (NBAs) or ω-regular expressions. Existing methods for synthesizing expressions from NBAs only handle state-based acceptance. This limitation forces the conversion of compact transition-based NBAs into larger state-based NBAs before synthesis. This article introduces the first direct synthesis method for ω-regular expressions from transition-based NBAs, eliminating the need for this transformation. The method works by decomposing an NBA into triplets of nondeterministic finite automata, subsuming existing pair-based decompositions to handle transition-based acceptance. We prove that our decomposition is correct, establishing our method’s soundness and completeness. We discuss the time and descriptional complexity of our method. Our empirical evaluation on 185 linear temporal logic formulas supports our hypothesis; transition-based synthesis reduces postfix size by 4.1× and 1.5× for recurrence and reactivity properties, respectively. We also analyze the structural NBA factors that determine when the transition-based NBA will yield a more compact expression and develop this into a simple criterion that, when applied, yields expressions that are at least as compact as those obtained by direct state-based synthesis.

Boundary conditions express situations under which requirements specifications conflict. They are used within a broader conflict management process to produce less idealized specifications. Several approaches have been proposed to identify boundary conditions automatically. Some introduce a prioritization criteria to reduce the number of boundary conditions presented to an engineer. However, identifying the few, relevant boundary conditions remains an open challenge. In this paper, we argue that one of the problems of the state of the art is with the definition of boundary condition itselfit is too weak. We propose a stronger definition which we refer to as Unavoidable Boundary Conditions (UBCs), which utilizes the notion of realizability in reactive synthesis. We show experimentally that UBCs non-trivially reduce the number of conditions produced by existing boundary condition identification techniques. We also relate UBCs to existing concepts in reactive synthesis used to provide feedback for unrealizable specifications (including counter-strategies and unrealizable cores). We then show that UBCs provide a targeted form of feedback for repairing unrealizable specifications.

Causal models provide a formal framework for identifying and reasoning about the causes of observed phenomena, making them valuable for decision-support contexts where understanding causality is essential. Yet applying these models in practice requires automated tools for key reasoning tasks. We present an Answer Set Programming (ASP)-based tool that supports three core capabilities for all acyclic binary causal models: (1) checking whether an event is an actual cause of another; (2) finding all minimal subsets of a failed candidate that do qualify as causes; and (3) inferring all actual causes of an outcome without assuming any candidate. Our tool is the first to support all three tasks within a unified framework, guaranteeing minimal contingency sets and outperforming prior implementations in both runtime and memory. We describe the system’s design and report on an empirical evaluation using existing benchmarks.

For systems to respond to scenarios that were unforeseen at design time, they must be capable of safely adapting, at runtime, the assumptions they make about the environment, the goals they are expected to achieve, and the strategy that guarantees the goals are fulfilled if the assumptions hold. Such adaptation often involves the system degrading its functionality, by weakening its environment assumptions and/or the goals it aims to meet, ideally in a graceful manner. However, finding weaker assumptions that account for the unanticipated behaviour and of goals that are achievable in the new environment in a systematic and safe way remains an open challenge. In this paper, we propose a novel framework that supports assumption and, if necessary, goal degradation to allow systems to cope with runtime assumption violations. The framework, which integrates into the MORPH reference architecture, combines symbolic learning and reactive synthesis to compute implementable controllers that may be deployed safely. We describe and implement an algorithm that illustrates the working of this framework. We further demonstrate in our evaluation its effectiveness and applicability to a series of benchmarks from the literature. The results show that the algorithm successfully learns realizable specifications that accommodate previously violating environment behaviour in almost all cases. Exceptions are discussed in the evaluation.

Specification learning and controller synthesis are two methods that promise to provide control systems with assured adaptive capabilities at run-time. Specification learning can automatically update specifications in light of violation traces observed within the operational environment. Controller synthesis can then automatically generate implementations that are guaranteed to satisfy these specifications in every environment.Specification learning is implemented using general-purpose AI systems. These systems are highly configurable, and the configuration choice heavily affects the effectiveness. Setting configuration parameters is far from obvious as they bear no clear semantic relation with the adaptation task. State of the art requires configurations to be set by domain experts at design time for each application domain.In this paper, we argue that to create assured control systems that can effectively and efficiently adapt at run-time, the learning systems upon which they are built must also have adaptive learning strategies for determining configurations at runtime. We demonstrate this idea with a proof-of-concept that computes domain-dependent policies using reinforcement learning.

The engineering of high-quality software requirements generally relies on properties and assumptions about the environment in which the software-to-be has to operate. Such properties and assumptions, referred to as environment conditions in this paper, are highly subject to change over time or from one software variant to another. As a consequence, the requirements engineered for a specific set of environment conditions may no longer be adequate, complete and consistent for another set.

Consider a policymaker who wants to decide which intervention to perform in order to change a currently undesirable situation. The policymaker has at her disposal a team of experts, each with their own understanding of the causal dependencies between different factors contributing to the outcome. The policymaker has varying degrees of confidence in the experts’ opinions. She wants to combine their opinions in order to decide on the most effective intervention. We formally define the notion of an effective intervention, and then consider how experts’ causal judgments can be combined in order to determine the most effective intervention. We define a notion of two causal models being compatible, and show how compatible causal models can be combined. We then use it as the basis for combining experts causal judgments. We illustrate our approach on a number of real-life examples.

Abstract When dealing with unrealizable specifications in reactive synthesis, finding the weakest environment assumptions that ensure realizability is often considered a desirable property. However, little effort has been dedicated to defining or evaluating the notion of weakness of assumptions formally. The question of whether one assumption is weaker than another is commonly interpreted by considering the implication relationship between the two or, equivalently, their language inclusion. This interpretation fails to provide any insight into the weakness of the assumptions when implication (or language inclusion) does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it cannot distinguish the weakness of assumptions expressed as fairness properties. In this paper, we propose a refined measure of weakness based on combining entropy with Hausdorff dimension, a concept that captures the notion of size of the ω -language satisfying a linear temporal logic formula. We focus on a special subset of linear temporal logic formulae which is of particular interest in reactive synthesis, called GR(1). We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae, and propose a refined measure to cover cases when two formulae are strictly ordered by implication but have the same entropy and Hausdorff dimension. We prove the consistency between our weakness measure and logical implication, that is, if one formula implies another, the latter is weaker than the former according to our measure. We evaluate our proposed weakness measure in two contexts. The first is in computing GR(1) assumption refinements where our weakness measure is used as a heuristic to drive the refinement search towards weaker solutions. The second is in the context of quantitative model checking where it is used to measure the size of the language of a model violating a linear temporal logic formula.

Forensic readiness denotes the capability of a system to support digital forensic investigations of potential, known incidents by preserving in advance data that could serve as evidence explaining how an incident occurred. Given the increasing rate at which (potentially criminal) incidents occur, designing so‰ware systems that are forensic-ready can facilitate and reduce the costs of digital forensic investigations. However, to date, little or no attention has been given to how forensic-ready so‰ftware systems can be designed systematically. In this paper we propose to explicitly represent evidence preservation requirements prescribing preservation of the minimal amount of data that would be relevant to a future digital investigation. We formalise evidence preservation requirements and propose an approach for synthesising specifications for systems to meet these requirements. We present our prototype implementation—based on a satisfiability solver and a logic-based learner—which we use to evaluate our approach, applying it to two digital forensic corpora. Our evaluation suggests that our approach preserves relevant data that could support hypotheses of potential incidents. Moreover, it enables significant reduction in the volume of data that would need to be examined during an investigation.

Requirements incompleteness is often the result of unanticipated adverse conditions which prevent the software and its environment from behaving as expected. These conditions represent risks that can cause severe software failures. The identification and resolution of such risks is therefore a crucial step towards requirements completeness. Obstacle analysis is a goal-driven form of risk analysis that aims at detecting missing conditions that can obstruct goals from being satisfied in a given domain, and resolving them.

Goal-oriented requirements engineering approaches propose capturing how a system should behave through the specification of high-level goals, from which requirements can then be systematically derived. Goals may however admit subtle situations that make them diverge, i.e., not be satisfiable as a whole under specific circumstances feasible within the domain, called boundary conditions. While previous work allows one to identify boundary conditions for conflicting goals written in LTL, it does so through a pattern-based approach, that supports a limited set of patterns, and only produces pre-determined formulations of boundary conditions.

Goal oriented methods have been successfully employed for eliciting and elaborating software requirements. When goals are assigned to an agent, they have to be operationalised: the agent’s operations have to be refined, by equipping them with appropriate enabling and triggering conditions, so that the goals are fulfilled. Goal operationalisation generally demands a significant effort of the engineer. Although there exist approaches that tackle this problem, they are either informal or at most semi automated, requiring the engineer to assist in the process. In this paper, we present an approach for goal operationalisation that automatically computes required preconditions and required triggering conditions for operations, so that the resulting operations establish the goals. The process is iterative, is able to deal with safety goals and particular kinds of liveness goals, and is based on the use of interpolation and SAT solving.

The purpose of requirements validation is to determine whether a large requirements set will lead to the achievement of system-related goals under different conditions — a task that needs automation if it is to be performed quickly and accurately. One reason for the current lack of software tools to undertake such validation is the absence of the computational mechanisms needed to associate scenario, system specification and goal analysis tools. Therefore, in this paper, we report first research experiments in developing these new capabilities, and demonstrate them with a non-trivial example associated with a Rolls Royce aircraft engine software component.

The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer's knowledge of the domain and the envisioned system.

Missing requirements are known to be among the major causes of software failure. They often result from a natural inclination to conceive over-ideal systems where the software-to-be and its environment always behave as expected. Obstacle analysis is a goal-anchored form of risk analysis whereby exceptional conditions that may obstruct system goals are identified, assessed and resolved to produce complete requirements. Various techniques have been proposed for identifying obstacle conditions systematically. Among these, the formal ones have limited applicability or are costly to automate. This paper describes a tool-supported technique for generating a set of obstacle conditions guaranteed to be complete and consistent with respect to the known domain properties. The approach relies on a novel combination of model checking and learning technologies. Obstacles are iteratively learned from counterexample and witness traces produced by model checking against a goal and converted into positive and negative examples, respectively. A comparative evaluation is provided with respect to published results on the manual derivation of obstacles in a real safety-critical system for which failures have been reported.

Abstract One of the difficulties in goal-oriented requirements engineering (GORE) is the construction of behaviour models from declarative goal specifications. This paper addresses this problem using a combination of model checking and machine learning. First, a goal model is transformed into a (potentially Zeno) behaviour model. Then, via an iterative process, Zeno traces are identified by model checking the behaviour model against a time progress property, and inductive logic programming (ILP) is used to learn operational requirements ( pre-conditions ) that eliminate these traces. The process terminates giving a non-Zeno behaviour model produced from the learned pre-conditions and the given goal model.

Goal-oriented methods have increasingly been recognised as an effective means for eliciting, elaborating, analysing and specifying software requirements. A key activity in these approaches is the elaboration of a correct and complete set of opertional requirements, in the form of pre- and trigger-conditions, that guarantee the system goals. Few existing approaches provide support for this crucial task and mainly rely on significant effort and expertise of the engineer. In this paper we propose a tool-based framework that combines model checking, inductive learning and scenarios for elaborating operational requirements from goal models. This is an iterative process that requires the engineer to identify positive and negative scenarios from counterexamples to the goals, generated using model checking, and to select operational requirements from suggestions computed by inductive learning.