-
Stalnaker's Epistemic Logic in Isabelle/HOL
Authors:
Laura P. Gamboa Guzman,
Kristin Y. Rozier
Abstract:
The foundations of formal models for epistemic and doxastic logics often rely on certain logical aspects of modal logics such as S4 and S4.2 and their semantics; however, the corresponding mathematical results are often stated in papers or books without including a detailed proof, or a reference to it, that allows the reader to convince themselves about them. We reinforce the foundations of the ep…
▽ More
The foundations of formal models for epistemic and doxastic logics often rely on certain logical aspects of modal logics such as S4 and S4.2 and their semantics; however, the corresponding mathematical results are often stated in papers or books without including a detailed proof, or a reference to it, that allows the reader to convince themselves about them. We reinforce the foundations of the epistemic logic S4.2 for countably many agents by formalizing its soundness and completeness results for the class of all weakly-directed pre-orders in the proof assistant Isabelle/HOL. This logic corresponds to the knowledge fragment, i.e., the logic for formulas that may only include knowledge modalities in Stalnaker's system for knowledge and belief. Additionally, we formalize the equivalence between two axiomatizations for S4, which are used depending on the type of semantics given to the modal operators, as one is commonly used for the relational semantics, and the other one arises naturally from the topological semantics.
△ Less
Submitted 23 April, 2024;
originally announced April 2024.
-
Challenges of Quantum Software Engineering for the Next Decade: The Road Ahead
Authors:
Juan M. Murillo,
Jose Garcia-Alonso,
Enrique Moguel,
Johanna Barzen,
Frank Leymann,
Shaukat Ali,
Tao Yue,
Paolo Arcaini,
Ricardo Pérez Castillo,
Ignacio García Rodríguez de Guzmán,
Mario Piattini,
Antonio Ruiz-Cortés,
Antonio Brogi,
Jianjun Zhao,
Andriy Miranskyy,
Manuel Wimmer
Abstract:
As quantum computers evolve, so does the complexity of the software that they can run. To make this software efficient, maintainable, reusable, and cost-effective, quality attributes that any industry-grade software should strive for, mature software engineering approaches should be applied during its design, development, and operation. Due to the significant differences between classical and quan…
▽ More
As quantum computers evolve, so does the complexity of the software that they can run. To make this software efficient, maintainable, reusable, and cost-effective, quality attributes that any industry-grade software should strive for, mature software engineering approaches should be applied during its design, development, and operation. Due to the significant differences between classical and quantum software, applying classical software engineering solutions to quantum software is difficult. This resulted in the birth of Quantum Software Engineering as a discipline in the contemporary software engineering landscape. In this work, a set of active researchers is currently addressing the challenges of Quantum Software Engineering and analyzing the most recent research advances in this domain. This analysis is used to identify needed breakthroughs and future research directions for Quantum Software Engineering.
△ Less
Submitted 10 April, 2024;
originally announced April 2024.
-
Resource allocation exploiting reflective surfaces to minimize the outage probability in VLC
Authors:
Borja Genoves Guzman,
Maximo Morales Cespedes,
Victor P. Gil Jimenez,
Ana Garcia Armada,
Maite Brandt-Pearce
Abstract:
Visible light communication (VLC) is a technology that complements radio frequency (RF) to fulfill the ever-increasing demand for wireless data traffic. The ubiquity of light-emitting diodes (LEDs), exploited as transmitters, increases the VLC market penetration and positions it as one of the most promising technologies to alleviate the spectrum scarcity of RF. However, VLC deployment is hindered…
▽ More
Visible light communication (VLC) is a technology that complements radio frequency (RF) to fulfill the ever-increasing demand for wireless data traffic. The ubiquity of light-emitting diodes (LEDs), exploited as transmitters, increases the VLC market penetration and positions it as one of the most promising technologies to alleviate the spectrum scarcity of RF. However, VLC deployment is hindered by blockage causing connectivity outages in the presence of obstacles. Recently, optical reconfigurable intelligent surfaces (ORISs) have been considered to mitigate this problem. While prior works exploit ORISs for data or secrecy rate maximization, this paper studies the optimal placement of mirrors and ORISs, and the LED power allocation, for jointly minimizing the outage probability while kee** the lighting standards. We describe an optimal outage minimization framework and present solvable heuristics. We provide extensive numerical results and show that the use of ORISs may reduce the outage probability by up to 67% with respect to a no-mirror scenario and provide a gain of hundreds of kbit/J in optical energy efficiency with respect to the presented benchmark.
△ Less
Submitted 29 January, 2024;
originally announced January 2024.
-
Calculating spin correlations with a quantum computer
Authors:
Jed Brody,
Gavin Guzman
Abstract:
We calculate spin correlation functions using IBM quantum processors, accessed online. We demonstrate the rotational invariance of the singlet state, interesting properties of the triplet states, and surprising features of a state of three entangled qubits. This exercise is ideal for remote learning and generates data with real quantum mechanical systems that are impractical to investigate in the…
▽ More
We calculate spin correlation functions using IBM quantum processors, accessed online. We demonstrate the rotational invariance of the singlet state, interesting properties of the triplet states, and surprising features of a state of three entangled qubits. This exercise is ideal for remote learning and generates data with real quantum mechanical systems that are impractical to investigate in the local laboratory. Students learn a wide variety of skills, including calculation of multipartite spin correlation functions, design and analysis of quantum circuits, and remote measurement with real quantum processors.
△ Less
Submitted 26 June, 2022;
originally announced June 2022.
-
A Fiber Measurement System with Approximate Deconvolution Based on the Analysis of Fault Clusters in Linearized Bregman Iterations
Authors:
Yuneisy Garcia Guzman,
Felipe Calliari,
Gustavo C. Amaral,
Michael Lunglmayr
Abstract:
Automatic detection of faults in optical fibers is an active area of research that plays a significant role in the design of reliable and stable optical networks. A fiber measurement system that combines automated data acquisition and processing represents a disruptive impact in the management of optical fiber networks with fast and reliable event detection. It has been shown in the literature tha…
▽ More
Automatic detection of faults in optical fibers is an active area of research that plays a significant role in the design of reliable and stable optical networks. A fiber measurement system that combines automated data acquisition and processing represents a disruptive impact in the management of optical fiber networks with fast and reliable event detection. It has been shown in the literature that the linearized Bregman iterations (LBI) algorithm and variations can be successfully used for processing and accurately identifying faults in a fiber profile. One of the factors that impact the performance of these algorithms is the degradation of spatial resolution, which is mainly caused by the appearance of fault clusters due to a reduced number of iterations. In this paper, a method is proposed based on an approximate deconvolution approach for increasing the spatial resolution, possible after a thorough analysis of fault clusters that appear in the algorithm's output. The effect of such approximate deconvolution is shown to extend beyond the improvement of spatial resolution, allowing for better performances to be reached at shorter processing times. An efficient hardware architecture that implements the approximate deconvolution, compatible with the hardware structure recently presented for the LBI algorithm, is also proposed and discussed.
△ Less
Submitted 4 November, 2021;
originally announced November 2021.
-
How to help university students to manage their interruptions and improve their attention and time management
Authors:
Aurora Vizcaíno,
Ignacio García-Rodríguez de Guzmán,
Antonio Manjavacas,
Félix García,
José A. Cruz-Lemus,
Manuel Ángel Serrano
Abstract:
Technology has changed both our way of life and the way in which we learn. Students now attend lectures with laptops and mobile phones, and this situation is accentuated in the case of students on Computer Science degrees, since they require their computers in order to participate in both theoretical and practical lessons. Problems, however, arise when the students' social networks are opened on t…
▽ More
Technology has changed both our way of life and the way in which we learn. Students now attend lectures with laptops and mobile phones, and this situation is accentuated in the case of students on Computer Science degrees, since they require their computers in order to participate in both theoretical and practical lessons. Problems, however, arise when the students' social networks are opened on their computers and they receive notifications that interrupt their work. We set up a workshop regarding time, thoughts and attention management with the objective of teaching our students techniques that would allow them to manage interruptions, concentrate better and definitively make better use of their time. Those who took part in the workshop were then evaluated to discover its effects. The results obtained are quite optimistic and are described in this paper with the objective of encouraging other universities to perform similar initiatives.
△ Less
Submitted 23 April, 2021;
originally announced April 2021.
-
Rational and $p$-local Motivic Homotopy Theory
Authors:
Gabriela Guzman
Abstract:
Let $F$ and $k$ be perfect fields. The main goal of this paper is to investigate algebraic models for the Morel-Voevodsky unstable motivic homotopy category $\mathrm{Ho}(F)$ after $\mathbf{H}^{\mathbb{A}^1}k$ localization. More specifically, we extend results of Goerss to the $\mathbb{A}^1$-algebraic topology setting: we study the homotopy theory of the category $s\mathrm{coCAlg}_k(Sm_F)$ of presh…
▽ More
Let $F$ and $k$ be perfect fields. The main goal of this paper is to investigate algebraic models for the Morel-Voevodsky unstable motivic homotopy category $\mathrm{Ho}(F)$ after $\mathbf{H}^{\mathbb{A}^1}k$ localization. More specifically, we extend results of Goerss to the $\mathbb{A}^1$-algebraic topology setting: we study the homotopy theory of the category $s\mathrm{coCAlg}_k(Sm_F)$ of presheaves of simplicial coalgebras over a field $k$ and their $τ$ and $\mathbb{A}^1$-localizations. For $k$ algebraically closed, we show that the unit of the adjunction $k^δ[-]\dashv(-)^{gp}$ determines the $\mathbf{H}^{\mathbb{A}^1}k$ homotopy type, where $k^δ[-]$ is the canonical coalgebra functor induced by the diagonal map $Δ:\mathcal{X}\rightarrow \mathcal{X}\times \mathcal{X}$. We extend this result for the category of presheaves of coalgebras over a non-algebraically closed field $k$ and the category of discrete $G$-motivic spaces, for $G=Gal(\bar{k}/k)$.
On the other hand, we show that the category of coalgebra objects in $\mathrm{PST}(Sm_F,k)$ is locally presentable, where $\mathrm{PST}(Sm_F,k)$ is the category of presheaves with Voevodsky transfers and the monoidal structure is given by a Day convolution product.
△ Less
Submitted 12 November, 2019;
originally announced November 2019.
-
Fuse and IUE Spectroscopy of the Prototype Dwarf Nova ER Ursa Majoris During Quiescence
Authors:
Giannina Guzman,
Edward Sion,
Patrick Godon
Abstract:
ER Ursae Majoris is the prototype for a subset of SU UMa-type dwarf novae characterized by short cycle times between outburst, high outburst frequency, and ``negative'' superhumps. It suffers superoutbursts every 43 days, lasting 20 days, normal outbursts every 4 days and has an outburst amplitude of 3 magnitudes. We have carried out a far ultraviolet (FUV) spectral analysis of ER UMa in quiescenc…
▽ More
ER Ursae Majoris is the prototype for a subset of SU UMa-type dwarf novae characterized by short cycle times between outburst, high outburst frequency, and ``negative'' superhumps. It suffers superoutbursts every 43 days, lasting 20 days, normal outbursts every 4 days and has an outburst amplitude of 3 magnitudes. We have carried out a far ultraviolet (FUV) spectral analysis of ER UMa in quiescence, by fitting Far Ultraviolet Spectroscopic Explorer (FUSE) and International Ultraviolet Explorer (IUE) spectra with model accretion disks and high gravity photosphere models. Using the Gaia parallax distance and an orbital inclination of $50^{\circ}$, we find that during the brief quiescence of only four days, the accretion rate is $7.3 \times 10^{-11}M_{\odot}$/yr, with the ER UMa white dwarf contributing 55% of the FUV flux and the accretion disk contributing the remaining 45\% of the flux. The white dwarf in ER UMa is markedly hotter (32,000~K) than the other white dwarfs in dwarf novae below the CV period gap which have typical temperatures $\sim$15,000~K. For a higher inclinations of 60 to 75 degrees, the accretion rates that we derive are roughly an order of magnitude higher $1 - 3 \times 10^{-10}M_{\odot}$/yr.
△ Less
Submitted 15 July, 2019;
originally announced July 2019.
-
astroquery: An Astronomical Web-Querying Package in Python
Authors:
Adam Ginsburg,
Brigitta M. Sipőcz,
C. E. Brasseur,
Philip S. Cowperthwaite,
Matthew W. Craig,
Christoph Deil,
James Guillochon,
Giannina Guzman,
Simon Liedtke,
Pey Lian Lim,
Kelly E. Lockhart,
Michael Mommert,
Brett M. Morris,
Henrik Norman,
Madhura Parikh,
Magnus V. Persson,
Thomas P. Robitaille,
Juan-Carlos Segovia,
Leo P. Singer,
Erik J. Tollerud,
Miguel de Val-Borro,
Ivan Valtchanov,
Julien Woillez,
the Astroquery collaboration
Abstract:
astroquery is a collection of tools for requesting data from databases hosted on remote servers with interfaces exposed on the internet, including those with web pages but without formal application program interfaces (APIs). These tools are built on the Python requests package, which is used to make HTTP requests, and astropy, which provides most of the data parsing functionality. astroquery modu…
▽ More
astroquery is a collection of tools for requesting data from databases hosted on remote servers with interfaces exposed on the internet, including those with web pages but without formal application program interfaces (APIs). These tools are built on the Python requests package, which is used to make HTTP requests, and astropy, which provides most of the data parsing functionality. astroquery modules generally attempt to replicate the web page interface provided by a given service as closely as possible, making the transition from browser-based to command-line interaction easy. astroquery has received significant contributions from throughout the astronomical community, including several significant contributions from telescope archives. astroquery enables the creation of fully reproducible workflows from data acquisition through publication. This paper describes the philosophy, basic structure, and development model of the astroquery package. The complete documentation for astroquery can be found at http://astroquery.readthedocs.io/.
△ Less
Submitted 14 January, 2019;
originally announced January 2019.
-
A Survey of CH3CN and HC3N in Protoplanetary Disks
Authors:
Jennifer B. Bergner,
Viviana G. Guzman,
Karin I. Oberg,
Ryan A. Loomis,
Jamila Pegues
Abstract:
The organic content of protoplanetary disks sets the initial compositions of planets and comets, thereby influencing subsequent chemistry that is possible in nascent planetary systems. We present observations of the complex nitrile-bearing species CH3CN and HC3N towards the disks around the T Tauri stars AS 209, IM Lup, LkCa 15, and V4046 Sgr as well as the Herbig Ae stars MWC 480 and HD 163296. H…
▽ More
The organic content of protoplanetary disks sets the initial compositions of planets and comets, thereby influencing subsequent chemistry that is possible in nascent planetary systems. We present observations of the complex nitrile-bearing species CH3CN and HC3N towards the disks around the T Tauri stars AS 209, IM Lup, LkCa 15, and V4046 Sgr as well as the Herbig Ae stars MWC 480 and HD 163296. HC3N is detected towards all disks except IM Lup, and CH3CN is detected towards V4046 Sgr, MWC 480, and HD 163296. Rotational temperatures derived for disks with multiple detected lines range from 29-73K, indicating emission from the temperate molecular layer of the disk. V4046 Sgr and MWC 480 radial abundance profiles are constrained using a parametric model; the gas-phase CH3CN and HC3N abundances with respect to HCN are a few to tens of percent in the inner 100 AU of the disk, signifying a rich nitrile chemistry at planet- and comet-forming disk radii. We find consistent relative abundances of CH3CN, HC3N, and HCN between our disk sample, protostellar envelopes, and solar system comets; this is suggestive of a robust nitrile chemistry with similar outcomes under a wide range of physical conditions.
△ Less
Submitted 13 March, 2018;
originally announced March 2018.
-
CTZS Thin Films Grown by a Sequential Deposition of Precursors
Authors:
Daniel Cruz-Lemus,
Miguel Angel Gracia-Pinilla,
Mikel Hurtado,
Gerardo Gordillo Guzman,
Iver Lauermann
Abstract:
A comparative study of the structural, optical and morphological properties of Cu2ZnSnS4 (CZTS) thin films prepared by two different techniques was performed. One consists of sequential evaporation of the elemental metallic precursors under a flux of sulphur supplied by evaporation from an effusion cell (physical vapor deposition-PVD) and the second one is a solution-based chemical route where thi…
▽ More
A comparative study of the structural, optical and morphological properties of Cu2ZnSnS4 (CZTS) thin films prepared by two different techniques was performed. One consists of sequential evaporation of the elemental metallic precursors under a flux of sulphur supplied by evaporation from an effusion cell (physical vapor deposition-PVD) and the second one is a solution-based chemical route where thin layers of CuS, SnS and ZnS are deposited sequentially by diffusion membrane- assisted chemical bath deposition techniques; the membranes are used to optimize the kinetic growth through a moderate control of the release of the metal into CBD solution by osmosis. The present comparative study is helpful to the synthesis of kesterite nanostructured thin films.
△ Less
Submitted 9 October, 2014;
originally announced October 2014.
