-
Demonstration of Near-Epithermal Neutron Reflective Optics
Authors:
Takuhiro Fujiie,
Ryota Abe,
Masahiro Hino,
Mayu Hishida,
Takuya Hosobata,
Masaaki Kitaguchi,
Rintaro Nakabe,
Kenichi Oikawa,
Takuya Okudaira,
Joseph D. Parker,
Kenji Sakai,
Hirohiko M. Shimizu,
Yusuke Tsuchikawa,
Yutaka Yamagata
Abstract:
Specular reflection of neutrons on material surfaces has been demonstrated in the energy range of 0.09-0.7 eV. The results suggest that the applicable energy range of reflective neutron optics can be extended to the near-epithermal region by using existing techniques.
Specular reflection of neutrons on material surfaces has been demonstrated in the energy range of 0.09-0.7 eV. The results suggest that the applicable energy range of reflective neutron optics can be extended to the near-epithermal region by using existing techniques.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
Development of a near-infrared wide-field integral field unit by ultra-precision diamond cutting
Authors:
Kosuke Kushibiki,
Shinobu Ozaki,
Masahiro Takeda,
Takuya Hosobata,
Yutaka Yamagata,
Shinya Morita,
Toshihiro Tsuzuki,
Keiichi Nakagawa,
Takao Saiki,
Yutaka Ohtake,
Kenji Mitsui,
Hirofumi Okita,
Yutaro Kitagawa,
Yukihiro Kono,
Kentaro Motohara,
Hidenori Takahashi,
Masahiro Konishi,
Natsuko Kato,
Shuhei Koyama,
Nuo Chen
Abstract:
Integral Field Spectroscopy (IFS) is an observational method to obtain spatially resolved spectra over a specific field of view (FoV) in a single exposure. In recent years, near-infrared IFS has gained importance in observing objects with strong dust attenuation or at high redshift. One limitation of existing near-infrared IFS instruments is their relatively small FoV, less than 100 arcsec$^2$, co…
▽ More
Integral Field Spectroscopy (IFS) is an observational method to obtain spatially resolved spectra over a specific field of view (FoV) in a single exposure. In recent years, near-infrared IFS has gained importance in observing objects with strong dust attenuation or at high redshift. One limitation of existing near-infrared IFS instruments is their relatively small FoV, less than 100 arcsec$^2$, compared to optical instruments. Therefore, we have developed a near-infrared (0.9-2.5 $\mathrmμ$m) image-slicer type integral field unit (IFU) with a larger FoV of 13.5 $\times$ 10.4 arcsec$^2$ by matching a slice width to a typical seeing size of 0.4 arcsec. The IFU has a compact optical design utilizing off-axis ellipsoidal mirrors to reduce aberrations. Complex optical elements were fabricated using an ultra-precision cutting machine to achieve RMS surface roughness of less than 10 nm and a P-V shape error of less than 300 nm. The ultra-precision machining can also simplify alignment procedures. The on-sky performance evaluation confirmed that the image quality and the throughput of the IFU were as designed. In conclusion, we have successfully developed a compact IFU utilizing an ultra-precision cutting technique, almost fulfilling the requirements.
△ Less
Submitted 3 March, 2024;
originally announced March 2024.
-
Sagnac-type neutron displacement-noise-free interferometeric gravitational-wave detector
Authors:
Yuki Kawasaki,
Shoki Iwaguchi,
Tomohiro Ishikawa,
Atsushi Nishizawa,
Masaaki Kitaguchi,
Yutaka Yamagata,
Yanbei Chen,
Bin Wu,
Ryuma Shimizu,
Kurumi Umemura,
Kenji Tsuji,
Hirohiko Shimizu,
Yuta Michimura,
Kazuhiro Kobayashi,
Takafumi Onishi,
Seiji Kawamura
Abstract:
The detection of low-frequency gravitational waves on Earth requires the reduction of displacement noise, which dominates the low-frequency band. One method to cancel test mass displacement noise is a neutron displacement-noise-free interferometer (DFI). This paper proposes a new neutron DFI configuration, a Sagnac-type neutron DFI, which uses a Sagnac interferometer in place of the Mach-Zehnder i…
▽ More
The detection of low-frequency gravitational waves on Earth requires the reduction of displacement noise, which dominates the low-frequency band. One method to cancel test mass displacement noise is a neutron displacement-noise-free interferometer (DFI). This paper proposes a new neutron DFI configuration, a Sagnac-type neutron DFI, which uses a Sagnac interferometer in place of the Mach-Zehnder interferometer. We demonstrate that a sensitivity of the Sagnac-type neutron DFI is higher than that of a conventional neutron DFI with the same interferometer scale. This configuration is particularly significant for neutron DFIs with limited space for construction and limited flux from available neutron sources.
△ Less
Submitted 25 March, 2024; v1 submitted 12 November, 2023;
originally announced November 2023.
-
Notion of validity for the bilateral classical logic
Authors:
Ukyo Suzuki,
Yoriyuki Yamagata
Abstract:
This paper explores proof-theoretic semantics, a formal approach to inferential semantics. It derives sentence meaning from formalized proofs, building upon Gentzen and Prawitz's work. The study addresses challenges in understanding how proofs contribute to sentence meaning. In this setting, classical logic poses "Dummett's challenge" due to its mismatch with the proof-theoretic framework designed…
▽ More
This paper explores proof-theoretic semantics, a formal approach to inferential semantics. It derives sentence meaning from formalized proofs, building upon Gentzen and Prawitz's work. The study addresses challenges in understanding how proofs contribute to sentence meaning. In this setting, classical logic poses "Dummett's challenge" due to its mismatch with the proof-theoretic framework designed for intuitionist logic. For example, in Rumfitt's bilateral classical logic (BCL), the justification of coordination rules, notably RAA, is contentious. This paper employs the notion of validity, introduced by Prawitz, to provide a comprehensive justification for BCL, defining valid arguments and demonstrating its soundness. It resolves the circularity associated with RAA using fixed-point construction. Notably, this approach relies on impredicative comprehension but without on the excluded middle principle, suggesting that bivalence may not be essential for justifying classical logic.
△ Less
Submitted 20 October, 2023;
originally announced October 2023.
-
Development of Neutron Interferometer using Multilayer Mirrors and Measurements of Neutron-Nuclear Scattering Length with Pulsed Neutron Source
Authors:
Takuhiro Fujiie,
Masahiro Hino,
Takuya Hosobata,
Go Ichikawa,
Masaaki Kitaguchi,
Kenji Mishima,
Yoshichika Seki,
Hirohiko M. Shimizu,
Yutaka Yamagata
Abstract:
This study entailed the successful deployment of a novel neutron interferometer that utilizes multilayer mirrors. The apparatus facilitates a precise evaluation of the wavelength dependence of interference fringes utilizing a pulsed neutron source. Our interferometer achieved an impressive precision of 0.02 rad within a 20-min of recording time. Compared to systems using silicon crystals, the meas…
▽ More
This study entailed the successful deployment of a novel neutron interferometer that utilizes multilayer mirrors. The apparatus facilitates a precise evaluation of the wavelength dependence of interference fringes utilizing a pulsed neutron source. Our interferometer achieved an impressive precision of 0.02 rad within a 20-min of recording time. Compared to systems using silicon crystals, the measurement sensitivity was maintained even when using a simplified disturbance suppressor. By segregating beam paths entirely, we achieved successful measurements of neutron-nuclear scattering lengths across various samples. The values measured for Si, Al, and Ti were in agreement with those found in the literature, while V showed a disparity of 45%. This discrepancy may be attributable to impurities encountered in previous investigations. The accuracy of measurements can be enhanced further by mitigating systematic uncertainties that are associated with neutron wavelength, sample impurity, and thickness. This novel neutron interferometer enables us to measure fundamental parameters, such as the neutron-nuclear scattering length of materials, with a precision that surpasses that of conventional interferometers.
△ Less
Submitted 5 October, 2023; v1 submitted 19 July, 2023;
originally announced August 2023.
-
On the Metric Temporal Logic for Continuous Stochastic Processes
Authors:
Mitsumasa Ikeda,
Yoriyuki Yamagata,
Takayuki Kihara
Abstract:
In this paper, we prove measurability of event for which a general continuous-time stochastic process satisfies continuous-time Metric Temporal Logic (MTL) formula. Continuous-time MTL can define temporal constrains for physical system in natural way. Then there are several researches that deal with probability of continuous MTL semantics for stochastic processes. However, proving measurability fo…
▽ More
In this paper, we prove measurability of event for which a general continuous-time stochastic process satisfies continuous-time Metric Temporal Logic (MTL) formula. Continuous-time MTL can define temporal constrains for physical system in natural way. Then there are several researches that deal with probability of continuous MTL semantics for stochastic processes. However, proving measurability for such events is by no means an obvious task, even though it is essential. The difficulty comes from the semantics of "until operator", which is defined by logical sum of uncountably many propositions. Given the difficulty involved in proving the measurability of such an event using classical measure-theoretic methods, we employ a theorem from stochastic analysis. This theorem is utilized to prove the measurability of hitting times for stochastic processes, and it stands as a profound result within the theory of capacity. Next, we provide an example that illustrates the failure of probability approximation when discretizing the continuous semantics of MTL formulas with respect to time. Additionally, we prove that the probability of the discretized semantics converges to that of the continuous semantics when we impose restrictions on diamond operators to prevent nesting.
△ Less
Submitted 12 June, 2024; v1 submitted 2 August, 2023;
originally announced August 2023.
-
Displacement-noise-free interferometeric gravitational-wave detector using unidirectional neutrons with four speeds
Authors:
Shoki Iwaguchi,
Atsushi Nishizawa,
Yanbei Chen,
Yuki Kawasaki,
Tomohiro Ishikawa,
Masaaki Kitaguchi,
Yutaka Yamagata,
Bin Wu,
Ryuma Shimizu,
Kurumi Umemura,
Kenji Tsuji,
Hirohiko Shimizu,
Yuta Michimura,
Seiji Kawamura
Abstract:
For further gravitational wave (GW) detections, it is significant to invent a technique to reduce all kinds of mirror displacement noise dominant at low frequencies for ground-based detectors. The neutron displacement-noise-free interferometer (DFI) is one of the tools to reduce all the mirror displacement noise at lower frequencies. In this paper, we describe a further simplified configuration of…
▽ More
For further gravitational wave (GW) detections, it is significant to invent a technique to reduce all kinds of mirror displacement noise dominant at low frequencies for ground-based detectors. The neutron displacement-noise-free interferometer (DFI) is one of the tools to reduce all the mirror displacement noise at lower frequencies. In this paper, we describe a further simplified configuration of a neutron DFI in terms of neutron incidence direction. In the new configuration, neutrons enter the interferometer with unidirectional incidence at four speeds as opposed to two bidirectional incidences of opposite directions at two speeds as reported previously. This simplification of the neutron DFI is significant for proof-of-principle experiments.
△ Less
Submitted 1 November, 2022;
originally announced November 2022.
-
On proving consistency of equational theories in Bounded Arithmetic
Authors:
Arnold Beckmann,
Yoriyuki Yamagata
Abstract:
We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory $S^1_2$ proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independ…
▽ More
We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory $S^1_2$ proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.
△ Less
Submitted 9 March, 2022;
originally announced March 2022.
-
Assessment of waterfront office redevelopment plan on optimal building energy demand and rooftop photovoltaics for urban decarbonization
Authors:
Younghun Choi,
Takuro Kobashi,
Yoshiki Yamagata,
Akito Murayama
Abstract:
Designing waterfront redevelopment generally focuses on attractiveness, leisure, and beauty, resulting in various types of building and block shapes with limited considerations on environmental aspects. However, increasing climate change impacts necessitate these buildings to be sustainable, resilient, and zero CO2 emissions. By producing five scenarios (plus existing buildings) with constant floo…
▽ More
Designing waterfront redevelopment generally focuses on attractiveness, leisure, and beauty, resulting in various types of building and block shapes with limited considerations on environmental aspects. However, increasing climate change impacts necessitate these buildings to be sustainable, resilient, and zero CO2 emissions. By producing five scenarios (plus existing buildings) with constant floor areas, we investigated how building and district form with building integrated photovoltaics (BIPV) affect energy consumption and production, self-sufficiency, CO2 emission, and energy costs in the context of waterfront redevelopment in Tokyo. From estimated hourly electricity demands of the buildings, techno-economic analyses are conducted for rooftop PV systems for 2018 and 2030 with declining costs of rooftop PV systems. We found that environmental building designs with rooftop PV system are increasingly economical in Tokyo with CO2 emission reduction of 2-9% that depends on rooftop sizes. Payback periods drop from 14 years in 2018 to 6 years in 2030. Toward net-zero CO2 emissions by 2050, immediate actions are necessary to install rooftop PVs on existing and new buildings with energy efficiency improvements by construction industry and building owners. To facilitate such actions, national and local governments need to adopt appropriate policies.
△ Less
Submitted 20 August, 2021;
originally announced August 2021.
-
Deeply decarbonizing residential and urban central districts through photovoltaics plus electric vehicle applications
Authors:
Takuro Kobashi,
Younghun Choi,
Yujiro Hirano,
Yoshiki Yamagata,
Kelvin Say
Abstract:
With the costs of renewable energy technologies declining, new forms of urban energy systems are emerging that can be established in a cost-effective way. The SolarEV City concept has been proposed that uses rooftop Photovoltaics (PV) to its maximum extent, combined with Electric Vehicle (EV) with bi-directional charging for energy storage. Urban environments consist of various areas, such as resi…
▽ More
With the costs of renewable energy technologies declining, new forms of urban energy systems are emerging that can be established in a cost-effective way. The SolarEV City concept has been proposed that uses rooftop Photovoltaics (PV) to its maximum extent, combined with Electric Vehicle (EV) with bi-directional charging for energy storage. Urban environments consist of various areas, such as residential and commercial districts, with different energy consumption patterns, building structures, and car parks. The cost effectiveness and decarbonization potentials of PV + EV and PV (+ battery) systems vary across these different urban environments and change over time as cost structures gradually shift. To evaluate these characteristics, we performed techno-economic analyses of PV, battery, and EV technologies for a residential area in Shinchi, Fukushima and the central commercial district of Kyoto, Japan between 2020 and 2040. We found that PV + EV and PV only systems in 2020 are already cost competitive relative to existing energy systems (grid electricity and gasoline car). In particular, the PV + EV system rapidly increases its economic advantage over time, particularly in the residential district which has larger PV capacity and EV battery storage relative to the size of energy demand. Electricity exchanges between neighbors (e.g., peer-to-peer or microgrid) further enhanced the economic value (net present value) and decarbonization potential of PV + EV systems up to 23 percent and 7 percent in 2030, respectively. These outcomes have important strategic implications for urban decarbonization over the coming decades.
△ Less
Submitted 7 May, 2021;
originally announced May 2021.
-
Pendellösung Interferometry Probes the Neutron Charge Radius, Lattice Dynamics, and Fifth Forces
Authors:
Benjamin Heacock,
Takuhiro Fujiie,
Robert W. Haun,
Albert Henins,
Katsuya Hirota,
Takuya Hosobata,
Michael G. Huber,
Masaaki Kitaguchi,
Dmitry A. Pushin,
Hirohiko Shimizu,
Masahiro Takeda,
Robert Valdillez,
Yutaka Yamagata,
Albert Young
Abstract:
Structure factors describe how incident radiation is scattered from materials such as silicon and germanium and characterize the physical interaction between the material and scattered particles. We use neutron pendellösung interferometry to make precision measurements of the (220) and (400) neutron-silicon structure factors, and achieve a factor of four improvement in the (111) structure factor u…
▽ More
Structure factors describe how incident radiation is scattered from materials such as silicon and germanium and characterize the physical interaction between the material and scattered particles. We use neutron pendellösung interferometry to make precision measurements of the (220) and (400) neutron-silicon structure factors, and achieve a factor of four improvement in the (111) structure factor uncertainty. These data provide measurements of the silicon Debye-Waller factor at room temperature and the mean square neutron charge radius $\langle r_n^2 \rangle = -0.1101 \pm 0.0089 \, \mathrm{fm}^2$. Combined with existing measurements of the Debye-Waller factor and charge radius, the measured structure factors also improve constraints on the strength of a Yukawa-modification to gravity by an order of magnitude over the 20 pm to 10 nm length scale range.
△ Less
Submitted 19 August, 2021; v1 submitted 9 March, 2021;
originally announced March 2021.
-
New high-sensitivity searches for neutrons converting into antineutrons and/or sterile neutrons at the European Spallation Source
Authors:
A. Addazi,
K. Anderson,
S. Ansell,
K. Babu,
J. Barrow,
D. V. Baxter,
P. M. Bentley,
Z. Berezhiani,
R. Bevilacqua,
C. Bohm,
G. Brooijmans,
J. Broussard,
R. Biondi,
B. Dev,
C. Crawford,
A. Dolgov,
K. Dunne,
P. Fierlinger,
M. R. Fitzsimmons,
A. Fomin,
M. Frost,
S. Gardner,
A. Galindo-Uribarri,
E. Golubeva,
S. Girmohanta
, et al. (70 additional authors not shown)
Abstract:
The violation of Baryon Number, $\mathcal{B}$, is an essential ingredient for the preferential creation of matter over antimatter needed to account for the observed baryon asymmetry in the universe. However, such a process has yet to be experimentally observed. The HIBEAM/NNBAR %experiment program is a proposed two-stage experiment at the European Spallation Source (ESS) to search for baryon numbe…
▽ More
The violation of Baryon Number, $\mathcal{B}$, is an essential ingredient for the preferential creation of matter over antimatter needed to account for the observed baryon asymmetry in the universe. However, such a process has yet to be experimentally observed. The HIBEAM/NNBAR %experiment program is a proposed two-stage experiment at the European Spallation Source (ESS) to search for baryon number violation. The program will include high-sensitivity searches for processes that violate baryon number by one or two units: free neutron-antineutron oscillation ($n\rightarrow \bar{n}$) via mixing, neutron-antineutron oscillation via regeneration from a sterile neutron state ($n\rightarrow [n',\bar{n}'] \rightarrow \bar{n}$), and neutron disappearance ($n\rightarrow n'$); the effective $Δ\mathcal{B}=0$ process of neutron regeneration ($n\rightarrow [n',\bar{n}'] \rightarrow n$) is also possible. The program can be used to discover and characterise mixing in the neutron, antineutron, and sterile neutron sectors. The experiment addresses topical open questions such as the origins of baryogenesis, the nature of dark matter, and is sensitive to scales of new physics substantially in excess of those available at colliders. A goal of the program is to open a discovery window to neutron conversion probabilities (sensitivities) by up to three orders of magnitude compared with previous searches. The opportunity to make such a leap in sensitivity tests should not be squandered. The experiment pulls together a diverse international team of physicists from the particle (collider and low energy) and nuclear physics communities, while also including specialists in neutronics and magnetics.
△ Less
Submitted 8 June, 2020;
originally announced June 2020.
-
Simultaneous estimation of the effective reproducing number and the detection rate of COVID-19
Authors:
Yoriyuki Yamagata
Abstract:
A major difficulty to estimate $R$ (the effective reproducing number) of COVID-19 is that most cases of COVID-19 infection are mild or asymptomatic, therefore true number of infection is difficult to determine. This paper estimates the daily change of $R$ and the detection rate simultaneously using a Bayesian model. The analysis using synthesized data shows that our model correctly estimates $R$ a…
▽ More
A major difficulty to estimate $R$ (the effective reproducing number) of COVID-19 is that most cases of COVID-19 infection are mild or asymptomatic, therefore true number of infection is difficult to determine. This paper estimates the daily change of $R$ and the detection rate simultaneously using a Bayesian model. The analysis using synthesized data shows that our model correctly estimates $R$ and detects a short-term shock of the detection rate. Then, we apply our model to data from several countries to evaluate the effectiveness of public healthcare measures. Our analysis focuses Japan, which employs a moderate measure to keep "social distance". The result indicates a downward trend and now $R$ becomes below $1$. Although our analysis is preliminary, this may suggest that a moderate policy still can prevent epidemic of COVID-19.
△ Less
Submitted 13 May, 2020; v1 submitted 1 May, 2020;
originally announced May 2020.
-
Spatiotemporal analysis of urban heatwaves using Tukey g-and-h random field models
Authors:
Daisuke Murakami,
Gareth W. Peters,
Tomoko Matsui,
Yoshiki Yamagata
Abstract:
The statistical quantification of temperature processes for the analysis of urban heat island (UHI) effects and local heat-waves is an increasingly important application domain in smart city dynamic modelling. This leads to the increased importance of real-time heatwave risk management on a fine-grained spatial resolution. This study attempts to analyze and develop new methods for modelling the sp…
▽ More
The statistical quantification of temperature processes for the analysis of urban heat island (UHI) effects and local heat-waves is an increasingly important application domain in smart city dynamic modelling. This leads to the increased importance of real-time heatwave risk management on a fine-grained spatial resolution. This study attempts to analyze and develop new methods for modelling the spatio-temporal behavior of ground temperatures. The developed models consider higher-order stochastic spatial properties such as skewness and kurtosis, which are key components for understanding and describing local temperature fluctuations and UHI's. The developed models are applied to the greater Tokyo metropolitan area for a detailed real-world data case study. The analysis also demonstrates how to statistically incorporate a variety of real data sets. This includes remotely sensed imagery and a variety of ground-based monitoring site data to build models linking city and urban covariates to air temperature. The air temperature models are then used to capture high-resolution spatial emulator outputs for ground surface temperature modelling. The main class of processes studied includes the Tukey g-and-h processes for capturing spatial and temporal aspects of heat processes in urban environments.
△ Less
Submitted 2 April, 2020;
originally announced April 2020.
-
Separation of bounded arithmetic using a consistency statement
Authors:
Yoriyuki Yamagata
Abstract:
This paper proves Buss's hierarchy of bounded arithmetics $S^1_2 \subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$ does not entirely collapse. More precisely, we prove that, for a certain $D$, $S^1_2 \subsetneq S^{2D+5}_2$ holds. Further, we can allow any finite set of true quantifier free formulas for the BASIC axioms of $S^1_2, S^2_2, \ldots$. By Takeuti's argument, this implies…
▽ More
This paper proves Buss's hierarchy of bounded arithmetics $S^1_2 \subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$ does not entirely collapse. More precisely, we prove that, for a certain $D$, $S^1_2 \subsetneq S^{2D+5}_2$ holds. Further, we can allow any finite set of true quantifier free formulas for the BASIC axioms of $S^1_2, S^2_2, \ldots$. By Takeuti's argument, this implies $\mathrm{P} \neq \mathrm{NP}$. Let $\mathbf{Ax}$ be a certain formulation of BASIC axioms. We prove that $S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ for sufficiently large $D$, while $S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ for a system $\mathrm{PV}^-_1(D)$, a fragment of the system $\mathrm{PV}^-_1$, induction free first order extension of Cook's $\mathrm{PV}$, of which proofs contain only formulas with less than $D$ connectives. $S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ is proved by straightforward adaption of the proof of $\mathrm{PV} \not\vdash \mathrm{Con}(\mathrm{PV}^-)$ by Buss and Ignjatović. $S^{2D+5}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$ is proved by $S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_q(D+2) + \mathbf{Ax})$, where $\mathrm{PV}^-_q$ is a quantifier-only extension of $\mathrm{PV}^-$. The later statement is proved by an extension of a technique used for Yamagata's proof of $S^2_2 \vdash \mathrm{Con}(\mathrm{PV}^-)$, in which a kind of satisfaction relation $\mathrm{Sat}$ is defined. By extending $\mathrm{Sat}$ to formulas with less than $D$-quantifiers, $S^{2D+3}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_q(D) + \mathbf{Ax})$ is obtained in a straightforward way.
△ Less
Submitted 30 October, 2019; v1 submitted 14 April, 2019;
originally announced April 2019.
-
Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Authors:
Takumi Akazaki,
Shuang Liu,
Yoriyuki Yamagata,
Yihai Duan,
Jianye Hao
Abstract:
With the rapid development of software and distributed computing, Cyber-Physical Systems (CPS) are widely adopted in many application areas, e.g., smart grid, autonomous automobile. It is difficult to detect defects in CPS models due to the complexities involved in the software and physical systems. To find defects in CPS models efficiently, robustness guided falsification of CPS is introduced. Ex…
▽ More
With the rapid development of software and distributed computing, Cyber-Physical Systems (CPS) are widely adopted in many application areas, e.g., smart grid, autonomous automobile. It is difficult to detect defects in CPS models due to the complexities involved in the software and physical systems. To find defects in CPS models efficiently, robustness guided falsification of CPS is introduced. Existing methods use several optimization techniques to generate counterexamples, which falsify the given properties of a CPS. However those methods may require a large number of simulation runs to find the counterexample and is far from practical. In this work, we explore state-of-the-art Deep Reinforcement Learning (DRL) techniques to reduce the number of simulation runs required to find such counterexamples. We report our method and the preliminary evaluation results.
△ Less
Submitted 1 May, 2018;
originally announced May 2018.
-
Anomaly Detection for a Water Treatment System Using Unsupervised Machine Learning
Authors:
Jun Inoue,
Yoriyuki Yamagata,
Yuqi Chen,
Christopher M. Poskitt,
Jun Sun
Abstract:
In this paper, we propose and evaluate the application of unsupervised machine learning to anomaly detection for a Cyber-Physical System (CPS). We compare two methods: Deep Neural Networks (DNN) adapted to time series data generated by a CPS, and one-class Support Vector Machines (SVM). These methods are evaluated against data from the Secure Water Treatment (SWaT) testbed, a scaled-down but fully…
▽ More
In this paper, we propose and evaluate the application of unsupervised machine learning to anomaly detection for a Cyber-Physical System (CPS). We compare two methods: Deep Neural Networks (DNN) adapted to time series data generated by a CPS, and one-class Support Vector Machines (SVM). These methods are evaluated against data from the Secure Water Treatment (SWaT) testbed, a scaled-down but fully operational raw water purification plant. For both methods, we first train detectors using a log generated by SWaT operating under normal conditions. Then, we evaluate the performance of both methods using a log generated by SWaT operating under 36 different attack scenarios. We find that our DNN generates fewer false positives than our one-class SVM while our SVM detects slightly more anomalies. Overall, our DNN has a slightly better F measure than our SVM. We discuss the characteristics of the DNN and one-class SVM used in this experiment, and compare the advantages and disadvantages of the two methods.
△ Less
Submitted 25 September, 2017; v1 submitted 15 September, 2017;
originally announced September 2017.
-
Operational Semantics of Process Monitors
Authors:
Jun Inoue,
Yoriyuki Yamagata
Abstract:
CSPe is a specification language for runtime monitors that can directly express concurrency in a bottom-up manner that composes the system from simpler, interacting components. It includes constructs to explicitly flag failures to the monitor, which unlike deadlocks and livelocks in conventional process algebras, propagate globally and aborts the whole system's execution. Although CSPe has a trace…
▽ More
CSPe is a specification language for runtime monitors that can directly express concurrency in a bottom-up manner that composes the system from simpler, interacting components. It includes constructs to explicitly flag failures to the monitor, which unlike deadlocks and livelocks in conventional process algebras, propagate globally and aborts the whole system's execution. Although CSPe has a trace semantics along with an implementation demonstrating acceptable performance, it lacks an operational semantics. An operational semantics is not only more accessible than trace semantics but also indispensable for ensuring the correctness of the implementation. Furthermore, a process algebra like CSPe admits multiple denotational semantics appropriate for different purposes, and an operational semantics is the basis for justifying such semantics' integrity and relevance. In this paper, we develop an SOS-style operational semantics for CSPe, which properly accounts for explicit failures and will serve as a basis for further study of its properties, its optimization, and its use in runtime verification.
△ Less
Submitted 15 May, 2017;
originally announced May 2017.
-
Log-based Anomaly Detection of CPS Using a Statistical Method
Authors:
Yoshiyuki Harada,
Yoriyuki Yamagata,
Osamu Mizuno,
Eun-Hye Choi
Abstract:
Detecting anomalies of a cyber physical system (CPS), which is a complex system consisting of both physical and software parts, is important because a CPS often operates autonomously in an unpredictable environment. However, because of the ever-changing nature and lack of a precise model for a CPS, detecting anomalies is still a challenging task. To address this problem, we propose applying an out…
▽ More
Detecting anomalies of a cyber physical system (CPS), which is a complex system consisting of both physical and software parts, is important because a CPS often operates autonomously in an unpredictable environment. However, because of the ever-changing nature and lack of a precise model for a CPS, detecting anomalies is still a challenging task. To address this problem, we propose applying an outlier detection method to a CPS log. By using a log obtained from an actual aquarium management system, we evaluated the effectiveness of our proposed method by analyzing outliers that it detected. By investigating the outliers with the developer of the system, we confirmed that some outliers indicate actual faults in the system. For example, our method detected failures of mutual exclusion in the control system that were unknown to the developer. Our method also detected transient losses of functionalities and unexpected reboots. On the other hand, our method did not detect anomalies that were too many and similar. In addition, our method reported rare but unproblematic concurrent combinations of operations as anomalies. Thus, our approach is effective at finding anomalies, but there is still room for improvement.
△ Less
Submitted 12 January, 2017;
originally announced January 2017.
-
Estimation of gridded population and GDP scenarios with spatially explicit statistical downscaling
Authors:
Daisuke Murakami,
Yoshiki Yamagata
Abstract:
This study downscales the population and gross domestic product (GDP) scenarios given under Shared Socioeconomic Pathways (SSPs) into 0.5-degree grids. Our downscale approach has the following features: (i) it explicitly considers spatial and socioeconomic interactions among cities; (ii) it utilizes auxiliary variables, including, road network and land cover; (iii) it endogenously estimates influe…
▽ More
This study downscales the population and gross domestic product (GDP) scenarios given under Shared Socioeconomic Pathways (SSPs) into 0.5-degree grids. Our downscale approach has the following features: (i) it explicitly considers spatial and socioeconomic interactions among cities; (ii) it utilizes auxiliary variables, including, road network and land cover; (iii) it endogenously estimates influence from each factor by a model ensemble approach; (iv) it allows us controlling urban shrinkage/dispersion depending on SSPs. It is confirmed that our downscaling results are consistent with scenario assumptions (e.g., concentration in SSP1 and dispersion in SSP3). Besides, while existing grid-level scenario tends to have overly-smoothed population distributions in non-urban areas, ours does not suffer from the problem, and captures difference in urban and non-urban areas in a more reasonable manner.
△ Less
Submitted 13 April, 2017; v1 submitted 27 October, 2016;
originally announced October 2016.
-
A Moran coefficient-based mixed effects approach to investigate spatially varying relationships
Authors:
Daisuke Murakami,
Takahiro Yoshida,
Hajime Seya,
Daniel A. Griffith,
Yoshiki Yamagata
Abstract:
This study develops a spatially varying coefficient model by extending the random effects eigenvector spatial filtering model. The developed model has the following properties: its coefficients are interpretable in terms of the Moran coefficient; each of its coefficients can have a different degree of spatial smoothness; and it yields a variant of a Bayesian spatially varying coefficient model. Al…
▽ More
This study develops a spatially varying coefficient model by extending the random effects eigenvector spatial filtering model. The developed model has the following properties: its coefficients are interpretable in terms of the Moran coefficient; each of its coefficients can have a different degree of spatial smoothness; and it yields a variant of a Bayesian spatially varying coefficient model. Also, parameter estimation of the model can be executed with a relatively small computationally burden. Results of a Monte Carlo simulation reveal that our model outperforms a conventional eigenvector spatial filtering (ESF) model and geographically weighted regression (GWR) models in terms of the accuracy of the coefficient estimates and computational time. We empirically apply our model to the hedonic land price analysis of flood risk in Japan.
△ Less
Submitted 10 August, 2016; v1 submitted 22 June, 2016;
originally announced June 2016.
-
A non-intrusive measurement technique applying CARS for concentration measurement in a gas mixing flow
Authors:
Ken Yamamoto,
Yuki Yamagata,
Madoka Moriya,
Reiko Kuriyama,
Yohei Sato
Abstract:
Coherent anti-Stokes Raman scattering (CARS) microscope system was built and applied to a non-intrusive gas concentration measurement of a mixing flow in a millimeter-scale channel. Carbon dioxide and nitrogen were chosen as test fluids and CARS signals from the fluids were generated by adjusting the wavelengths of the Pump and the Stokes beams. The generated CARS signals, whose wavelengths are di…
▽ More
Coherent anti-Stokes Raman scattering (CARS) microscope system was built and applied to a non-intrusive gas concentration measurement of a mixing flow in a millimeter-scale channel. Carbon dioxide and nitrogen were chosen as test fluids and CARS signals from the fluids were generated by adjusting the wavelengths of the Pump and the Stokes beams. The generated CARS signals, whose wavelengths are different from those of the Pump and the Stokes beams, were captured by an EM-CCD camera after filtering out the excitation beams. A calibration experiment was performed in order to confirm the applicability of the built-up CARS system by measuring the intensity of the CARS signal from known concentrations of the samples. After confirming that the measured CARS intensity was proportional to the second power of the concentrations as was theoretically predicted, the CARS intensities in the gas mixing flow channel were measured. Ten different measurement points were set and concentrations of both carbon dioxide and nitrogen at each point were obtained. Consequently, it was observed that the mixing of two fluids progressed as the measurement point moved downstream. The results show the applicability of CARS to the non-intrusive concentration measurement of gas flows without any preprocess such as gas absorption into liquid or solid.
△ Less
Submitted 5 August, 2015;
originally announced August 2015.
-
A spatiotemporal analysis of participatory sensing data "tweets" and extreme climate events toward real-time urban risk management
Authors:
Yoshiki Yamagata,
Daisuke Murakami,
Gareth W. Peters,
Tomoko Matsui
Abstract:
Real-time urban climate monitoring provides useful information that can be utilized to help monitor and adapt to extreme events, including urban heatwaves. Typical approaches to the monitoring of climate data include weather station monitoring and remote sensing. However, climate monitoring stations are very often distributed spatially in a sparse manner, and consequently, this has a significant i…
▽ More
Real-time urban climate monitoring provides useful information that can be utilized to help monitor and adapt to extreme events, including urban heatwaves. Typical approaches to the monitoring of climate data include weather station monitoring and remote sensing. However, climate monitoring stations are very often distributed spatially in a sparse manner, and consequently, this has a significant impact on the ability to reveal exposure risks due to extreme climates at an intra-urban scale. Additionally, traditional remote sensing data sources are typically not received and analyzed in real-time which is often required for adaptive urban management of climate extremes, such as sudden heatwaves. Fortunately, recent social media, such as Twitter, furnishes real-time and high-resolution spatial information that might be useful for climate condition estimation. The objective of this study is utilizing geo-tagged tweets (participatory sensing data) for urban temperature analysis. We first detect tweets relating hotness (hot-tweets). Then, we study relationships between monitored temperatures and hot-tweets via a statistical model framework based on copula modelling methods. We demonstrate that there are strong relationships between "hot-tweets" and temperatures recorded at an intra-urban scale. Subsequently, we then investigate the application of "hot-tweets" informing spatio-temporal Gaussian process interpolation of temperatures as an application example of "hot-tweets". We utilize a combination of spatially sparse weather monitoring sensor data and spatially and temporally dense lower quality twitter data. Here, a spatial best linear unbiased estimation technique is applied. The result suggests that tweets provide some useful auxiliary information for urban climate assessment. Lastly, effectiveness of tweets toward a real-time urban risk management is discussed based on the results.
△ Less
Submitted 17 September, 2015; v1 submitted 22 May, 2015;
originally announced May 2015.
-
Consistency proof of a fragment of PV with substitution in bounded arithmetic
Authors:
Yoriyuki Yamagata
Abstract:
This paper presents proof that Buss's $S^2_2$ can prove the consistency of a fragment of Cook and Urquhart's $\mathrm{PV}$ from which induction has been removed but substitution has been retained.
This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic $S^1_2$.
Our proof relies on the notion of "computation" of the terms…
▽ More
This paper presents proof that Buss's $S^2_2$ can prove the consistency of a fragment of Cook and Urquhart's $\mathrm{PV}$ from which induction has been removed but substitution has been retained.
This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic $S^1_2$.
Our proof relies on the notion of "computation" of the terms of $\mathrm{PV}$.
In our work, we first prove that, in the system under consideration, if an equation is proved and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively.
By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven.
This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of $\mathrm{PV}$ without induction but with substitution in Buss's $S^1_2$.
However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours.
On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies.
△ Less
Submitted 24 December, 2018; v1 submitted 25 November, 2014;
originally announced November 2014.
-
Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking
Authors:
Ling Fang,
Yoriyuki Yamagata,
Yutaka Oiwa
Abstract:
If a Micro Processor Unit (MPU) receives an external electric signal as noise, the system function will freeze or malfunction easily. A new resilience strategy is implemented in order to reset the MPU automatically and stop the MPU from freezing or malfunctioning. The technique is useful for embedded systems which work in non-human environments. However, evaluating resilience strategies is difficu…
▽ More
If a Micro Processor Unit (MPU) receives an external electric signal as noise, the system function will freeze or malfunction easily. A new resilience strategy is implemented in order to reset the MPU automatically and stop the MPU from freezing or malfunctioning. The technique is useful for embedded systems which work in non-human environments. However, evaluating resilience strategies is difficult because their effectiveness depends on numerous, complex, interacting factors.
In this paper, we use probabilistic model checking to evaluate the embedded systems installed with the above mentioned new resilience strategy. Qualitative evaluations are implemented with 6 PCTL formulas, and quantitative evaluations use two kinds of evaluation. One is system failure reduction, and the other is ADT (Average Down Time), the industry standard. Our work demonstrates the benefits brought by the resilience strategy. Experimental results indicate that our evaluation is cost-effective and reliable.
△ Less
Submitted 5 May, 2014;
originally announced May 2014.
-
Bounded Arithmetic in Free Logic
Authors:
Yoriyuki Yamagata
Abstract:
One of the central open questions in bounded arithmetic is whether Buss' hierarchy of theories of bounded arithmetic collapses or not. In this paper, we reformulate Buss' theories using free logic and conjecture that such theories are easier to handle. To show this, we first prove that Buss' theories prove consistencies of induction-free fragments of our theories whose formulae have bounded compl…
▽ More
One of the central open questions in bounded arithmetic is whether Buss' hierarchy of theories of bounded arithmetic collapses or not. In this paper, we reformulate Buss' theories using free logic and conjecture that such theories are easier to handle. To show this, we first prove that Buss' theories prove consistencies of induction-free fragments of our theories whose formulae have bounded complexity. Next, we prove that although our theories are based on an apparently weaker logic, we can interpret theories in Buss' hierarchy by our theories using a simple translation. Finally, we investigate finitistic Gödel sentences in our systems in the hope of proving that a theory in a lower level of Buss' hierarchy cannot prove consistency of induction-free fragments of our theories whose formulae have higher complexity.
△ Less
Submitted 11 August, 2012; v1 submitted 18 January, 2012;
originally announced January 2012.
-
On Use of an Explicit Congruence Predicate in Bounded Arithmetic
Authors:
Yoriyuki Yamagata
Abstract:
We introduce system S^2_0E, a bounded arithmetic corresponding to Buss's S^2_0 with the predicate E which signifies the existence of the value. Then, we show that we can Σ^b_2-define truthness of S^2_0 E and therefore we can prove consistency of S^2_0 E in S^2_2. Finally, we conjecture that S^2_0 E + Σ^b_1-PIND interprets S^2_1.
We introduce system S^2_0E, a bounded arithmetic corresponding to Buss's S^2_0 with the predicate E which signifies the existence of the value. Then, we show that we can Σ^b_2-define truthness of S^2_0 E and therefore we can prove consistency of S^2_0 E in S^2_2. Finally, we conjecture that S^2_0 E + Σ^b_1-PIND interprets S^2_1.
△ Less
Submitted 2 April, 2009;
originally announced April 2009.
