arXiv subjects

Yoriyuki Yamagata

Publications and source records attributed to Yoriyuki Yamagata.

13 recordsLinked to original sources

arXiv2024

On the Metric Temporal Logic for Continuous Stochastic Processes

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.

cs.LO↗

arXiv2023

Notion of validity for the bilateral classical logic

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.

math.LO↗

arXiv2022

On proving consistency of equational theories in Bounded Arithmetic

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.

math.LO↗

arXiv2020

Simultaneous estimation of the effective reproducing number and the detection rate of COVID-19

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.

physics.soc-ph↗

arXiv2019

Separation of bounded arithmetic using a consistency statement

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.

math.LO↗

arXiv2018

Consistency proof of a fragment of PV with substitution in bounded arithmetic

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.

math.LO↗

arXiv2018

Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning

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.

cs.SE↗

arXiv2017

Anomaly Detection for a Water Treatment System Using Unsupervised Machine Learning

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.

cs.LG↗

arXiv2017

Operational Semantics of Process Monitors

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.

cs.PL↗

arXiv2017

Log-based Anomaly Detection of CPS Using a Statistical Method

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.

cs.SE↗

arXiv2014

Evaluation of A Resilience Embedded System Using Probabilistic Model-Checking

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.

cs.SE↗

arXiv2012

Bounded Arithmetic in Free Logic

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.

math.LO↗

arXiv2009

On Use of an Explicit Congruence Predicate in Bounded Arithmetic

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.

math.LO↗