85 results
Filters
Settings
Now showing1 - 10 of 85
- Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , Local explanations for classification of ventilation data by neural networksNeural networks (NNs) have great potential to improve individualization of medicine, e.g., through analysis of signals. However, they are generally not interpretable. Understanding NN decisions is crucial, especially in safety-critical domains such as medicine. This work presents a new method to provide local explanations for classifications of signals made by NNs. Our method extends the Sig-LIME explanation method from one-dimensional signals to multidimensional signals by introducing new perturbation techniques. We evaluate the proposed method on an NN that classifies the positive end-expiratory pressure (PEEP) applied by a ventilator. The evaluation shows that the generated explanations are plausible, stable and concise.Publicationtype: Conference Paper18 8 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , A provably safe controller for the needle-steering problem using online strategy synthesisAutonomous systems often address complex planning problems, which require both prospective action planning and retrospective data evaluation. Timed games could aid since they automatically synthesize strategies that, provably correct, solve those planning problems; yet, they assume a static model of the environment, which is not realistic for autonomous systems. However, many autonomous systems are control applications, which employ sensors that capture system behavior at run time and can thus compensate for incomplete knowledge at modeling time. In this paper, we propose an online strategy synthesis, which, based on offline strategy synthesis on the one hand and on sensor information about the current state of the physical world on the other hand, derives formal safety guarantees while reacting and adapting to environment changes. We formalize the needle-steering problem from medical robotics, i.e., the problem of navigating a (flexible and beveled) needle through partially unknown tissue towards a target without damaging its surroundings, by interpreting it as a timed game. Further, we introduce a new representation of its environment through different region types that determine the acceptance of action plans and trigger local correcting actions. We present an algorithm for online strategy synthesis and, for the given region representation, formally prove that it returns safe online controllers. The algorithm is implemented on top of Uppaal Stratego. For two medical applications of needle steering, peridural anesthesia and predefined needle trajectory, we demonstrate the necessity of online adjustments in a series of simulations with various degrees of initial knowledge about the environment, and show that the overhead of online synthesis remains practical.Publicationtype: Journal Article34 26 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , Configurable abstraction of signals using signal temporal logicAbstractions of signals help to avoid cognitive and storage overload, especially in systems with many signals such as cyber-physical systems (CPS). For assessing trends and reconstructing behavior, it often suffices to have a rough understanding how signals evolve, e.g., whether their behavior is monotonic or periodic. This work provides a configurable abstraction of signal behavior, where signals are described by a sequence of oscillation and linear patterns. We formalize templates of both behaviors in parameterized signal temporal logic (PSTL) and provide an algorithm that abstracts signals in terms of those patterns. The templates are configurable such that they allow for choosing the level of abstraction, e.g., by limiting the approximation error or the minimal oscillation frequency. For segmentation of the signal, we solve an optimization problem using a modified version of TeLEx. The evaluation demonstrates that configuration of the patterns is suitable to define the level of abstraction. Further, on control output from the ARCH wind turbine benchmark and flow data from medical ventilation, it demonstrates that the abstraction method can be applied to real-world signals.Publicationtype: Conference Paper27 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , SLS-enhanced core-boosted linear search for anytime maximum satisfiability(Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 2025-08-08); Maximum Satisfiability (MaxSAT), the constraint paradigm of minimizing a linear expression over Boolean (0-1) variables subject to a set of propositional clauses, is today used for solving NP-hard combinatorial optimization problems in various domains. Especially anytime MaxSAT solvers that compute low-cost solutions within a limited available computational time have significantly improved in recent years. Such solvers can be divided into SAT-based methods that use sophisticated reasoning, and stochastic local search (SLS) methods that heuristically explore the search space. The two are complementary; roughly speaking, SLS struggles with finding feasible solutions, and SAT-based methods with minimizing cost. Consequently, most state-of-the-art anytime MaxSAT solvers run SLS before a SAT-based algorithm with minimal communication between the two. In this paper, we aim to harness the complementary strengths of SAT-based, and SLS approaches in the context of anytime MaxSAT. More precisely, we describe several ways to enhance the performance of the so-called core-boosted linear search algorithm for anytime MaxSAT with SLS techniques. Core-boosted linear search is a three-phase algorithm where each phase uses different types of reasoning. Beyond MaxSAT, core-boosted search has also been successful in the related paradigms of pseudo-boolean optimization and constraint programming. We describe how an SLS approach to MaxSAT can be tightly integrated with all three phases of the algorithm, resulting in non-trivial information exchange in both directions between the SLS algorithm and the reasoning methods. We evaluate our techniques on standard benchmarks from the latest MaxSAT Evaluation and demonstrate that our techniques can noticeably improve on implementations of core-boosted search and SLS.Publicationtype: Conference Paper23 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , Efficient adversarial generation through selective SBFL guidance and automated sub-model strategyFast Gradient Sign Method (FGSM) is an effective method for generating adversarial inputs for neural networks, but it is memory-intensive. DeepFault reduces the memory costs of FGSM by transferring Spectrum-Based Fault Localization (SBFL) to neural networks. SBFL is a technique traditionally using the execution trace of a program to iden-tify suspicious code locations that are likely to contain faults. DeepFault employs SBFL to identify neurons in a neural network that are likely to be responsible for misclassifications to guide FGSM. We propose an adjustable SBFL-guided adversarial input generation approach that addresses both memory and runtime efficiency challenges for sequential classification models. Our contributions include: (1) an automated and adjustable sub-model strategy that selects smaller model configurations for input synthesis, reducing both memory overhead and computational effort, (2) vector-based hit-spectrum computation using GPU-accelerated operations to significantly reduce computation time (3) targeted adversarial input generation enabling modifications in favor of specific target classes, and (4) comprehensive experimental evaluation on contemporary sequential neural network architectures. Our evaluation demonstrates substantial improvements over existing methods: up to 4.7× memory reduction compared to FGSM and up to 301× speedup over DeepFault while maintaining comparable adversarial input quality. All experiments complete within tens of seconds, demonstrating practical scalability for contemporary models.Publicationtype: Conference Paper11 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , A model template for reachability-based containment checking of imprecise observations in timed automataVerifying safety requirements by model checking becomes increasingly important for safety-critical applications. For the validity of such proof in practice, the model needs to capture the actual behavior of the real system, which could be tested by containment checks of real observation traces. Basic equivalence checks, however, are not applicable if the system is only partially or imprecisely observable, if the model abstracts from explicit states with symbolic semantics, or if the checks are not expressible in the logics supported by a model checker. In this article, we solve the problem of observation containment checking in timed automata via reachability checking on tester systems. We introduce the logic SRL (sequence reachability logic) to express observations as sequences of delayed reachability properties. Through SBLL (introduced by Aceto et al.) as intermediate logic, we synthesize a set of matcher model templates for partial and imprecise observations and further extend these templates for the case of limited state accessibility in a model. For the obtained matching traces, we define the back-transformation into the original model domain and formally prove the correctness of the transformation. We implemented the observation matching approach, and apply it to a set of 7 demo and 3 case study models with different levels of observability. The results show that all positive and negative observations are correctly classified, and that the most advanced matcher model instance still offers average run times between 0.1 and 1 s in all but 3 scenarios.Publicationtype: Journal Article17 89 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , Efficient Hit-Spectrum-Guided Fast Gradient Sign Method: An Adjustable Approach with Memory and Runtime OptimizationsFast Gradient Sign Method (FGSM) is an effective method for generating adversarial inputs for neural networks, but it is memory-intensive. DeepFault reduces the memory costs of FGSM by transferring Spectrum-Based Fault Localization to neural networks. SBFL is a technique traditionally using the execution trace of a program to identify suspicious code locations that are likely to contain faults. DeepFault employs SBFL to identify neurons in a neural network that are likely to be responsible for misclassifications to guide FGSM. We propose an adjustable hit-spectrum-guided FGSM approach applying a sub-model strategy to avoid gradient ascent evaluation over the entire model. Additionally, we alter DeepFault’s hit-spectrum computation to be vector-based to allow parallelization of computation, and we modify the hit spectrum to depend on a specific class to allow targeted adversarial input generation. We conduct an experimental evaluation on image classification models showing how our app roach allows trading off effectiveness of adversarial input generation with reduced runtimes while maintaining scalability regarding larger models, with maximum runtimes on the order of tens of seconds. For larger sample sizes, our approach reduces runtimes to fractions of 1/300 and less compared to DeepFault. When processing larger models, it requires only one-third of FGSM’s memory usage.Publicationtype: Conference Paper20 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , IGMaxHS - An Incremental MaxSAT Solver with Support for XOR Clauses(2024-10-21)Recently, a novel, MaxSAT-based method for error correction in quantum computing has been proposed that requires both incremental MaxSAT solving capabilities and support for XOR constraints, but no dedicated MaxSAT solver fulfilling these criteria existed yet. We alleviate that and introduce IGMaxHS, which is based on the existing solvers iMaxHS and GaussMaxHS, but poses fewer restrictions on the XOR constraints than GaussMaxHS. IGMaxHS is fuzz tested with xwcnfuzz, an extension of wcnfuzz that can directly output XOR constraints. As a result, IGMaxHS is the only solver that reported neither incorrect unsatisfiability verdicts nor invalid models nor incoherent cost model combinations in a final fuzz testing comparison of all three solvers with 10000 instances. We detail the steps required for implementing Gaussian elimination on XOR constraints in CDCL SAT solvers, and extend the recently proposed re-entrant incremental MaxSAT solver application program interface to allow for incremental addition of XOR constraints. Finally, we show that IGMaxHS is capable of decoding quantum color codes through simulation with the Munich Quantum Toolkit.Publicationtype: Conference Paper not in Proceedings28 41 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: with files , noSAT-MaxSATv3Using a SAT solver to solve MaxSAT is a well-established and efficient method. However, in resource-constrained computing environments, e.g., embedded systems, such algorithm designs can be hard to realize. With noSAT-MaxSAT, we explore alternatives that do not rely on an external, dedicated SAT solver. Compared to the previous version, the most notable changes in noSAT-MaxSATv3 include an update of the base algorithm to NuWLS-2.0, new rules for restarting, the integration of a new Frequency Fitness Assignment-inspired variable selection heuristic in local optima, and the inclusion of fixed-precision integer arithmetic to increase precision in weight calculations without resorting to floating-point numbers.Publicationtype: Conference Paper52 77 - Some of the metrics are blocked by yourconsent settings
Item type:Publication, Access status: without files , Repairing neural networks for image classification problems using spectrum-based fault localizationFault localization in neural networks develops methods to improve a model's accuracy, resilience, and performance. Improving a model's accuracy without extensive gradient descent training loops has not been a goal, yet. In this paper, we propose a novel model repair approach identifying suspicious neurons to be selected for modifications of greater impact upon a single iteration avoiding extensive training processes with the gradient descent method yielding potential overfitting. Our approach uses Spectrum-Based Fault Localization to guide the repair process. Spectrum-Based Fault Localization is an established method that assigns software code a suspiciousness value indicating a likelihood for fault presence depending on test suite outcomes and the associated code's execution. We employ hit-spectrum analysis to assign neurons a suspiciousness score. Our algorithm selects especially suspicious neurons for repair by reducing their activation values, while increasing the activation values of less suspicious neurons. Experiments conducted on convolutional layer and dense layer image classification models confirm that, overall, our approach leads to better mean accuracies. In 2 scenarios, the repair approach has led to small accuracy improvements by increasing the corresponding models' mean accuracies by 0.68 and 0.46 percentage points respectively. Remarkably, our repair approach has also led to significant accuracy improvements by increasing a specific model's accuracy by 15.73 percentage points. In conclusion, our method provides a promising alternative to additional training epochs running the risk of overfitting or depending on larger databases for the training process.Publicationtype: Conference Paper20