Showing 1–25 of 25 results for author: Winter, K

Glassy dynamics in deep neural networks: A structural comparison

Authors: Max Kerr Winter, Liesbeth M. C. Janssen

Abstract: Deep Neural Networks (DNNs) share important similarities with structural glasses. Both have many degrees of freedom, and their dynamics are governed by a high-dimensional, non-convex landscape representing either the loss or energy, respectively. Furthermore, both experience gradient descent dynamics subject to noise. In this work we investigate, by performing quantitative measurements on realisti… ▽ More Deep Neural Networks (DNNs) share important similarities with structural glasses. Both have many degrees of freedom, and their dynamics are governed by a high-dimensional, non-convex landscape representing either the loss or energy, respectively. Furthermore, both experience gradient descent dynamics subject to noise. In this work we investigate, by performing quantitative measurements on realistic networks trained on the MNIST and CIFAR-10 datasets, the extent to which this qualitative similarity gives rise to glass-like dynamics in neural networks. We demonstrate the existence of a Topology Trivialisation Transition as well as the previously studied under-to-overparameterised transition analogous to jamming. By training DNNs with overdamped Langevin dynamics in the resulting disordered phases, we do not observe diverging relaxation times at non-zero temperature, nor do we observe any caging effects, in contrast to glass phenomenology. However, the weight overlap function follows a power law in time, with an exponent of approximately -0.5, in agreement with the Mode-Coupling Theory of structural glasses. In addition, the DNN dynamics obey a form of time-temperature superposition. Finally, dynamic heterogeneity and ageing are observed at low temperatures. These results highlight important and surprising points of both difference and agreement between the behaviour of DNNs and structural glasses. △ Less

Submitted 24 May, 2024; v1 submitted 21 May, 2024; originally announced May 2024.

Link groups of Kishino knot stacks

Authors: Blake K Winter

Abstract: For any virtual link, a class of new links can be defined called stacks, in which copies of the virtual link are placed on top of one another. The resulting virtual link depends only on the virtual isotopy class of the original link, and the fundamental group of such a link may be used to detect whether the link is nontrivial and whether it is nonclassical in some cases. We show that this group is… ▽ More For any virtual link, a class of new links can be defined called stacks, in which copies of the virtual link are placed on top of one another. The resulting virtual link depends only on the virtual isotopy class of the original link, and the fundamental group of such a link may be used to detect whether the link is nontrivial and whether it is nonclassical in some cases. We show that this group is able to distinguish three Kishino knots from the unknot using a stacked pair. However, for a fourth Kishino knot, the group and quandle of any stack invariant will be free with a number of generators equal to the number of copies in the stac. △ Less

Submitted 8 May, 2024; originally announced May 2024.

MSC Class: 57K12

MEDIATE: Mutually Endorsed Distributed Incentive Acknowledgment Token Exchange

Authors: Philipp Altmann, Katharina Winter, Michael Kölle, Maximilian Zorn, Thomy Phan, Claudia Linnhoff-Popien

Abstract: Recent advances in multi-agent systems (MAS) have shown that incorporating peer incentivization (PI) mechanisms vastly improves cooperation. Especially in social dilemmas, communication between the agents helps to overcome sub-optimal Nash equilibria. However, incentivization tokens need to be carefully selected. Furthermore, real-world applications might yield increased privacy requirements and l… ▽ More Recent advances in multi-agent systems (MAS) have shown that incorporating peer incentivization (PI) mechanisms vastly improves cooperation. Especially in social dilemmas, communication between the agents helps to overcome sub-optimal Nash equilibria. However, incentivization tokens need to be carefully selected. Furthermore, real-world applications might yield increased privacy requirements and limited exchange. Therefore, we extend the PI protocol for mutual acknowledgment token exchange (MATE) and provide additional analysis on the impact of the chosen tokens. Building upon those insights, we propose mutually endorsed distributed incentive acknowledgment token exchange (MEDIATE), an extended PI architecture employing automatic token derivation via decentralized consensus. Empirical results show the stable agreement on appropriate tokens yielding superior performance compared to static tokens and state-of-the-art approaches in different social dilemma environments with various reward distributions. △ Less

Submitted 4 April, 2024; originally announced April 2024.

Comments: 12 pages, 5 figures

Bias correction of wind power forecasts with SCADA data and continuous learning

Authors: Stefan Jonas, Kevin Winter, Bernhard Brodbeck, Angela Meyer

Abstract: Wind energy plays a critical role in the transition towards renewable energy sources. However, the uncertainty and variability of wind can impede its full potential and the necessary growth of wind power capacity. To mitigate these challenges, wind power forecasting methods are employed for applications in power management, energy trading, or maintenance scheduling. In this work, we present, evalu… ▽ More Wind energy plays a critical role in the transition towards renewable energy sources. However, the uncertainty and variability of wind can impede its full potential and the necessary growth of wind power capacity. To mitigate these challenges, wind power forecasting methods are employed for applications in power management, energy trading, or maintenance scheduling. In this work, we present, evaluate, and compare four machine learning-based wind power forecasting models. Our models correct and improve 48-hour forecasts extracted from a numerical weather prediction (NWP) model. The models are evaluated on datasets from a wind park comprising 65 wind turbines. The best improvement in forecasting error and mean bias was achieved by a convolutional neural network, reducing the average NRMSE down to 22%, coupled with a significant reduction in mean bias, compared to a NRMSE of 35% from the strongly biased baseline model using uncorrected NWP forecasts. Our findings further indicate that changes to neural network architectures play a minor role in affecting the forecasting performance, and that future research should rather investigate changes in the model pipeline. Moreover, we introduce a continuous learning strategy, which is shown to achieve the highest forecasting performance improvements when new data is made available. △ Less

Submitted 21 February, 2024; originally announced February 2024.

Comments: 20 pages

Bridging MDE and AI: A Systematic Review of Domain-Specific Languages and Model-Driven Practices in AI Software Systems Engineering

Authors: Simon Raedler, Luca Berardinelli, Karolin Winter, Abbas Rahimi, Stefanie Rinderle-Ma

Abstract: Background:Technical systems are growing in complexity with more components and functions across various disciplines. Model-Driven Engineering (MDE) helps manage this complexity by using models as key artifacts. Domain-Specific Languages (DSL) supported by MDE facilitate modeling. As data generation in product development increases, there's a growing demand for AI algorithms, which can be challeng… ▽ More Background:Technical systems are growing in complexity with more components and functions across various disciplines. Model-Driven Engineering (MDE) helps manage this complexity by using models as key artifacts. Domain-Specific Languages (DSL) supported by MDE facilitate modeling. As data generation in product development increases, there's a growing demand for AI algorithms, which can be challenging to implement. Integrating AI algorithms with DSL and MDE can streamline this process. Objective:This study aims to investigate the existing model-driven approaches relying on DSL in support of the engineering of AI software systems to sharpen future research further and define the current state of the art. Method:We conducted a Systemic Literature Review (SLR), collecting papers from five major databases resulting in 1335 candidate studies, eventually retaining 18 primary studies. Each primary study will be evaluated and discussed with respect to the adoption of MDE principles and practices and the phases of AI development support aligned with the stages of the CRISP-DM methodology. Results:The study's findings show that language workbenches are of paramount importance in dealing with all aspects of modeling language development and are leveraged to define DSL explicitly addressing AI concerns. The most prominent AI-related concerns are training and modeling of the AI algorithm, while minor emphasis is given to the time-consuming preparation of the data. Early project phases that support interdisciplinary communication of requirements, e.g., CRISP-DM Business Understanding phase, are rarely reflected. Conclusion:The study found that the use of MDE for AI is still in its early stages, and there is no single tool or method that is widely used. Additionally, current approaches tend to focus on specific stages of development rather than providing support for the entire development process. △ Less

Submitted 6 May, 2024; v1 submitted 10 July, 2023; originally announced July 2023.

Comments: 57 pages, 2 figures, 8 tables

ACM Class: A.1; H.1.0; I.2.4

A deep learning approach to the measurement of long-lived memory kernels from Generalised Langevin Dynamics

Authors: Max Kerr Winter, Ilian Pihlajamaa, Vincent E. Debets, Liesbeth M. C. Janssen

Abstract: Memory effects are ubiquitous in a wide variety of complex physical phenomena, ranging from glassy dynamics and metamaterials to climate models. The Generalised Langevin Equation (GLE) provides a rigorous way to describe memory effects via the so-called memory kernel in an integro-differential equation. However, the memory kernel is often unknown, and accurately predicting or measuring it via e.g.… ▽ More Memory effects are ubiquitous in a wide variety of complex physical phenomena, ranging from glassy dynamics and metamaterials to climate models. The Generalised Langevin Equation (GLE) provides a rigorous way to describe memory effects via the so-called memory kernel in an integro-differential equation. However, the memory kernel is often unknown, and accurately predicting or measuring it via e.g. a numerical inverse Laplace transform remains a herculean task. Here we describe a novel method using deep neural networks (DNNs) to measure memory kernels from dynamical data. As proof-of-principle, we focus on the notoriously long-lived memory effects of glassy systems, which have proved a major challenge to existing methods. Specifically, we learn a training set generated with the Mode-Coupling Theory (MCT) of hard spheres. Our DNNs are remarkably robust against noise, in contrast to conventional techniques which require ensemble averaging over many independent trajectories. Finally, we demonstrate that a network trained on data generated from analytic theory (hard-sphere MCT) generalises well to data from simulations of a different system (Brownian Weeks-Chandler-Andersen particles). We provide a general pipeline, KernelLearner, for training networks to extract memory kernels from any non-Markovian system described by a GLE. The success of our DNN method applied to glassy systems suggests deep learning can play an important role in the study of dynamical systems that exhibit memory effects. △ Less

Submitted 28 June, 2023; v1 submitted 27 February, 2023; originally announced February 2023.

Journal ref: J. Chem. Phys. 158, 244115 (2023)

Predictive Compliance Monitoring in Process-Aware Information Systems: State of the Art, Functionalities, Research Directions

Authors: Stefanie Rinderle-Ma, Karolin Winter, Janik-Vasily Benzin

Abstract: Business process compliance is a key area of business process management and aims at ensuring that processes obey to compliance constraints such as regulatory constraints or business rules imposed on them. Process compliance can be checked during process design time based on verification of process models and at runtime based on monitoring the compliance states of running process instances. For ex… ▽ More Business process compliance is a key area of business process management and aims at ensuring that processes obey to compliance constraints such as regulatory constraints or business rules imposed on them. Process compliance can be checked during process design time based on verification of process models and at runtime based on monitoring the compliance states of running process instances. For existing compliance monitoring approaches it remains unclear whether and how compliance violations can be predicted, although predictions are crucial in order to prepare and take countermeasures in time. This work, hence, analyzes existing literature from compliance monitoring as well as predictive process monitoring and provides an updated framework of compliance monitoring functionalities. Moreover, it raises the vision of a comprehensive predictive compliance monitoring system that integrates existing predicate prediction approaches with the idea of employing PPM with different prediction goals such as next activity or remaining time for prediction and subsequent map** of the prediction results onto the given set of compliance constraints (PCM). For each compliance monitoring functionality we elicit PCM system requirements and assess their coverage by existing approaches. Based on the assessment, open challenges and research directions realizing a comprehensive PCM system are elaborated. △ Less

Submitted 2 March, 2023; v1 submitted 10 May, 2022; originally announced May 2022.

Tissue hydraulics: physics of lumen formation and interaction

Authors: Alejandro Torres-Sánchez, Max Kerr Winter, Guillaume Salbreux

Abstract: Lumen formation plays an essential role in the morphogenesis of tissues during development. Here we review the physical principles that play a role in the growth and coarsening of lumens. Solute pum** by the cell, hydraulic flows driven by differences of osmotic and hydrostatic pressures, balance of forces between extracellular fluids and cell-generated cytoskeletal forces, and electro-osmotic e… ▽ More Lumen formation plays an essential role in the morphogenesis of tissues during development. Here we review the physical principles that play a role in the growth and coarsening of lumens. Solute pum** by the cell, hydraulic flows driven by differences of osmotic and hydrostatic pressures, balance of forces between extracellular fluids and cell-generated cytoskeletal forces, and electro-osmotic effects have been implicated in determining the dynamics and steady-state of lumens. We use the framework of linear irreversible thermodynamics to discuss the relevant force, time and length scales involved in these processes. We focus on order of magnitude estimates of physical parameters controlling lumen formation and coarsening. △ Less

Submitted 12 July, 2021; v1 submitted 12 April, 2021; originally announced April 2021.

Comments: 15 pages, 3 figures

Some generalizations of Satoh's Tube map

Authors: Blake K Winter

Abstract: Satoh has defined a map from virtual knots to ribbon surfaces embedded in $S^4$. Herein, we generalize this map to virtual $m$-links, and use this to construct generalizations of welded and extended welded knots to higher dimensions. This also allows us to construct two new geometric pictures of virtual $m$-links, including 1-links. Satoh has defined a map from virtual knots to ribbon surfaces embedded in $S^4$. Herein, we generalize this map to virtual $m$-links, and use this to construct generalizations of welded and extended welded knots to higher dimensions. This also allows us to construct two new geometric pictures of virtual $m$-links, including 1-links. △ Less

Submitted 15 March, 2021; originally announced March 2021.

Comments: 13 page, 6 figures

MSC Class: 57M25; 57M27; 57Q45

Detecting Production Phases Based on Sensor Values using 1D-CNNs

Authors: Burkhard Hoppenstedt, Manfred Reichert, Ghada El-Khawaga, Klaus Kammerer, Karl-Michael Winter, Rüdiger Pryss

Abstract: In the context of Industry 4.0, the knowledge extraction from sensor information plays an important role. Often, information gathered from sensor values reveals meaningful insights for production levels, such as anomalies or machine states. In our use case, we identify production phases through the inspection of sensor values with the help of convolutional neural networks. The data set stems from… ▽ More In the context of Industry 4.0, the knowledge extraction from sensor information plays an important role. Often, information gathered from sensor values reveals meaningful insights for production levels, such as anomalies or machine states. In our use case, we identify production phases through the inspection of sensor values with the help of convolutional neural networks. The data set stems from a tempering furnace used for metal heat treating. Our supervised learning approach unveils a promising accuracy for the chosen neural network that was used for the detection of production phases. We consider solutions like shown in this work as salient pillars in the field of predictive maintenance. △ Less

Submitted 23 April, 2020; originally announced April 2020.

Comments: 2 Pages

An abstract semantics of speculative execution for reasoning about security vulnerabilities

Authors: Robert J. Colvin, Kirsten Winter

Abstract: Reasoning about correctness and security of software is increasingly difficult due to the complexity of modern microarchitectural features such as out-of-order execution. A class of security vulnerabilities termed Spectre that exploits side effects of speculative, out-of-order execution was announced in 2018 and has since drawn much attention. In this paper we formalise speculative execution and i… ▽ More Reasoning about correctness and security of software is increasingly difficult due to the complexity of modern microarchitectural features such as out-of-order execution. A class of security vulnerabilities termed Spectre that exploits side effects of speculative, out-of-order execution was announced in 2018 and has since drawn much attention. In this paper we formalise speculative execution and its side effects with the intention of allowing speculation to be reasoned about abstractly at the program level, limiting the exposure to processor-specific or low-level semantics. To this end we encode and expose speculative execution explicitly in the programming language, rather than solely in the operational semantics; as a result the effects of speculative execution are captured by redefining the meaning of a conditional statement, and introducing novel language constructs that model transient execution of an alternative branch. We add an abstract cache to the global state of the system, and derive some general refinement rules that expose cache side effects due to speculative loads. Underlying this extension is a semantic model that is based on instruction-level parallelism. The rules are encoded in a simulation tool, which we use to analyse an abstract specification of a Spectre attack and vulnerable code fragments. △ Less

Submitted 9 March, 2020; originally announced April 2020.

A geometric invariant of virtual n-links

Authors: Blake K Winter

Abstract: For a virtual $n$-link $K$, we define a new virtual link $VD(K)$, which is invariant under virtual equivalence of $K$. The Dehn space of $VD(K)$, which we denote $DD(K)$, therefore has a homotopy type which is an invariant of $K$. We show that the quandle and even the fundamental group of this space are able to detect the virtual trefoil. We also consider applications to higher-dimensional virtual… ▽ More For a virtual $n$-link $K$, we define a new virtual link $VD(K)$, which is invariant under virtual equivalence of $K$. The Dehn space of $VD(K)$, which we denote $DD(K)$, therefore has a homotopy type which is an invariant of $K$. We show that the quandle and even the fundamental group of this space are able to detect the virtual trefoil. We also consider applications to higher-dimensional virtual links. △ Less

Submitted 19 June, 2020; v1 submitted 1 March, 2020; originally announced March 2020.

Comments: Accepted for publication in Topology and its Applications, 6/19/20

MSC Class: 57M25; 57M27; 57Q45

How do Quantifiers Affect the Quality of Requirements?

Authors: Katharina Winter, Henning Femmer, Andreas Vogelsang

Abstract: Context: Requirements quality can have a substantial impact on the effectiveness and efficiency of using requirements artifacts in a development process. Quantifiers such as "at least", "all", or "exactly" are common language constructs used to express requirements. Quantifiers can be formulated by affirmative phrases ("At least") or negative phrases ("Not less than"). Problem: It is long assumed… ▽ More Context: Requirements quality can have a substantial impact on the effectiveness and efficiency of using requirements artifacts in a development process. Quantifiers such as "at least", "all", or "exactly" are common language constructs used to express requirements. Quantifiers can be formulated by affirmative phrases ("At least") or negative phrases ("Not less than"). Problem: It is long assumed that negation in quantification negatively affects the readability of requirements, however, empirical research on these topics remains sparse. Principal Idea: In a web-based experiment with 51 participants, we compare the impact of negations and quantifiers on readability in terms of reading effort, reading error rate and perceived reading difficulty of requirements. Results: For 5 out of 9 quantifiers, our participants performed better on the affirmative phrase compared to the negative phrase. Only for one quantifier, the negative phrase was more effective. Contribution: This research focuses on creating an empirical understanding of the effect of language in Requirements Engineering. It furthermore provides concrete advice on how to phrase requirements. △ Less

Submitted 7 February, 2020; originally announced February 2020.

Untangling the GDPR Using ConRelMiner

Authors: Karolin Winter, Stefanie Rinderle-Ma

Abstract: The General Data Protection Regulation (GDPR) poses enormous challenges on companies and organizations with respect to understanding, implementing, and maintaining the contained constraints. We report on how the ConRelMiner method can be used for untangling the GDPR. For this, the GDPR is filtered and grouped along the roles mentioned by the GDPR and the reduction of sentences to be read by analys… ▽ More The General Data Protection Regulation (GDPR) poses enormous challenges on companies and organizations with respect to understanding, implementing, and maintaining the contained constraints. We report on how the ConRelMiner method can be used for untangling the GDPR. For this, the GDPR is filtered and grouped along the roles mentioned by the GDPR and the reduction of sentences to be read by analysts is shown. Moreover, the output of the ConRelMiner - a cluster graph with relations between the sentences - is displayed and interpreted. Overall the goal is to illustrate how the effort for implementing the GDPR can be reduced and a structured and meaningful representation of the relevant GDPR sentences can be found. △ Less

Submitted 8 November, 2018; originally announced November 2018.

Correctness of Concurrent Objects under Weak Memory Models

Authors: Graeme Smith, Kirsten Winter, Robert J. Colvin

Abstract: In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when effects of operations become visible, and hence determine the semantics of objects, under a given memory model. The resulting notion of correctness, called object refinement, is generic as it is parameterised by the memory… ▽ More In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when effects of operations become visible, and hence determine the semantics of objects, under a given memory model. The resulting notion of correctness, called object refinement, is generic as it is parameterised by the memory model under consideration. Our theory enforces the minimal constraints on the placing of observations and on the semantics of objects that underlie object refinement. Object refinement is suitable as a reference for correctness when proving new proof methods for objects under weak memory models to be sound and complete. △ Less

Submitted 22 October, 2018; originally announced October 2018.

Comments: In Proceedings Refine 2018, arXiv:1810.08739. arXiv admin note: text overlap with arXiv:1802.04954

Journal ref: EPTCS 282, 2018, pp. 53-67

A sound and complete definition of linearizability on weak memory models

Authors: Graeme Smith, Kirsten Winter, Robert J. Colvin

Abstract: Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory models, in particular for TSO. In this paper, we provide an overview of this research and show that such redefinitions of linearizability are not required: under an interpretation of specification behaviour which abstract… ▽ More Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory models, in particular for TSO. In this paper, we provide an overview of this research and show that such redefinitions of linearizability are not required: under an interpretation of specification behaviour which abstracts from weak memory effects, the standard definition of linearizability is sound and complete on all hardware weak memory models. We prove our result with respect to a definition of object refinement which takes a weak memory model as a parameter. The main consequence of our findings is that we can leverage the range of existing techniques and tools for standard linearizability when verifying concurrent objects running on hardware weak memory models. △ Less

Submitted 1 July, 2019; v1 submitted 13 February, 2018; originally announced February 2018.

Comments: 33 pages, including appendix. arXiv admin note: text overlap with arXiv:1810.09612

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency

Authors: Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin

Abstract: This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an instantiation of the more abstract algebra. Many of the core properties neede… ▽ More This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an instantiation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support for program verification. In rely/guarantee concurrency, programs are specified to guarantee certain behaviours until assumptions about the behaviour of their environment are violated. When assumptions are violated, program behaviour is unconstrained (aborting), and guarantees need no longer hold. To support these guarantees a second synchronous operator, weak conjunction, was introduced: both processes in a weak conjunction must agree to take each atomic step, unless one aborts in which case the whole aborts. In develo** the laws for parallel and weak conjunction we found many properties were shared by the operators and that the proofs of many laws were essentially the same. This insight led to the idea of generalising synchronisation to an abstract operator with only the axioms that are shared by the parallel and weak conjunction operator, so that those two operators can be viewed as instantiations of the abstract synchronisation operator. The main differences between parallel and weak conjunction are how they combine individual atomic steps; that is left open in the axioms for the abstract operator. △ Less

Submitted 9 October, 2017; originally announced October 2017.

Comments: Extended version of a Formal Methods 2016 paper, "An algebra of synchronous atomic steps"

Causality and quantum theory

Authors: Blake K Winter

Abstract: We begin with a brief summary of issues encountered involving causality in quantum theory, placing careful emphasis on the assumptions involved in results such as the EPR paradox and Bell's inequality. We critique some solutions to the resulting paradox, including Rovelli's relational quantum mechanics and the many-worlds interpretation. We then discuss how a spacetime manifold could come about on… ▽ More We begin with a brief summary of issues encountered involving causality in quantum theory, placing careful emphasis on the assumptions involved in results such as the EPR paradox and Bell's inequality. We critique some solutions to the resulting paradox, including Rovelli's relational quantum mechanics and the many-worlds interpretation. We then discuss how a spacetime manifold could come about on the classical level out of a quantum system, by constructing a space with a topology out of the algebra of observables, and show that even with an hypothesis of superluminal causation enforcing consistent measurements of entangled states, a causal cone structure arises on the classical level. Finally, we discuss the possibility that causality as understood in classical relativistic physics may be an emergent symmetry which does not hold on the quantum level. △ Less

Submitted 19 May, 2017; originally announced May 2017.

MSC Class: 81P05

Ribbon n-knots with isomorphic quandles

Authors: Blake Karl Winter

Abstract: Let $K, K'$ be ribbon knottings of $n$-spheres with $1$-handles in $S^{n+2}$, $n\geq 2$. We show that if the knot quandles of these knots are isomorphic, then the ribbon knottings are stably equivalent, in the sense of Nakanishi and Nakagawa, after taking a finite number of connected sums with trivially embedded copies of $S^{n-1}\times S^{1}$. Let $K, K'$ be ribbon knottings of $n$-spheres with $1$-handles in $S^{n+2}$, $n\geq 2$. We show that if the knot quandles of these knots are isomorphic, then the ribbon knottings are stably equivalent, in the sense of Nakanishi and Nakagawa, after taking a finite number of connected sums with trivially embedded copies of $S^{n-1}\times S^{1}$. △ Less

Submitted 27 December, 2018; v1 submitted 31 January, 2017; originally announced February 2017.

MSC Class: 57Q45

An algebra of synchronous atomic steps

Authors: Ian J. Hayes, Robert Colvin, Larissa Meinicke, Kirsten Winter, Andrius Velykis

Abstract: This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties need… ▽ More This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support. △ Less

Submitted 17 January, 2022; v1 submitted 1 September, 2016; originally announced September 2016.

ACM Class: D.2.4; F.3.1

Journal ref: Fitzgerald J., Heitmeyer C., Gnesi S., Philippou A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science, vol 9995. Springer, Cham

Photometric Supernova Classification With Machine Learning

Authors: Michelle Lochner, Jason D. McEwen, Hiranya V. Peiris, Ofer Lahav, Max K. Winter

Abstract: Automated photometric supernova classification has become an active area of research in recent years in light of current and upcoming imaging surveys such as the Dark Energy Survey (DES) and the Large Synoptic Survey Telescope, given that spectroscopic confirmation of type for all supernovae discovered will be impossible. Here, we develop a multi-faceted classification pipeline, combining existing… ▽ More Automated photometric supernova classification has become an active area of research in recent years in light of current and upcoming imaging surveys such as the Dark Energy Survey (DES) and the Large Synoptic Survey Telescope, given that spectroscopic confirmation of type for all supernovae discovered will be impossible. Here, we develop a multi-faceted classification pipeline, combining existing and new approaches. Our pipeline consists of two stages: extracting descriptive features from the light curves and classification using a machine learning algorithm. Our feature extraction methods vary from model-dependent techniques, namely SALT2 fits, to more independent techniques fitting parametric models to curves, to a completely model-independent wavelet approach. We cover a range of representative machine learning algorithms, including naive Bayes, k-nearest neighbors, support vector machines, artificial neural networks and boosted decision trees (BDTs). We test the pipeline on simulated multi-band DES light curves from the Supernova Photometric Classification Challenge. Using the commonly used area under the curve (AUC) of the Receiver Operating Characteristic as a metric, we find that the SALT2 fits and the wavelet approach, with the BDTs algorithm, each achieves an AUC of 0.98, where 1 represents perfect classification. We find that a representative training set is essential for good classification, whatever the feature set or algorithm, with implications for spectroscopic follow-up. Importantly, we find that by using either the SALT2 or the wavelet feature sets with a BDT algorithm, accurate classification is possible purely from light curve data, without the need for any redshift information. △ Less

Submitted 7 September, 2016; v1 submitted 2 March, 2016; originally announced March 2016.

Comments: Matches published version. 15 pages, 7 figures

Journal ref: ApJS (2016), 225(2), p.31

Measurement of charm production in neutrino charged-current interactions

Authors: A. Kayis-Topaksu, G. Önengüt, R. van Dantzig, M. de Jong, R. G. C. Oldeman, M. Güler, U. Köse, P. Tolun, M. G. Catanesi, M. T. Muciaccia, K. Winter, B. Van de Vyver, P. Vilain, G. Wilquet, B. Saitta, E. Di Capua, S. Ogawa, H. Shibuya, I. R. Hristova, T. Kawamura, D. Kolev, H. Meinhard, J. Panman, A. Rozanov, R. Tsenov , et al. (63 additional authors not shown)

Abstract: The nuclear emulsion target of the CHORUS detector was exposed to the wide-band neutrino beam of the CERN SPS of 27 GeV average neutrino energy from 1994 to 1997. In total about 100000 charged-current neutrino interactions with at least one identified muon were located in the emulsion target and fully reconstructed, using newly developed automated scanning systems. Charmed particles were searched… ▽ More The nuclear emulsion target of the CHORUS detector was exposed to the wide-band neutrino beam of the CERN SPS of 27 GeV average neutrino energy from 1994 to 1997. In total about 100000 charged-current neutrino interactions with at least one identified muon were located in the emulsion target and fully reconstructed, using newly developed automated scanning systems. Charmed particles were searched for by a program recognizing particle decays. The observation of the decay in nuclear emulsion makes it possible to select a sample with very low background and minimal kinematical bias. 2013 charged-current interactions with a charmed hadron candidate in the final state were selected and confirmed through visual inspection. The charm production rate induced by neutrinos relative to the charged-current cross-section is measured to be sigma(nu_mu N -> mu- C X)/sigma(CC) = (5.75 +-0.32 stat +-0.30 syst)%. The charm production cross-section as a function of the neutrino energy is also obtained. The results are in good agreement with previous measurements. The charm-quark hadronization produces the following charmed hadrons with relative fractions (in %): f_Dzero = 43.7+-4.5, f_Lambda_c^plus = 19.2+-4.2, f_Dplus = 25.3+-4.2, and f_D_splus = 11.8+-4.7. △ Less

Submitted 4 July, 2011; originally announced July 2011.

Comments: 16 pages, 5 figures

Report number: CERN-PH-EP-2011-109

A Revised Ephemeris and FUSE Observations of the Supersoft X-ray Source CAL 83

Authors: P. C. Schmidtke, A. P. Cowley, J. B. Hutchings, K. Winter, D. Crampton

Abstract: A new ephemeris has been determined for the supersoft X-ray binary CAL 83 using MACHO photometry. With an improved orbital period of 1.047568 days, it is now possible to phase together photometric and spectroscopic data obtained over the past two decades with new far ultraviolet spectra taken with FUSE. We discuss the properties of the orbital and longterm optical light curves as well as the col… ▽ More A new ephemeris has been determined for the supersoft X-ray binary CAL 83 using MACHO photometry. With an improved orbital period of 1.047568 days, it is now possible to phase together photometric and spectroscopic data obtained over the past two decades with new far ultraviolet spectra taken with FUSE. We discuss the properties of the orbital and longterm optical light curves as well as the colors of CAL 83. In the far ultraviolet the only well-detected stellar feature is emission from the O VI resonance doublet. The radial velocity of this emission appears to differ from that of HeII in the optical region, although we only have partial phase coverage for the O VI line. The FUSE continuum variations are similar to the optical light curve in phase and amplitude. △ Less

Submitted 17 November, 2003; originally announced November 2003.

Comments: 21 pages and 7 figures

FUSE Spectra of the Black Hole Binary LMC X-3

Authors: J. B. Hutchings, K. Winter, D. Crampton, A. P. Cowley, P. Schmidtke

Abstract: Far-ultraviolet spectra of LMC X-3 were taken covering photometric phases 0.47 to 0.74 in the 1.7-day orbital period of the black-hole binary (phase zero being superior conjunction of the X-ray source). The continuum is faint and flat, but appears to vary significantly during the observations. Concurrent RXTE/ASM observations show the system was in its most luminous X-ray state during the FUSE o… ▽ More Far-ultraviolet spectra of LMC X-3 were taken covering photometric phases 0.47 to 0.74 in the 1.7-day orbital period of the black-hole binary (phase zero being superior conjunction of the X-ray source). The continuum is faint and flat, but appears to vary significantly during the observations. Concurrent RXTE/ASM observations show the system was in its most luminous X-ray state during the FUSE observations. The FUV spectrum contains strong terrestrial airglow emission lines, while the only stellar lines clearly present are emissions from the O VI resonance doublet. Their flux does not change significantly during the FUSE observations. These lines are modelled as two asymmetrical profiles, including the local ISM absorptions due to C II and possibly O VI. Velocity variations of O VI emission are consistent with the orbital velocity of the black hole and provide a new constraint on its mass. △ Less

Submitted 27 August, 2003; originally announced August 2003.

Comments: 12 pages including 1 table, 4 diagrams To appear in AJ

Journal ref: Astron.J.126:2368,2003

FUV Spectroscopy of the Supersoft X-ray Binary RX J0513.9-6951

Authors: J. B. Hutchings, K. Winter, D. Crampton, A. P. Cowley, P. C. Schmidtke

Abstract: We have obtained spectroscopy with the Far Ultraviolet Spectroscopic Explorer (FUSE) of the supersoft X-ray binary RX J0513.9-6951 over a complete binary orbital cycle. The spectra show a hot continuum with extremely broad O VI emission and weak Lyman absorptions. He II emission is weak and narrow, while N III and C III emissions are undetected, although lines from these ions are prominent at op… ▽ More We have obtained spectroscopy with the Far Ultraviolet Spectroscopic Explorer (FUSE) of the supersoft X-ray binary RX J0513.9-6951 over a complete binary orbital cycle. The spectra show a hot continuum with extremely broad O VI emission and weak Lyman absorptions. He II emission is weak and narrow, while N III and C III emissions are undetected, although lines from these ions are prominent at optical wavelengths. The broad O VI emission and Lyman absorption show radial velocity curves that are approximately antiphased and have semiamplitudes of ~117 +- 40 and 54 +- 10 km/s, respectively. Narrow emissions from He II and O VI show small velocity variations with phasing different from the broad O VI, but consistent with the optical line peaks. We also measure considerable changes in the FUV continuum and O VI emission line flux. We discuss the possible causes of the measured variations and a tentative binary interpretation. △ Less

Submitted 30 July, 2002; originally announced July 2002.

Comments: 21 pages, including 2 tables, 6 figures. To appear in AJ