-
Inconsistency Masks: Removing the Uncertainty from Input-Pseudo-Label Pairs
Authors:
Michael R. H. Vorndran,
Bernhard F. Roeck
Abstract:
Efficiently generating sufficient labeled data remains a major bottleneck in deep learning, particularly for image segmentation tasks where labeling requires significant time and effort. This study tackles this issue in a resource-constrained environment, devoid of extensive datasets or pre-existing models. We introduce Inconsistency Masks (IM), a novel approach that filters uncertainty in image-p…
▽ More
Efficiently generating sufficient labeled data remains a major bottleneck in deep learning, particularly for image segmentation tasks where labeling requires significant time and effort. This study tackles this issue in a resource-constrained environment, devoid of extensive datasets or pre-existing models. We introduce Inconsistency Masks (IM), a novel approach that filters uncertainty in image-pseudo-label pairs to substantially enhance segmentation quality, surpassing traditional semi-supervised learning techniques. Employing IM, we achieve strong segmentation results with as little as 10% labeled data, across four diverse datasets and it further benefits from integration with other techniques, indicating broad applicability. Notably on the ISIC 2018 dataset, three of our hybrid approaches even outperform models trained on the fully labeled dataset. We also present a detailed comparative analysis of prevalent semi-supervised learning strategies, all under uniform starting conditions, to underline our approach's effectiveness and robustness. The full code is available at: https://github.com/MichaelVorndran/InconsistencyMasks
△ Less
Submitted 13 April, 2024; v1 submitted 25 January, 2024;
originally announced January 2024.
-
Synthesizing Adaptive Test Strategies from Temporal Logic Specifications
Authors:
Roderick Bloem,
Goerschwin Fey,
Fabian Greif,
Robert Koenighofer,
Ingo Pill,
Heinz Riener,
Franz Roeck
Abstract:
Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in every realization of t…
▽ More
Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in every realization of the specification and for every behavior of the uncontrollable part of the system's environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. Based on well-established hypotheses from fault-based testing, we argue that such tests are also sensitive for more complex bugs. Since the specification may not define the system behavior completely, we use reactive synthesis algorithms with partial information. The computed strategies are adaptive test strategies that react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing.
△ Less
Submitted 5 September, 2018;
originally announced September 2018.
-
A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Authors:
Ezio Bartocci,
Roderick Bloem,
Dejan Nickovic,
Franz Roeck
Abstract:
We consider the problem of monitoring a Linear Time Logic (LTL) specification that is defined on infinite paths, over finite traces. For example, we may need to draw a verdict on whether the system satisfies or violates the property "p holds infinitely often." The problem is that there is always a continuation of a finite trace that satisfies the property and a different continuation that violates…
▽ More
We consider the problem of monitoring a Linear Time Logic (LTL) specification that is defined on infinite paths, over finite traces. For example, we may need to draw a verdict on whether the system satisfies or violates the property "p holds infinitely often." The problem is that there is always a continuation of a finite trace that satisfies the property and a different continuation that violates it.
We propose a two-step approach to address this problem. First, we introduce a counting semantics that computes the number of steps to witness the satisfaction or violation of a formula for each position in the trace. Second, we use this information to make a prediction on inconclusive suffixes. In particular, we consider a good suffix to be one that is shorter than the longest witness for a satisfaction, and a bad suffix to be shorter than or equal to the longest witness for a violation. Based on this assumption, we provide a verdict assessing whether a continuation of the execution on the same system will presumably satisfy or violate the property.
△ Less
Submitted 9 April, 2018;
originally announced April 2018.
