-
Counterfactual Explanations for MITL Violations
Authors:
Bernd Finkbeiner,
Felix Jahn,
Julian Siber
Abstract:
MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed automata. A violation of an MITL specification is then witnessed by a timed trace of the network, i.e., an execution consisting of both discrete actions and real…
▽ More
MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed automata. A violation of an MITL specification is then witnessed by a timed trace of the network, i.e., an execution consisting of both discrete actions and real-valued delays between these actions. Finding and fixing the root cause of such a violation requires significant manual effort since both discrete actions and real-time delays have to be considered. In this paper, we present an automatic explanation method that eases this process by computing the root causes for the violation of an MITL specification on the execution of a network of timed automata. This method is based on newly developed definitions of counterfactual causality tailored to networks of timed automata in the style of Halpern and Pearl's actual causality. We present and evaluate a prototype implementation that demonstrates the efficacy of our method on several benchmarks from the literature.
△ Less
Submitted 9 May, 2025; v1 submitted 29 November, 2024;
originally announced December 2024.
-
Acting for the Right Reasons: Creating Reason-Sensitive Artificial Moral Agents
Authors:
Kevin Baum,
Lisa Dargasz,
Felix Jahn,
Timo P. Gros,
Verena Wolf
Abstract:
We propose an extension of the reinforcement learning architecture that enables moral decision-making of reinforcement learning agents based on normative reasons. Central to this approach is a reason-based shield generator yielding a moral shield that binds the agent to actions that conform with recognized normative reasons so that our overall architecture restricts the agent to actions that are (…
▽ More
We propose an extension of the reinforcement learning architecture that enables moral decision-making of reinforcement learning agents based on normative reasons. Central to this approach is a reason-based shield generator yielding a moral shield that binds the agent to actions that conform with recognized normative reasons so that our overall architecture restricts the agent to actions that are (internally) morally justified. In addition, we describe an algorithm that allows to iteratively improve the reason-based shield generator through case-based feedback from a moral judge.
△ Less
Submitted 25 October, 2024; v1 submitted 23 September, 2024;
originally announced September 2024.
-
Grayscale Electron Beam Lithography Direct Patterned Antimony Sulfide
Authors:
Wei Wang,
Uwe Hübner,
Tao Chen,
Anne Gärtner,
Joseph Köbel,
Franka Jahn,
Henrik Schneidwind,
Andrea Dellith,
Jan Dellith,
Torsten Wieduwilt,
Matthias Zeisberger,
Tanveer Ahmed Shaik,
Astrid Bingel,
Markus A Schmidt,
Jer-Shing Huang,
Volker Deckert
Abstract:
The rise of micro/nanooptics and lab-on-chip devices demands the fabrication of three-dimensional structures with decent resolution. Here, we demonstrate the combination of grayscale electron beam lithography and direct forming methodology to fabricate antimony sulfide structures with free form for the first time. The refractive index of the electron beam patterned structure was calculated based o…
▽ More
The rise of micro/nanooptics and lab-on-chip devices demands the fabrication of three-dimensional structures with decent resolution. Here, we demonstrate the combination of grayscale electron beam lithography and direct forming methodology to fabricate antimony sulfide structures with free form for the first time. The refractive index of the electron beam patterned structure was calculated based on an optimization algorithm that is combined with genetic algorithm and transfer matrix method. By adopting electron irradiation with variable doses, 4-level Fresnel Zone Plates and metalens were produced and characterized. This method can be used for the fabrication of three-dimensional diffractive optical elements and metasurfaces in a single step manner.
△ Less
Submitted 24 January, 2024;
originally announced January 2024.
-
A Study on Quantifying Sim2Real Image Gap in Autonomous Driving Simulations Using Lane Segmentation Attention Map Similarity
Authors:
Seongjeong Park,
Jinu Pahk,
Lennart Lorenz Freimuth Jahn,
Yongseob Lim,
Jinung An,
Gyeungho Choi
Abstract:
Autonomous driving simulations require highly realistic images. Our preliminary study found that when the CARLA Simulator image was made more like reality by using DCLGAN, the performance of the lane recognition model improved to levels comparable to real-world driving. It was also confirmed that the vehicle's ability to return to the center of the lane after deviating from it improved significant…
▽ More
Autonomous driving simulations require highly realistic images. Our preliminary study found that when the CARLA Simulator image was made more like reality by using DCLGAN, the performance of the lane recognition model improved to levels comparable to real-world driving. It was also confirmed that the vehicle's ability to return to the center of the lane after deviating from it improved significantly. However, there is currently no agreed-upon metric for quantitatively evaluating the realism of simulation images. To address this issue, based on the idea that FID (Fréchet Inception Distance) measures the feature vector distribution distance using a pre-trained model, this paper proposes a metric that measures the similarity of simulation road images using the attention map from the self-attention distillation process of ENet-SAD. Finally, this paper verified the suitability of the measurement method by applying it to the image of the CARLA map that implemented a realworld autonomous driving test road.
△ Less
Submitted 18 June, 2023;
originally announced June 2023.
-
An FPTAS of Minimizing Total Weighted Completion Time on Single Machine with Position Constraint
Authors:
G. Calinescu,
F. Jaehn,
M. Li,
K. Wang
Abstract:
In this paper we study the classical scheduling problem of minimizing the total weighted completion time on a single machine with the constraint that one specific job must be scheduled at a specified position. We give dynamic programs with pseudo-polynomial running time, and a fully polynomial-time approximation scheme (FPTAS).
In this paper we study the classical scheduling problem of minimizing the total weighted completion time on a single machine with the constraint that one specific job must be scheduled at a specified position. We give dynamic programs with pseudo-polynomial running time, and a fully polynomial-time approximation scheme (FPTAS).
△ Less
Submitted 30 October, 2017;
originally announced October 2017.
-
Regular Ideal Languages and Their Boolean Combinations
Authors:
Franz Jahn,
Manfred Kufleitner,
Alexander Lauser
Abstract:
We consider ideals and Boolean combinations of ideals. For the regular languages within these classes we give expressively complete automaton models. In addition, we consider general properties of regular ideals and their Boolean combinations. These properties include effective algebraic characterizations and lattice identities.
In the main part of this paper we consider the following determinis…
▽ More
We consider ideals and Boolean combinations of ideals. For the regular languages within these classes we give expressively complete automaton models. In addition, we consider general properties of regular ideals and their Boolean combinations. These properties include effective algebraic characterizations and lattice identities.
In the main part of this paper we consider the following deterministic one-way automaton models: unions of flip automata, weak automata, and Staiger-Wagner automata. We show that each of these models is expressively complete for regular Boolean combination of right ideals. Right ideals over finite words resemble the open sets in the Cantor topology over infinite words. An omega-regular language is a Boolean combination of open sets if and only if it is recognizable by a deterministic Staiger-Wagner automaton; and our result can be seen as a finitary version of this classical theorem. In addition, we also consider the canonical automaton models for right ideals, prefix-closed languages, and factorial languages.
In the last section, we consider a two-way automaton model which is known to be expressively complete for two-variable first-order logic. We show that the above concepts can be adapted to these two-way automata such that the resulting languages are the right ideals (resp. prefix-closed languages, resp. Boolean combinations of right ideals) definable in two-variable first-order logic.
△ Less
Submitted 25 May, 2012; v1 submitted 24 February, 2011;
originally announced February 2011.
