LONov 14, 2023
Completeness of Tableau Calculi for Two-Dimensional Hybrid LogicsYuki Nishimura
Hybrid logic is one of the extensions of modal logic. The many-dimensional product of hybrid logic is called hybrid product logic (HPL). We construct a sound and complete tableau calculus for two-dimensional HPL. Also, we made a tableau calculus for hybrid dependent product logic (HdPL), where one dimension depends on the other. In addition, we add a special rule to the tableau calculus for HdPL and show that it is still sound and complete. All of them lack termination, however.
62.2SYMar 30
Stochastic Safety-critical Control Compensating Safety Probability for Marine Vessel TrackingToo Matsuo, Yuki Nishimura, Kenta Hoshino et al.
A marine vessel is a nonlinear system subject to irregular disturbances such as wind and waves, which cause tracking errors between the nominal and actual trajectories. In this study, a nonlinear vessel maneuvering model that includes a tracking controller is formulated and then controlled using a linear approximation around the nominal trajectory. The resulting stochastic linearized system is analyzed using a stochastic zeroing control barrier function (ZCBF). A stochastic safety compensator is designed to ensure probabilistic safety, and its effectiveness is verified through numerical simulations.
16.2SYMar 30
Collision Avoidance Control for a Two-wheeled Vehicle under Stochastic Vibration using an Almost Sure Control Barrier FunctionTaichi Arimura, Yuki Nishimura, Taichi Ikezaki et al.
In recent years, many control problems of autonomous mobile robots have been developed. In particular, the robots are required to be safe; that is, they need to be controlled to avoid colliding with people or objects while traveling. In addition, since safety should be ensured even under irregular disturbances, the control for safety is required to be effective for stochastic systems. In this study, we design an almost sure safety-critical control law, which ensures safety with probability one, for a two-wheeled vehicle based on the stochastic control barrier function approach. In the procedure, we also consider a system model using the relative distance measured by a 2D LiDAR. The validity of the proposed control scheme is confirmed by experiments of a collision avoidance problem for a two-wheeled vehicle under vibration.
4.9LOMar 16
Terminating Hybrid Tableaus for Ordered ModelsYuki Nishimura
Hybrid logic extends modal logic with special propositions called nominals, each of which is true at only one state in a model. This enables us to describe some properties of binary relations, such as irreflexivity and anti-symmetry, which are essential to treat partial orders. We present terminating tableau calculi complete with respect to models whose accessibility relations are strictly partially ordered, unbounded strictly partially ordered, and partially ordered.
SYSep 8, 2015
Stabilization by Unbounded-Variation NoisesYuki Nishimura
In this paper, we claim the availability of deterministic noises for stabilization of the origins of dynamical systems, provided that the noises have unbounded variations. To achieve the result, we first consider the system representations based on rough path analysis; then, we provide the notion of asymptotic stability in roughness to analyze the stability for the systems. In the procedure, we also confirm that the system representations include stochastic differential equations; we also found that asymptotic stability in roughness is the same property as uniform almost sure asymptotic stability provided by Bardi and Cesaroni. After the discussion, we confirm that there is a case that deterministic noises are capable of making the origin become asymptotically stable in roughness while stochastic noises do not achieve the same stabilization results.