-
Finite-valued Streaming String Transducers
Authors:
Emmanuel Filiot,
Ismaël Jecker,
Gabriele Puppis,
Christof Löding,
Anca Muscholl,
Sarah Winter
Abstract:
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finite-valued transducers very attractive. For classical transducers, it is also known that fini…
▽ More
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finite-valued transducers very attractive. For classical transducers, it is also known that finite valuedness is decidable and that any k-valued finite transducer can be decomposed as a union of k single-valued finite transducers.
In this paper, we extend the above results to copyless streaming string transducers (SSTs), answering questions raised by Alur and Deshmukh in 2011. SSTs strictly extend the expressiveness of one-way transducers via additional variables that store partial outputs. We prove that any k-valued SST can be effectively decomposed as a union of k (single-valued) deterministic SSTs. As a corollary, we obtain equivalence of SSTs and two-way transducers in the finite-valued case (those two models are incomparable in general). Another corollary is an elementary upper bound for checking equivalence of finite-valued SSTs. The latter problem was already known to be decidable, but the proof complexity was unknown (it relied on Ehrenfeucht's conjecture). Finally, our main result is that finite valuedness of SSTs is decidable. The complexity is PSpace, and even PTime when the number of variables is fixed.
△ Less
Submitted 13 June, 2024; v1 submitted 13 May, 2024;
originally announced May 2024.
-
Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking
Authors:
Sarah Winter,
Martin Zimmermann
Abstract:
HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Both paradigms are based on the maxim ``counterexamples/explanations are Skolem fu…
▽ More
HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Both paradigms are based on the maxim ``counterexamples/explanations are Skolem functions for the existentially quantified trace variables''.
Our first paradigm is complete (everything can be explained), but restricted to ultimately periodic system traces. The second paradigm works with (Turing machine) computable Skolem functions and is therefore much more general, but also shown incomplete (not everything can computably be explained). Finally, we prove that it is decidable whether a given finite transition system and a formula have computable Skolem functions witnessing that the system satisfies the formula. Our algorithm also computes transducers implementing computable Skolem functions, if they exist.
△ Less
Submitted 28 April, 2024;
originally announced April 2024.
-
A Lattice-Reduction Aided Vector Perturbation Precoder Relying on Quantum Annealing
Authors:
Samuel Winter,
Yangyishi Zhang,
Gan Zheng,
Lajos Hanzo
Abstract:
Quantum annealing (QA) is proposed for vector perturbation precoding (VPP) in multiple input multiple output (MIMO) communications systems. The mathematical framework of VPP is presented, outlining the problem formulation and the benefits of lattice reduction algorithms. Lattice reduction aided quantum vector perturbation (LRAQVP) is designed by harnessing physical quantum hardware, and the optimi…
▽ More
Quantum annealing (QA) is proposed for vector perturbation precoding (VPP) in multiple input multiple output (MIMO) communications systems. The mathematical framework of VPP is presented, outlining the problem formulation and the benefits of lattice reduction algorithms. Lattice reduction aided quantum vector perturbation (LRAQVP) is designed by harnessing physical quantum hardware, and the optimization of hardware parameters is discussed. We observe a 5dB gain over lattice reduction zero forcing precoding (LRZFP), which behaves similarly to a quantum annealing algorithm operating without a lattice reduction stage. The proposed algorithm is also shown to approach the performance of a sphere encoder, which exhibits an exponentially escalating complexity.
△ Less
Submitted 12 February, 2024;
originally announced February 2024.
-
Error Propagation Analysis for Multithreaded Programs: An Empirical Approach
Authors:
Stefan Winter,
Abraham Chan,
Habib Saissi,
Karthik Pattabiraman,
Neeraj Suri
Abstract:
Fault injection is a technique to measure the robustness of a program to errors by introducing faults into the program under test. Following a fault injection experiment, Error Propagation Analysis (EPA) is deployed to understand how errors affect a program's execution. EPA typically compares the traces of a fault-free (golden) run with those from a faulty run of the program. While this suffices f…
▽ More
Fault injection is a technique to measure the robustness of a program to errors by introducing faults into the program under test. Following a fault injection experiment, Error Propagation Analysis (EPA) is deployed to understand how errors affect a program's execution. EPA typically compares the traces of a fault-free (golden) run with those from a faulty run of the program. While this suffices for deterministic programs, EPA approaches are unsound for multithreaded programs with non-deterministic golden runs. In this paper, we propose Invariant Propagation Analysis (IPA) as the use of automatically inferred likely invariants ("invariants" in the following) in lieu of golden traces for conducting EPA in multithreaded programs. We evaluate the stability and fault coverage of invariants derived by IPA through fault injection experiments across six different fault types and six representative programs that can be executed with varying numbers of threads. We find that stable invariants can be inferred in all cases, but their fault coverage depends on the application and the fault type. We also find that fault coverage for multithreaded executions with IPA can be even higher than for traditional singlethreaded EPA, which emphasizes that IPA results cannot be trivially extrapolated from traditional EPA results.
△ Less
Submitted 27 December, 2023;
originally announced December 2023.
-
The Effects of Computational Resources on Flaky Tests
Authors:
Denini Silva,
Martin Gruber,
Satyajit Gokhale,
Ellen Arteca,
Alexi Turcotte,
Marcelo d'Amorim,
Wing Lam,
Stefan Winter,
Jonathan Bell
Abstract:
Flaky tests are tests that nondeterministically pass and fail in unchanged code. These tests can be detrimental to developers' productivity. Particularly when tests run in continuous integration environments, the tests may be competing for access to limited computational resources (CPUs, memory etc.), and we hypothesize that resource (in)availability may be a significant factor in the failure rate…
▽ More
Flaky tests are tests that nondeterministically pass and fail in unchanged code. These tests can be detrimental to developers' productivity. Particularly when tests run in continuous integration environments, the tests may be competing for access to limited computational resources (CPUs, memory etc.), and we hypothesize that resource (in)availability may be a significant factor in the failure rate of flaky tests. We present the first assessment of the impact that computational resources have on flaky tests, including a total of 52 projects written in Java, JavaScript and Python, and 27 different resource configurations. Using a rigorous statistical methodology, we determine which tests are RAFT (Resource-Affected Flaky Tests). We find that 46.5% of the flaky tests in our dataset are RAFT, indicating that a substantial proportion of flaky-test failures can be avoided by adjusting the resources available when running tests. We report RAFTs and configurations to avoid them to developers, and received interest to either fix the RAFTs or to improve the specifications of the projects so that tests would be run only in configurations that are unlikely to encounter RAFT failures. Our results also have implications for researchers attempting to detect flaky tests, e.g., reducing the resources available when running tests is a cost-effective approach to detect more flaky failures.
△ Less
Submitted 18 October, 2023;
originally announced October 2023.
-
Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games
Authors:
Martin Fränzle,
Sarah Winter,
Martin Zimmermann
Abstract:
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We fu…
▽ More
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. Our main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyze existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down.
△ Less
Submitted 2 October, 2023;
originally announced October 2023.
-
Benchmarking Deep Learning Architectures for Urban Vegetation Point Cloud Semantic Segmentation from MLS
Authors:
Aditya Aditya,
Bharat Lohani,
Jagannath Aryal,
Stephan Winter
Abstract:
Vegetation is crucial for sustainable and resilient cities providing various ecosystem services and well-being of humans. However, vegetation is under critical stress with rapid urbanization and expanding infrastructure footprints. Consequently, mapping of this vegetation is essential in the urban environment. Recently, deep learning for point cloud semantic segmentation has shown significant prog…
▽ More
Vegetation is crucial for sustainable and resilient cities providing various ecosystem services and well-being of humans. However, vegetation is under critical stress with rapid urbanization and expanding infrastructure footprints. Consequently, mapping of this vegetation is essential in the urban environment. Recently, deep learning for point cloud semantic segmentation has shown significant progress. Advanced models attempt to obtain state-of-the-art performance on benchmark datasets, comprising multiple classes and representing real world scenarios. However, class specific segmentation with respect to vegetation points has not been explored. Therefore, selection of a deep learning model for vegetation points segmentation is ambiguous. To address this problem, we provide a comprehensive assessment of point-based deep learning models for semantic segmentation of vegetation class. We have selected seven representative point-based models, namely PointCNN, KPConv (omni-supervised), RandLANet, SCFNet, PointNeXt, SPoTr and PointMetaBase. These models are investigated on three different datasets, specifically Chandigarh, Toronto3D and Kerala, which are characterized by diverse nature of vegetation and varying scene complexity combined with changing per-point features and class-wise composition. PointMetaBase and KPConv (omni-supervised) achieve the highest mIoU on the Chandigarh (95.24%) and Toronto3D datasets (91.26%), respectively while PointCNN provides the highest mIoU on the Kerala dataset (85.68%). The paper develops a deeper insight, hitherto not reported, into the working of these models for vegetation segmentation and outlines the ingredients that should be included in a model specifically for vegetation segmentation. This paper is a step towards the development of a novel architecture for vegetation points segmentation.
△ Less
Submitted 1 May, 2024; v1 submitted 17 June, 2023;
originally announced June 2023.
-
On the Existence of Reactive Strategies Resilient to Delay
Authors:
Martin Fränzle,
Paul Kröger,
Sarah Winter,
Martin Zimmermann
Abstract:
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of…
▽ More
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyse existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. In this setting, some games surely won by the alter player in delay games can now be won almost surely by the protagonist in the corresponding game under delayed control, showing that it indeed makes a difference whether the protagonist has to grant lookahead or both players suffer from partial informedness. These results get even more pronounced when we finally address the quantitative goal of winning with a probability in $[0,1]$. We show that for any rational threshold $θ\in [0,1]$ there is a game that can be won by the protagonist with exactly probability $θ$ under delayed control, while being surely won by alter in the delay game setting. All these findings refine our original result that games under delayed control are not determined.
△ Less
Submitted 12 March, 2024; v1 submitted 31 May, 2023;
originally announced May 2023.
-
Machine Learning and the Future of Bayesian Computation
Authors:
Steven Winter,
Trevor Campbell,
Lizhen Lin,
Sanvesh Srivastava,
David B. Dunson
Abstract:
Bayesian models are a powerful tool for studying complex data, allowing the analyst to encode rich hierarchical dependencies and leverage prior information. Most importantly, they facilitate a complete characterization of uncertainty through the posterior distribution. Practical posterior computation is commonly performed via MCMC, which can be computationally infeasible for high dimensional model…
▽ More
Bayesian models are a powerful tool for studying complex data, allowing the analyst to encode rich hierarchical dependencies and leverage prior information. Most importantly, they facilitate a complete characterization of uncertainty through the posterior distribution. Practical posterior computation is commonly performed via MCMC, which can be computationally infeasible for high dimensional models with many observations. In this article we discuss the potential to improve posterior computation using ideas from machine learning. Concrete future directions are explored in vignettes on normalizing flows, Bayesian coresets, distributed Bayesian inference, and variational inference.
△ Less
Submitted 21 April, 2023;
originally announced April 2023.
-
Deterministic regular functions of infinite words
Authors:
Olivier Carton,
Gaëtan Douéneau-Tabot,
Emmanuel Filiot,
Sarah Winter
Abstract:
Regular functions of infinite words are (partial) functions realized by deterministic two-way transducers with infinite look-ahead. Equivalently, Alur et. al. have shown that they correspond to functions realized by deterministic Muller streaming string transducers, and to functions defined by MSO-transductions. Regular functions are however not computable in general (for a classical extension of…
▽ More
Regular functions of infinite words are (partial) functions realized by deterministic two-way transducers with infinite look-ahead. Equivalently, Alur et. al. have shown that they correspond to functions realized by deterministic Muller streaming string transducers, and to functions defined by MSO-transductions. Regular functions are however not computable in general (for a classical extension of Turing computability to infinite inputs), and we consider in this paper the class of deterministic regular functions of infinite words, realized by deterministic two-way transducers without look-ahead. We prove that it is a well-behaved class of functions: they are computable, closed under composition, characterized by the guarded fragment of MSO-transductions, by deterministic Büchi streaming string transducers, by deterministic two-way transducers with finite look-ahead, and by finite compositions of sequential functions and one fixed basic function called map-copy-reverse.
△ Less
Submitted 13 February, 2023;
originally announced February 2023.
-
A virtual reality-based method for examining audiovisual prosody perception
Authors:
Hartmut Meister,
Isa Samira Winter,
Moritz Waeachtler,
Pascale Sandmann,
Khaled Abdellatif
Abstract:
Prosody plays a vital role in verbal communication. Acoustic cues of prosody have been examined extensively. However, prosodic characteristics are not only perceived auditorily, but also visually based on head and facial movements. The purpose of this report is to present a method for examining audiovisual prosody using virtual reality. We show that animations based on a virtual human provide moti…
▽ More
Prosody plays a vital role in verbal communication. Acoustic cues of prosody have been examined extensively. However, prosodic characteristics are not only perceived auditorily, but also visually based on head and facial movements. The purpose of this report is to present a method for examining audiovisual prosody using virtual reality. We show that animations based on a virtual human provide motion cues similar to those obtained from video recordings of a real talker. The use of virtual reality opens up new avenues for examining multimodal effects of verbal communication. We discuss the method in the framework of examining prosody perception in cochlear implant listeners.
△ Less
Submitted 13 September, 2022;
originally announced September 2022.
-
A Regular and Complete Notion of Delay for Streaming String Transducers
Authors:
Emmanuel Filiot,
Ismaël Jecker,
Christof Löding,
Sarah Winter
Abstract:
The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can chec…
▽ More
The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.
△ Less
Submitted 29 April, 2024; v1 submitted 9 May, 2022;
originally announced May 2022.
-
Translating Place-Related Questions to GeoSPARQL Queries
Authors:
Ehsan Hamzei,
Martin Tomko,
Stephan Winter
Abstract:
Many place-related questions can only be answered by complex spatial reasoning, a task poorly supported by factoid question retrieval. Such reasoning using combinations of spatial and non-spatial criteria pertinent to place-related questions is increasingly possible on linked data knowledge bases. Yet, to enable question answering based on linked knowledge bases, natural language questions must fi…
▽ More
Many place-related questions can only be answered by complex spatial reasoning, a task poorly supported by factoid question retrieval. Such reasoning using combinations of spatial and non-spatial criteria pertinent to place-related questions is increasingly possible on linked data knowledge bases. Yet, to enable question answering based on linked knowledge bases, natural language questions must first be re-formulated as formal queries. Here, we first present an enhanced version of YAGO2geo, the geospatially-enabled variant of the YAGO2 knowledge base, by linking and adding more than one million places from OpenStreetMap data to YAGO2. We then propose a novel approach to translate the place-related questions into logical representations, theoretically grounded in the core concepts of spatial information. Next, we use a dynamic template-based approach to generate fully executable GeoSPARQL queries from the logical representations. We test our approach using the Geospatial Gold Standard dataset and report substantial improvements over existing methods.
△ Less
Submitted 6 May, 2022;
originally announced May 2022.
-
Weak Muller Conditions Make Delay Games Hard
Authors:
Sarah Winter,
Martin Zimmermann
Abstract:
We show that solving delay games with winning conditions given by deterministic and nondeterministic weak Muller automata is 2EXPTIME-complete respectively 3EXPTIME-complete. Furthermore, doubly and triply exponential lookahead is necessary and sufficient to win such games. These results are the first that show that the succinctness of the automata types used to specify the winning conditions has…
▽ More
We show that solving delay games with winning conditions given by deterministic and nondeterministic weak Muller automata is 2EXPTIME-complete respectively 3EXPTIME-complete. Furthermore, doubly and triply exponential lookahead is necessary and sufficient to win such games. These results are the first that show that the succinctness of the automata types used to specify the winning conditions has an influence on the complexity of these problems.
△ Less
Submitted 19 October, 2022; v1 submitted 7 March, 2022;
originally announced March 2022.
-
Decision problems for origin-close top-down tree transducers (full version)
Authors:
Sarah Winter
Abstract:
Tree transductions are binary relations of finite trees. For tree transductions defined by non-deterministic top-down tree transducers, inclusion, equivalence and synthesis problems are known to be undecidable. Adding origin semantics to tree transductions, i.e., tagging each output node with the input node it originates from, is a known way to recover decidability for inclusion and equivalence. T…
▽ More
Tree transductions are binary relations of finite trees. For tree transductions defined by non-deterministic top-down tree transducers, inclusion, equivalence and synthesis problems are known to be undecidable. Adding origin semantics to tree transductions, i.e., tagging each output node with the input node it originates from, is a known way to recover decidability for inclusion and equivalence. The origin semantics is rather rigid, in this work, we introduce a similarity measure for transducers with origin semantics and show that we can decide inclusion, equivalence and synthesis problems for origin-close non-deterministic top-down tree transducers.
△ Less
Submitted 6 July, 2021;
originally announced July 2021.
-
Resynchronized Uniformization and Definability Problems for Rational Relations
Authors:
Christof Löding,
Sarah Winter
Abstract:
Regular synchronization languages can be used to define rational relations of finite words, and to characterize subclasses of rational relations, like automatic or recognizable relations. We provide a systematic study of the decidability of uniformization and definability problems for subclasses of rational relations defined in terms of such synchronization languages. We rephrase known results in…
▽ More
Regular synchronization languages can be used to define rational relations of finite words, and to characterize subclasses of rational relations, like automatic or recognizable relations. We provide a systematic study of the decidability of uniformization and definability problems for subclasses of rational relations defined in terms of such synchronization languages. We rephrase known results in this setting and complete the picture by adding several new decidability and undecidability results.
△ Less
Submitted 29 August, 2023; v1 submitted 26 April, 2021;
originally announced April 2021.
-
Does Your Dermatology Classifier Know What It Doesn't Know? Detecting the Long-Tail of Unseen Conditions
Authors:
Abhijit Guha Roy,
Jie Ren,
Shekoofeh Azizi,
Aaron Loh,
Vivek Natarajan,
Basil Mustafa,
Nick Pawlowski,
Jan Freyberg,
Yuan Liu,
Zach Beaver,
Nam Vo,
Peggy Bui,
Samantha Winter,
Patricia MacWilliams,
Greg S. Corrado,
Umesh Telang,
Yun Liu,
Taylan Cemgil,
Alan Karthikesalingam,
Balaji Lakshminarayanan,
Jim Winkens
Abstract:
We develop and rigorously evaluate a deep learning based system that can accurately classify skin conditions while detecting rare conditions for which there is not enough data available for training a confident classifier. We frame this task as an out-of-distribution (OOD) detection problem. Our novel approach, hierarchical outlier detection (HOD) assigns multiple abstention classes for each train…
▽ More
We develop and rigorously evaluate a deep learning based system that can accurately classify skin conditions while detecting rare conditions for which there is not enough data available for training a confident classifier. We frame this task as an out-of-distribution (OOD) detection problem. Our novel approach, hierarchical outlier detection (HOD) assigns multiple abstention classes for each training outlier class and jointly performs a coarse classification of inliers vs. outliers, along with fine-grained classification of the individual classes. We demonstrate the effectiveness of the HOD loss in conjunction with modern representation learning approaches (BiT, SimCLR, MICLe) and explore different ensembling strategies for further improving the results. We perform an extensive subgroup analysis over conditions of varying risk levels and different skin types to investigate how the OOD detection performance changes over each subgroup and demonstrate the gains of our framework in comparison to baselines. Finally, we introduce a cost metric to approximate downstream clinical impact. We use this cost metric to compare the proposed method against a baseline system, thereby making a stronger case for the overall system effectiveness in a real-world deployment scenario.
△ Less
Submitted 8 April, 2021;
originally announced April 2021.
-
Synthesizing Computable Functions from Rational Specifications over Infinite Words
Authors:
Emmanuel Filiot,
Sarah Winter
Abstract:
The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined non-determini…
▽ More
The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined non-deterministic parity transducers. We prove that the synthesis problem of computable functions from rational specifications is undecidable. We provide an incomplete but sound reduction to some parity game, such that if Eve wins the game, then the rational specification is realizable by a computable function. We prove that this function is even computable by a deterministic two-way transducer. We provide a sufficient condition under which the latter game reduction is complete. This entails the decidability of the synthesis problem of computable functions, which we prove to be ExpTime-complete, for a large subclass of rational specifications, namely deterministic rational specifications. This subclass contains the class of automatic relations over infinite words, a yardstick in reactive synthesis.
△ Less
Submitted 8 February, 2024; v1 submitted 9 March, 2021;
originally announced March 2021.
-
Synthesis from Weighted Specifications with Partial Domains over Finite Words
Authors:
Emmanuel Filiot,
Christof Löding,
Sarah Winter
Abstract:
In this paper, we investigate the synthesis problem of terminating reactive systems from quantitative specifications. Such systems are modeled as finite transducers whose executions are represented as finite words in $(I\times O)^*$, where $I,O$ are finite sets of input and output symbols, respectively. A weighted specification $S$ assigns a rational value (or $-\infty$) to words in…
▽ More
In this paper, we investigate the synthesis problem of terminating reactive systems from quantitative specifications. Such systems are modeled as finite transducers whose executions are represented as finite words in $(I\times O)^*$, where $I,O$ are finite sets of input and output symbols, respectively. A weighted specification $S$ assigns a rational value (or $-\infty$) to words in $(I\times O)^*$, and we consider three kinds of objectives for synthesis, namely threshold objectives where the system's executions are required to be above some given threshold, best-value and approximate objectives where the system is required to perform as best as it can by providing output symbols that yield the best value and $\varepsilon$-best value respectively w.r.t. $S$. We establish a landscape of decidability results for these three objectives and weighted specifications with partial domain over finite words given by deterministic weighted automata equipped with sum, discounted-sum and average measures. The resulting objectives are not regular in general and we develop an infinite game framework to solve the corresponding synthesis problems, namely the class of (weighted) critical prefix games.
△ Less
Submitted 9 March, 2021;
originally announced March 2021.
-
Templates of generic geographic information for answering where-questions
Authors:
Ehsan Hamzei,
Stephan Winter,
Martin Tomko
Abstract:
In everyday communication, where-questions are answered by place descriptions. To answer where-questions automatically, computers should be able to generate relevant place descriptions that satisfy inquirers' information needs. Human-generated answers to where-questions constructed based on a few anchor places that characterize the location of inquired places. The challenge for automatically gener…
▽ More
In everyday communication, where-questions are answered by place descriptions. To answer where-questions automatically, computers should be able to generate relevant place descriptions that satisfy inquirers' information needs. Human-generated answers to where-questions constructed based on a few anchor places that characterize the location of inquired places. The challenge for automatically generating such relevant responses stems from selecting relevant anchor places. In this paper, we present templates that allow to characterize the human-generated answers and to imitate their structure. These templates are patterns of generic geographic information derived and encoded from the largest available machine comprehension dataset, MS MARCO v2.1. In our approach, the toponyms in the questions and answers of the dataset are encoded into sequences of generic information. Next, sequence prediction methods are used to model the relation between the generic information in the questions and their answers. Finally, we evaluate the performance of predicting templates for answers to where-questions.
△ Less
Submitted 20 January, 2021;
originally announced January 2021.
-
Characterizing digital microstructures by the Minkowski-based quadratic normal tensor
Authors:
Felix Ernesti,
Matti Schneider,
Steffen Winter,
Daniel Hug,
Günter Last,
Thomas Böhlke
Abstract:
For material modeling of microstructured media, an accurate characterization of the underlying microstructure is indispensable. Mathematically speaking, the overall goal of microstructure characterization is to find simple functionals which describe the geometric shape as well as the composition of the microstructures under consideration, and enable distinguishing microstructures with distinct eff…
▽ More
For material modeling of microstructured media, an accurate characterization of the underlying microstructure is indispensable. Mathematically speaking, the overall goal of microstructure characterization is to find simple functionals which describe the geometric shape as well as the composition of the microstructures under consideration, and enable distinguishing microstructures with distinct effective material behavior. For this purpose, we propose using Minkowski tensors, in general, and the quadratic normal tensor, in particular, and introduce a computational algorithm applicable to voxel-based microstructure representations. Rooted in the mathematical field of integral geometry, Minkowski tensors associate a tensor to rather general geometric shapes, which make them suitable for a wide range of microstructured material classes. Furthermore, they satisfy additivity and continuity properties, which makes them suitable and robust for large-scale applications. We present a modular algorithm for computing the quadratic normal tensor of digital microstructures. We demonstrate multigrid convergence for selected numerical examples and apply our approach to a variety of microstructures. Strikingly, the presented algorithm remains unaffected by inaccurate computation of the interface area. The quadratic normal tensor may be used for engineering purposes, such as mean-field homogenization or as target value for generating synthetic microstructures.
△ Less
Submitted 30 July, 2020;
originally announced July 2020.
-
Disambiguating fine-grained place names from descriptions by clustering
Authors:
Hao Chen,
Maria Vasardani,
Stephan Winter
Abstract:
Everyday place descriptions often contain place names of fine-grained features, such as buildings or businesses, that are more difficult to disambiguate than names referring to larger places, for example cities or natural geographic features. Fine-grained places are often significantly more frequent and more similar to each other, and disambiguation heuristics developed for larger places, such as…
▽ More
Everyday place descriptions often contain place names of fine-grained features, such as buildings or businesses, that are more difficult to disambiguate than names referring to larger places, for example cities or natural geographic features. Fine-grained places are often significantly more frequent and more similar to each other, and disambiguation heuristics developed for larger places, such as those based on population or containment relationships, are often not applicable in these cases. In this research, we address the disambiguation of fine-grained place names from everyday place descriptions. For this purpose, we evaluate the performance of different existing clustering-based approaches, since clustering approaches require no more knowledge other than the locations of ambiguous place names. We consider not only approaches developed specifically for place name disambiguation, but also clustering algorithms developed for general data mining that could potentially be leveraged. We compare these methods with a novel algorithm, and show that the novel algorithm outperforms the other algorithms in terms of disambiguation precision and distance error over several tested datasets.
△ Less
Submitted 17 August, 2018;
originally announced August 2018.
-
Uniformization Problems for Synchronizations of Automatic Relations on Words
Authors:
Sarah Winter
Abstract:
A uniformization of a binary relation is a function that is contained in the relation and has the same domain as the relation. The synthesis problem asks for effective uniformization for classes of relations and functions that can be implemented in a specific way.
We consider the synthesis problem for automatic relations over finite words (also called regular or synchronized rational relations)…
▽ More
A uniformization of a binary relation is a function that is contained in the relation and has the same domain as the relation. The synthesis problem asks for effective uniformization for classes of relations and functions that can be implemented in a specific way.
We consider the synthesis problem for automatic relations over finite words (also called regular or synchronized rational relations) by functions implemented by specific classes of sequential transducers.
It is known that the problem "Given an automatic relation, does it have a uniformization by a subsequential transducer?" is decidable in the two variants where the uniformization can either be implemented by an arbitrary subsequential transducer or it has to be implemented by a synchronous transducer. We introduce a new variant of this problem in which the allowed input/output behavior of the subsequential transducer is specified by a set of synchronizations and prove decidability for a specific class of synchronizations.
△ Less
Submitted 7 May, 2018;
originally announced May 2018.
-
Geo-referencing Place from Everyday Natural Language Descriptions
Authors:
Hao Chen,
Maria Vasardani,
Stephan Winter
Abstract:
Natural language place descriptions in everyday communication provide a rich source of spatial knowledge about places. An important step to utilize such knowledge in information systems is geo-referencing all the places referred to in these descriptions. Current techniques for geo-referencing places from text documents are using place name recognition and disambiguation; however, place description…
▽ More
Natural language place descriptions in everyday communication provide a rich source of spatial knowledge about places. An important step to utilize such knowledge in information systems is geo-referencing all the places referred to in these descriptions. Current techniques for geo-referencing places from text documents are using place name recognition and disambiguation; however, place descriptions often contain place references that are not known by gazetteers, or that are expressed in other, more flexible ways. Hence, the approach for geo-referencing presented in this paper starts from a place graph that contains the place references as well as spatial relationships extracted from place descriptions. Spatial relationships are used to constrain the locations of places and allow the later best-matching process for geo-referencing. The novel geo-referencing process results in higher precision and recall compared to state-of-art toponym resolution approaches on several tested place description datasets.
△ Less
Submitted 9 October, 2017;
originally announced October 2017.
-
Finite-state Strategies in Delay Games (full version)
Authors:
Sarah Winter,
Martin Zimmermann
Abstract:
What is a finite-state strategy in a delay game? We answer this surprisingly non-trivial question by presenting a very general framework that allows to remove delay: finite-state strategies exist for all winning conditions where the resulting delay-free game admits a finite-state strategy. The framework is applicable to games whose winning condition is recognized by an automaton with an acceptance…
▽ More
What is a finite-state strategy in a delay game? We answer this surprisingly non-trivial question by presenting a very general framework that allows to remove delay: finite-state strategies exist for all winning conditions where the resulting delay-free game admits a finite-state strategy. The framework is applicable to games whose winning condition is recognized by an automaton with an acceptance condition that satisfies a certain aggregation property. Our framework also yields upper bounds on the complexity of determining the winner of such delay games and upper bounds on the necessary lookahead to win the game. In particular, we cover all previous results of that kind as special cases of our uniform approach.
△ Less
Submitted 13 December, 2019; v1 submitted 28 April, 2017;
originally announced April 2017.
-
A Comprehensive Model of Usability
Authors:
Sebastian Winter,
Stefan Wagner,
Florian Deissenboeck
Abstract:
Usability is a key quality attribute of successful software systems. Unfortunately, there is no common understanding of the factors influencing usability and their interrelations. Hence, the lack of a comprehensive basis for designing, analyzing, and improving user interfaces. This paper proposes a 2-dimensional model of usability that associates system properties with the activities carried out b…
▽ More
Usability is a key quality attribute of successful software systems. Unfortunately, there is no common understanding of the factors influencing usability and their interrelations. Hence, the lack of a comprehensive basis for designing, analyzing, and improving user interfaces. This paper proposes a 2-dimensional model of usability that associates system properties with the activities carried out by the user. By separating activities and properties, sound quality criteria can be identified, thus facilitating statements concerning their interdependencies. This model is based on a tested quality meta-model that fosters preciseness and completeness. A case study demonstrates the manner by which such a model aids in revealing contradictions and omissions in existing usability standards. Furthermore, the model serves as a central and structured knowledge base for the entire quality assurance process, e.g. the automatic generation of guideline documents.
△ Less
Submitted 14 December, 2016;
originally announced December 2016.
-
Managing Quality Requirements Using Activity-Based Quality Models
Authors:
Stefan Wagner,
Florian Deissenboeck,
Sebastian Winter
Abstract:
Managing requirements on quality aspects is an important issue in the development of software systems. Difficulties arise from expressing them appropriately what in turn results from the difficulty of the concept of quality itself. Building and using quality models is an approach to handle the complexity of software quality. A novel kind of quality models uses the activities performed on and with…
▽ More
Managing requirements on quality aspects is an important issue in the development of software systems. Difficulties arise from expressing them appropriately what in turn results from the difficulty of the concept of quality itself. Building and using quality models is an approach to handle the complexity of software quality. A novel kind of quality models uses the activities performed on and with the software as an explicit dimension. These quality models are a well-suited basis for managing quality requirements from elicitation over refinement to assurance. The paper proposes such an approach and shows its applicability in an automotive case study.
△ Less
Submitted 4 November, 2016;
originally announced November 2016.
-
On Equivalence and Uniformisation Problems for Finite Transducers
Authors:
Emmanuel Filiot,
Ismaël Jecker,
Christof Löding,
Sarah Winter
Abstract:
Transductions are binary relations of finite words. For rational transductions, i.e., transductions defined by finite transducers, the inclusion, equivalence and sequential uniformisation problems are known to be undecidable. In this paper, we investigate stronger variants of inclusion, equivalence and sequential uniformisation, based on a general notion of transducer resynchronisation, and show t…
▽ More
Transductions are binary relations of finite words. For rational transductions, i.e., transductions defined by finite transducers, the inclusion, equivalence and sequential uniformisation problems are known to be undecidable. In this paper, we investigate stronger variants of inclusion, equivalence and sequential uniformisation, based on a general notion of transducer resynchronisation, and show their decidability. We also investigate the classes of finite-valued rational transductions and deterministic rational transductions, which are known to have a decidable equivalence problem. We show that sequential uniformisation is also decidable for them.
△ Less
Submitted 27 February, 2016;
originally announced February 2016.
-
Geospatial Big Data Handling Theory and Methods: A Review and Research Challenges
Authors:
S. Li,
S. Dragicevic,
F. Anton,
M. Sester,
S. Winter,
A. Coltekin,
C. Pettit,
B. Jiang,
J. Haworth,
A. Stein,
T. Cheng
Abstract:
Big data has now become a strong focus of global interest that is increasingly attracting the attention of academia, industry, government and other organizations. Big data can be situated in the disciplinary area of traditional geospatial data handling theory and methods. The increasing volume and varying format of collected geospatial big data presents challenges in storing, managing, processing,…
▽ More
Big data has now become a strong focus of global interest that is increasingly attracting the attention of academia, industry, government and other organizations. Big data can be situated in the disciplinary area of traditional geospatial data handling theory and methods. The increasing volume and varying format of collected geospatial big data presents challenges in storing, managing, processing, analyzing, visualizing and verifying the quality of data. This has implications for the quality of decisions made with big data. Consequently, this position paper of the International Society for Photogrammetry and Remote Sensing (ISPRS) Technical Commission II (TC II) revisits the existing geospatial data handling methods and theories to determine if they are still capable of handling emerging geospatial big data. Further, the paper synthesises problems, major issues and challenges with current developments as well as recommending what needs to be developed further in the near future.
Keywords: Big data, Geospatial, Data handling, Analytics, Spatial Modeling, Review
△ Less
Submitted 10 November, 2015;
originally announced November 2015.
-
Synthesis of Deterministic Top-down Tree Transducers from Automatic Tree Relations
Authors:
Christof Löding,
Sarah Winter
Abstract:
We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of specifications that are deterministic top-down tree automatic, meaning the specification is recognizable by a deterministic top-down tree automaton that reads the two given trees synchronously in parallel. In this setting we stud…
▽ More
We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of specifications that are deterministic top-down tree automatic, meaning the specification is recognizable by a deterministic top-down tree automaton that reads the two given trees synchronously in parallel. In this setting we study tree transducers that are allowed to have either bounded delay or arbitrary delay. Delay is caused whenever the transducer reads a symbol from the input tree but does not produce output. We provide decision procedures for both bounded and arbitrary delay that yield deterministic top-down tree transducers which realize the specification for valid input trees. Similar to the case of relations over words, we use two-player games to obtain our results.
△ Less
Submitted 25 August, 2014;
originally announced August 2014.
-
Trees over Infinite Structures and Path Logics with Synchronization
Authors:
Alex Spelten,
Wolfgang Thomas,
Sarah Winter
Abstract:
We provide decidability and undecidability results on the model-checking problem for infinite tree structures. These tree structures are built from sequences of elements of infinite relational structures. More precisely, we deal with the tree iteration of a relational structure M in the sense of Shelah-Stupp. In contrast to classical results where model-checking is shown decidable for MSO-logic, w…
▽ More
We provide decidability and undecidability results on the model-checking problem for infinite tree structures. These tree structures are built from sequences of elements of infinite relational structures. More precisely, we deal with the tree iteration of a relational structure M in the sense of Shelah-Stupp. In contrast to classical results where model-checking is shown decidable for MSO-logic, we show decidability of the tree model-checking problem for logics that allow only path quantifiers and chain quantifiers (where chains are subsets of paths), as they appear in branching time logics; however, at the same time the tree is enriched by the equal-level relation (which holds between vertices u, v if they are on the same tree level). We separate cleanly the tree logic from the logic used for expressing properties of the underlying structure M. We illustrate the scope of the decidability results by showing that two slight extensions of the framework lead to undecidability. In particular, this applies to the (stronger) tree iteration in the sense of Muchnik-Walukiewicz.
△ Less
Submitted 14 November, 2011;
originally announced November 2011.
