arXiv subjects

Javier Díaz

Publications and source records attributed to Javier Díaz.

6 recordsLinked to original sources

arXiv2023

Proofs about Network Communication: For Humans and Machines

Many concurrent and distributed systems are safety-critical and therefore have to provide a high degree of assurance. Important properties of such systems are frequently proved on the specification level, but implementations typically deviate from specifications for practical reasons. Machine-checked proofs of bisimilarity statements are often useful for guaranteeing that properties of specifications carry over to implementations. In this paper, we present a way of conducting such proofs with a focus on network communication. The proofs resulting from our approach are not just machine-checked but also intelligible for humans.

cs.LO↗

arXiv2023

Recovering Arrhythmic EEG Transients from Their Stochastic Interference

Traditionally, the neuronal dynamics underlying electroencephalograms (EEG) have been understood as arising from \textit{rhythmic oscillators with varying degrees of synchronization}. This dominant metaphor employs frequency domain EEG analysis to identify the most prominent populations of neuronal current sources in terms of their frequency and spectral power. However, emerging perspectives on EEG highlight its arrhythmic nature, which is primarily inferred from broadband EEG properties like the ubiquitous $1/f$ spectrum. In the present study, we use an \textit{arrhythmic superposition of pulses} as a metaphor to explain the origin of EEG. This conceptualization has a fundamental problem because the interference produced by the superpositions of pulses generates colored Gaussian noise, masking the temporal profile of the generating pulse. We solved this problem by developing a mathematical method involving the derivative of the autocovariance function to recover excellent approximations of the underlying pulses, significantly extending the analysis of this type of stochastic processes. When the method is applied to spontaneous mouse EEG sampled at $5$ kHz during the sleep-wake cycle, specific patterns -- called $Ψ$-patterns -- characterizing NREM sleep, REM sleep, and wakefulness are revealed. $Ψ$-patterns can be understood theoretically as \textit{power density in the time domain} and correspond to combinations of generating pulses at different time scales. Remarkably, we report the first EEG wakefulness-specific feature, which corresponds to an ultra-fast ($\sim 1$ ms) transient component of the observed patterns. By shifting the paradigm of EEG genesis from oscillators to random pulse generators, our theoretical framework pushes the boundaries of traditional Fourier-based EEG analysis, paving the way for new insights into the arrhythmic components of neural dynamics.

q-bio.NC↗

arXiv2022

The amplitude modulation pattern of Gaussian noise is a fingerprint of Gaussianity

We introduce a new approach for Gaussianity testing using the envelope of a signal and its coefficient of variation. The envelope of a Gaussian signal follows the Rayleigh distribution, and given that the coefficient of variation of the Rayleigh distribution is invariant, the envelope of Gaussian noise's coefficient of variation is a universal constant and can be exploited as a discriminating statistic. The main application of this approach is to detect the Gaussianity of time series. However, the coefficient of variation of the envelope is also a measure of amplitude modulation patterns that captures the structure of the Fourier phase profile, making it a useful parameter to differentiate types of non-Gaussianity and for signal classification.

eess.SP↗

arXiv2022

Correctness of Broadcast via Multicast: Graphically and Formally

Maintaining data consistency among multiple parties requires nodes to repeatedly send data to all other nodes. For example, the nodes of a blockchain network have to disseminate the blocks they create across the whole network. The scientific literature typically takes the ideal perspective that such data distribution is performed by broadcasting to all nodes directly, while in practice data is distributed by repeated multicast. Since correctness and security of consistency maintenance protocols usually have been established for the ideal setting only, it is vital to show that these properties carry over to real-world implementations. Therefore, it is desirable to prove that the ideal and the real behavior are equivalent. In the work described in this paper, we take an important step towards such a proof by proving a simpler variant of this equivalence statement. The simplification is that we consider only a concrete pair of network topologies, which nevertheless illustrates important phenomena encountered with arbitrary topologies. For describing systems that distribute data, we use a domain-specific language of processes that corresponds to a class of Petri nets and is embedded in a general-purpose process calculus. This way, we can outline our proof using an intuitive graphical notation and leverage the rich theory of process calculi in the actual proof, which is machine-checked using the Isabelle proof assistant.

cs.LO↗

arXiv2022

Your Blockchain Needn't Care How the Message is Spread

In a blockchain system, nodes regularly distribute data to other nodes. The ideal perspective taken in the scientific literature is that data is broadcast to all nodes directly, while in practice data is distributed by repeated multicast. Since correctness and security typically have been established for the ideal setting only, it is vital to show that these properties carry over to real-world implementations. This can be done by proving that the ideal and the real behavior are equivalent. In the work described in this paper, we take an important step towards such a proof by proving a simpler variant of the above equivalence statement. The simplification is that we consider only a concrete pair of network topologies, which nevertheless illustrates important phenomena encountered with arbitrary topologies. For describing systems that distribute data, we use a domain-specific language of processes that is embedded in a general-purpose process calculus. This allows us to leverage the rich theory of process calculi in our proof, which is machine-checked using the Isabelle proof assistant.

cs.PL↗

arXiv2021

Magnetic moment orientation and in depth distribution of dysprosium near the surface of DyCo$_{4.6}$ thin films determined by the analysis of their X ray circularly polarized absorption Dy $M_{5}$ spectra

We have investigated the RE atomic distribution and its magnetic moment orientation at the region near the surface of DyCo$_{4.4 \& 4.6}$ ferrimagnetic amorphous films with perpendicular magnetic anisotropy (PMA). XMCD spectroscopy of the films at the Dy $M_{4,5}$ and Co $L_{2,3}$ edges using total electron yield (TEY) detection was performed at 2 K and 300 K temperatures, and at sample orientations ranged from 0$^{\circ}$ to 70$^{\circ}$ with respect to the magnetic easy axis. The measurements showed an apparent partial decoupling between the cobalt and dysprosium magnetic sublattices. At RT, the magnetic moment per atom of dysprosium was below the minimum value expected if all dysprosium moments were AF coupled to cobalt. At 2 K, the cobalt sublattice presented a stronger magnetic anisotropic behavior than the dysprosium sublattice. A detailed analysis of the circularly polarized spectra of the Dy $M_{5}$ edge, based on the deconvolution of the spectra in their related parallel, antiparallel and transverse to $J_{z}$ spectral components, demonstrates that the spectra are composed by dysprosium with different magnetic moment distributions. The fit of the Dy $M_{5}$ spectra using the $J_{z}$ spectral components evidenced a gradation of dysprosium concentration due to segregation at the region probed by TEY. The topmost layer was magnetically uncoupled from cobalt. At RT, 25$\%$ of the dysprosium magnetic moments in the under layer were found averaged oriented in the same direction as cobalt. The expected weak magnetic coupling of these dysprosium atoms to cobalt would explain the surprisingly lower magnetic anisotropy of the dysprosium sublattice compared to that of cobalt probed by TEY at 2 K.

cond-mat.mtrl-sci↗