-
We propose fluid equivalences to compare and reduce behaviour of labeled
fluid stochastic Petri nets (LFSPNs) while preserving their discrete and
continuous properties. We define a linear-time relation of fluid trace
equivalence and its branching-time counterpart, fluid bisimulation equivalence.
Both fluid relations take into account the essential features of the LFSPNs
behaviour: functional activity, stochastic timing and fluid flow. We consider
the LFSPNs whose continuous markings have no influence to the discrete ones and
whose discrete part is continuous time stochastic Petri nets. The underlying
stochastic model for the discrete part of the LFSPNs is continuous time Markov
chains (CTMCs). The performance analysis of the continuous part of LFSPNs is
accomplished via the associated stochastic fluid models (SFMs). We show that
fluid trace equivalence preserves average potential fluid change volume for the
transition sequences of every certain length. We prove that fluid bisimulation
equivalence preserves the aggregated probability functions: stationary
probability mass for the underlying CTMC, as well as stationary fluid buffer
empty probability, fluid density and distribution for the associated SFM.
Hence, the equivalence guarantees identity of a number of discrete and
continuous performance measures. Fluid bisimulation equivalence is then used to
simplify the qualitative and quantitative analysis of LFSPNs via quotienting
the discrete reachability graph and underlying CTMC. To describe the quotient
associated SFM, the quotients of the probability functions are defined. We
characterize logically fluid trace and bisimulation equivalences with two novel
fluid modal logics $HML_{flt}$ and $HML_{flb}$, based on the Hennessy-Milner
Logic HML. The application example of a document preparation system
demonstrates the behavioural analysis via quotienting by fluid bisimulation
equivalence.
-
We measure the energy emitted by extensive air showers in the form of radio
emission in the frequency range from 30 to 80 MHz. Exploiting the accurate
energy scale of the Pierre Auger Observatory, we obtain a radiation energy of
15.8 \pm 0.7 (stat) \pm 6.7 (sys) MeV for cosmic rays with an energy of 1 EeV
arriving perpendicularly to a geomagnetic field of 0.24 G, scaling
quadratically with the cosmic-ray energy. A comparison with predictions from
state-of-the-art first-principle calculations shows agreement with our
measurement. The radiation energy provides direct access to the calorimetric
energy in the electromagnetic cascade of extensive air showers. Comparison with
our result thus allows the direct calibration of any cosmic-ray radio detector
against the well-established energy scale of the Pierre Auger Observatory.
-
The Auger Engineering Radio Array (AERA) is part of the Pierre Auger
Observatory and is used to detect the radio emission of cosmic-ray air showers.
These observations are compared to the data of the surface detector stations of
the Observatory, which provide well-calibrated information on the cosmic-ray
energies and arrival directions. The response of the radio stations in the 30
to 80 MHz regime has been thoroughly calibrated to enable the reconstruction of
the incoming electric field. For the latter, the energy deposit per area is
determined from the radio pulses at each observer position and is interpolated
using a two-dimensional function that takes into account signal asymmetries due
to interference between the geomagnetic and charge-excess emission components.
The spatial integral over the signal distribution gives a direct measurement of
the energy transferred from the primary cosmic ray into radio emission in the
AERA frequency range. We measure 15.8 MeV of radiation energy for a 1 EeV air
shower arriving perpendicularly to the geomagnetic field. This radiation energy
-- corrected for geometrical effects -- is used as a cosmic-ray energy
estimator. Performing an absolute energy calibration against the
surface-detector information, we observe that this radio-energy estimator
scales quadratically with the cosmic-ray energy as expected for coherent
emission. We find an energy resolution of the radio reconstruction of 22% for
the data set and 17% for a high-quality subset containing only events with at
least five radio stations with signal.
-
Neutrinos in the cosmic ray flux with energies near 1 EeV and above are
detectable with the Surface Detector array of the Pierre Auger Observatory. We
report here on searches through Auger data from 1 January 2004 until 20 June
2013. No neutrino candidates were found, yielding a limit to the diffuse flux
of ultra-high energy neutrinos that challenges the Waxman-Bahcall bound
predictions. Neutrino identification is attempted using the broad
time-structure of the signals expected in the SD stations, and is efficiently
done for neutrinos of all flavors interacting in the atmosphere at large zenith
angles, as well as for "Earth-skimming" neutrino interactions in the case of
tau neutrinos. In this paper the searches for downward-going neutrinos in the
zenith angle bins $60^\circ-75^\circ$ and $75^\circ-90^\circ$ as well as for
upward-going neutrinos, are combined to give a single limit. The $90\%$ C.L.
single-flavor limit to the diffuse flux of ultra-high energy neutrinos with an
$E^{-2}$ spectrum in the energy range $1.0 \times 10^{17}$ eV - $2.5 \times
10^{19}$ eV is $E_\nu^2 dN_\nu/dE_\nu < 6.4 \times 10^{-9}~ {\rm GeV~ cm^{-2}~
s^{-1}~ sr^{-1}}$.
-
A measurement of the cosmic-ray spectrum for energies exceeding
$4{\times}10^{18}$ eV is presented, which is based on the analysis of showers
with zenith angles greater than $60^{\circ}$ detected with the Pierre Auger
Observatory between 1 January 2004 and 31 December 2013. The measured spectrum
confirms a flux suppression at the highest energies. Above $5.3{\times}10^{18}$
eV, the "ankle", the flux can be described by a power law $E^{-\gamma}$ with
index $\gamma=2.70 \pm 0.02 \,\text{(stat)} \pm 0.1\,\text{(sys)}$ followed by
a smooth suppression region. For the energy ($E_\text{s}$) at which the
spectral flux has fallen to one-half of its extrapolated value in the absence
of suppression, we find
$E_\text{s}=(5.12\pm0.25\,\text{(stat)}^{+1.0}_{-1.2}\,\text{(sys)}){\times}10^{19}$
eV.
-
Contributions of the Pierre Auger Collaboration to the 33rd International
Cosmic Ray Conference, Rio de Janeiro, Brazil, July 2013
-
A large number of different model checking approaches has been proposed
during the last decade. The different approaches are applicable to different
model types including untimed, timed, probabilistic and stochastic models. This
paper presents a new framework for model checking techniques which includes
some of the known approaches, but enlarges the class of models for which model
checking can be applied to the general class of weighted automata. The approach
allows an easy adaption of model checking to models which have not been
considered yet for this purpose. Examples for those new model types for which
model checking can be applied are max/plus or min/plus automata which are well
established models to describe different forms of dynamic systems and
optimization problems. In this context, model checking can be used to verify
temporal or quantitative properties of a system. The paper first presents
briefly our class of weighted automata, as a very general model type. Then
Valued Computational Tree Logic (CTL$) is introduced as a natural extension of
the well known branching time logic CTL. Afterwards, algorithms to check a
weighted automaton according to a CTL$ formula are presented. As a last result,
a bisimulation is presented for weighted automata and for CTL$.