• ### Behavioural equivalences for fluid stochastic Petri nets(1706.02641)

June 8, 2017 cs.LO
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.
• 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.
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\$.