-
Human-Machine Interface Evaluation Using EEG in Driving Simulator
Authors:
Y. C. Liu,
N. Figalova,
M. Baumann,
K Bengler
Abstract:
Automated vehicles are pictured as the future of transportation, and facilitating safer driving is only one of the many benefits. However, due to the constantly changing role of the human driver, users are easily confused and have little knowledge about their responsibilities. Being the bridge between automation and human, the human-machine interface (HMI) is of great importance to driving safety.…
▽ More
Automated vehicles are pictured as the future of transportation, and facilitating safer driving is only one of the many benefits. However, due to the constantly changing role of the human driver, users are easily confused and have little knowledge about their responsibilities. Being the bridge between automation and human, the human-machine interface (HMI) is of great importance to driving safety. This study was conducted in a static driving simulator. Three HMI designs were developed, among which significant differences in mental workload using NASA-TLX and the subjective transparency test were found. An electroencephalogram was applied throughout the study to determine if differences in the mental workload could also be found using EEG's spectral power analysis. Results suggested that more studies are required to determine the effectiveness of the spectral power of EEG on mental workload, but the three interface designs developed in this study could serve as a solid basis for future research to evaluate the effectiveness of psychophysiological measures. Marie Sklodowska-Curie Actions; Innovative Training Network (ITN); SHAPE-IT; Grant number 860410; Publication date: [27 July 2023]; DOI: [10.1109/IV55152.2023.10186567]
△ Less
Submitted 13 June, 2024;
originally announced June 2024.
-
DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing
Authors:
Yuandong Cyrus Liu,
Ton-Chanh Le,
Timos Antonopoulos,
Eric Koskinen,
ThanhVu Nguyen
Abstract:
For many decades, advances in static verification have focused on linear integer arithmetic (LIA) programs. Many real-world programs are, however, written with non-linear integer arithmetic (NLA) expressions, such as programs that model physical events, control systems, or nonlinear activation functions in neural networks. While there are some approaches to reasoning about such NLA programs, still…
▽ More
For many decades, advances in static verification have focused on linear integer arithmetic (LIA) programs. Many real-world programs are, however, written with non-linear integer arithmetic (NLA) expressions, such as programs that model physical events, control systems, or nonlinear activation functions in neural networks. While there are some approaches to reasoning about such NLA programs, still many verification tools fall short when trying to analyze them.
To expand the scope of existing tools, we introduce a new method of converting programs with NLA expressions into semantically equivalent LIA programs via a technique we call dual rewriting. Dual rewriting discovers a linear replacement for an NLA Boolean expression (e.g. as found in conditional branching), simultaneously exploring both the positive and negative side of the condition, and using a combination of static validation and dynamic generalization of counterexamples. While perhaps surprising at first, this is often possible because the truth value of a Boolean NLA expression can be characterized in terms of a Boolean combination of linearly-described regions/intervals where the expression is true and those where it is false.
The upshot is that rewriting NLA expressions to LIA expressions beforehand enables off-the-shelf LIA tools to be applied to the wider class of NLA programs. We built a new tool DrNLA and show it can discover LIA replacements for a variety of NLA programs. We then applied our work to branching-time verification of NLA programs, creating the first set of such benchmarks (92 in total) and showing that DrNLA's rewriting enable tools such as FuncTion and T2 to verify CTL properties of 42 programs that previously could not be verified. We also show a potential use of DrNLA assisting Frama-C in program slicing, and report that execution speed is not impacted much by rewriting.
△ Less
Submitted 27 June, 2023;
originally announced June 2023.
-
Position Bias Estimation with Item Embedding for Sparse Dataset
Authors:
Shion Ishikawa,
Yun Ching Liu,
Young-Joo Chung,
Yu Hirate
Abstract:
Estimating position bias is a well-known challenge in Learning to Rank (L2R). Click data in e-commerce applications, such as targeted advertisements and search engines, provides implicit but abundant feedback to improve personalized rankings. However, click data inherently includes various biases like position bias. Based on the position-based click model, Result Randomization and Regression Expec…
▽ More
Estimating position bias is a well-known challenge in Learning to Rank (L2R). Click data in e-commerce applications, such as targeted advertisements and search engines, provides implicit but abundant feedback to improve personalized rankings. However, click data inherently includes various biases like position bias. Based on the position-based click model, Result Randomization and Regression Expectation-Maximization algorithm (REM) have been proposed to estimate position bias, but they require various paired observations of (item, position). In real-world scenarios of advertising, marketers frequently display advertisements in a fixed pre-determined order, which creates difficulties in estimation due to the limited availability of various pairs in the training data, resulting in a sparse dataset. We propose a variant of the REM that utilizes item embeddings to alleviate the sparsity of (item, position). Using a public dataset and internal carousel advertisement click dataset, we empirically show that item embedding with Latent Semantic Indexing (LSI) and Variational Auto-Encoder (VAE) improves the accuracy of position bias estimation and the estimated position bias enhances Learning to Rank performance. We also show that LSI is more effective as an embedding creation method for position bias estimation.
△ Less
Submitted 11 March, 2024; v1 submitted 9 May, 2023;
originally announced May 2023.
-
Source-Level Bitwise Branching for Temporal Verification
Authors:
Yuandong Cyrus Liu,
Ton-Chanh Le,
Eric Koskinen
Abstract:
There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. Still, verification tools are limited on termination and LTL verification of bitvector programs. In this work, we show that sim…
▽ More
There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. Still, verification tools are limited on termination and LTL verification of bitvector programs. In this work, we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We present two sets of rules, namely rewriting rules and weakening rules, that can be implemented as bitwise branching of program transformation, the branching path can facilitate verification tools widen verification tasks over bitvector programs. Our experiment shows this exploitation of integer reasoning and interpolation enables competitive termination verification of bitvector programs and leads to the first effective technique for LTL verification of bitvector programs.
△ Less
Submitted 4 November, 2021;
originally announced November 2021.
-
End-to-end Neural Diarization: From Transformer to Conformer
Authors:
Yi Chieh Liu,
Eunjung Han,
Chul Lee,
Andreas Stolcke
Abstract:
We propose a new end-to-end neural diarization (EEND) system that is based on Conformer, a recently proposed neural architecture that combines convolutional mappings and Transformer to model both local and global dependencies in speech. We first show that data augmentation and convolutional subsampling layers enhance the original self-attentive EEND in the Transformer-based EEND, and then Conforme…
▽ More
We propose a new end-to-end neural diarization (EEND) system that is based on Conformer, a recently proposed neural architecture that combines convolutional mappings and Transformer to model both local and global dependencies in speech. We first show that data augmentation and convolutional subsampling layers enhance the original self-attentive EEND in the Transformer-based EEND, and then Conformer gives an additional gain over the Transformer-based EEND. However, we notice that the Conformer-based EEND does not generalize as well from simulated to real conversation data as the Transformer-based model. This leads us to quantify the mismatch between simulated data and real speaker behavior in terms of temporal statistics reflecting turn-taking between speakers, and investigate its correlation with diarization error. By mixing simulated and real data in EEND training, we mitigate the mismatch further, with Conformer-based EEND achieving 24% error reduction over the baseline SA-EEND system, and 10% improvement over the best augmented Transformer-based system, on two-speaker CALLHOME data.
△ Less
Submitted 14 June, 2021;
originally announced June 2021.
-
Proving LTL Properties of Bitvector Programs and Decompiled Binaries (Extended)
Authors:
Yuandong Cyrus Liu,
Chengbin Pang,
Daniel Dietsch,
Eric Koskinen,
Ton-Chanh Le,
Georgios Portokalidis,
Jun Xu
Abstract:
There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. In this paper we show that similar linear arithmetic approximation of bitvector operations can be done at the s…
▽ More
There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. In this paper we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We show that, for reachability of bitvector programs, increased branching incurs negligible overhead yet, when combined with integer interpolation optimizations, enables more programs to be verified. We further show this exploitation of integer interpolation in the common case also enables competitive termination verification of bitvector programs and leads to the first effective technique for LTL verification of bitvector programs. Finally, we provide an in-depth case study of decompiled ("lifted") binary programs, which emulate X86 execution through frequent use of bitvector operations. We present a new tool DarkSea, the first tool capable of verifying reachability, termination, and LTL of lifted binaries.
△ Less
Submitted 28 August, 2021; v1 submitted 11 May, 2021;
originally announced May 2021.
-
Study of mechanical response in embossing of ceramic green substrate by micro-indentation
Authors:
Y. C. Liu,
X. -C. Shan
Abstract:
Micro-indentation test with a micro flat-end cone indenter was employed to simulate micro embossing process and investigate the thermo-mechanical response of ceramic green substrates. The laminated low temperature co-fired ceramic green tapes were used as the testing material ; the correlations of indentation depth versus applied force and applied stress at the temperatures of 25 degrees C and 7…
▽ More
Micro-indentation test with a micro flat-end cone indenter was employed to simulate micro embossing process and investigate the thermo-mechanical response of ceramic green substrates. The laminated low temperature co-fired ceramic green tapes were used as the testing material ; the correlations of indentation depth versus applied force and applied stress at the temperatures of 25 degrees C and 75degrees C were studied. The results showed that permanent indentation cavities could be formed at temperatures ranging from 25 degrees C to 75 degrees C, and the depth of cavities created was applied force, temperature and dwell time dependent. Creep occurred and made a larger contribution to the plastic deformation at elevated temperatures and high peak loads. There was instantaneous recovery during the unloading and retarded recovery in the first day after indentation. There was no significant pile-up due to material flow observed under compression at the temperature up to 75 degrees C. The plastic deformation was the main cause for formation of cavity on the ceramic green substrate under compression. The results can be used as a guideline for embossing ceramic green substrates.
△ Less
Submitted 7 May, 2008;
originally announced May 2008.
-
Studies of Polymer Deformation and Recovery in Hot Embossing
Authors:
X. C. Shan,
Y. C. Liu,
H. J. Lu,
Z. F. Wang,
Y. C. Lam
Abstract:
In large area micro hot embossing, the process temperature plays a critical role to both the local fidelity of microstructure formation and global uniformity. The significance of low temperature hot embossing is to improve global flatness of embossed devices. This paper reports on experimental studies of polymer deformation and relaxation in micro embossing when the process temperatures are belo…
▽ More
In large area micro hot embossing, the process temperature plays a critical role to both the local fidelity of microstructure formation and global uniformity. The significance of low temperature hot embossing is to improve global flatness of embossed devices. This paper reports on experimental studies of polymer deformation and relaxation in micro embossing when the process temperatures are below or near its glass transition temperature (Tg). In this investigation, an indentation system and a micro embosser were used to investigate the relationship of microstructure formation versus process temperature and load pressure. The depth of indentation was controlled and the load force at a certain indentation depth was measured. Experiments were carried out using 1 mm thick PMMA films with the process temperature ranging from Tg-55 degrees C to Tg +20 degrees C. The embossed structures included a single micro cavity and groups of micro cavity arrays. It was found that at temperature of Tg-55 degrees C, elastic deformation dominated the formation of microstructures and significant relaxation happened after embossing. From Tg-20 degrees C to Tg, plastic deformation dominated polymer deformation, and permanent cavities could be formed on PMMA substrates without obvious relaxation. However, the formation of protrusive structures as micro pillars was not complete since there was little polymer flow. With an increase in process temperature, microstructure could be formed under lower loading pressure. Considering the fidelity of a single microstructure and global flatness of embossed substrates, micro hot embossing at a low process temperature, but with good fidelity, should be preferred.
△ Less
Submitted 21 February, 2008;
originally announced February 2008.
