Dr. Gopi Krishna Seemala, Researcher
Research Institute for Sustainable Humanosphere (RISH), Kyoto University
講演題目
GPS and Ionospheric studies
概要
This presentation will be a semi popular talk. The presentation gives some basic information about the Global Positioning System (GPS), a satellite based navigation system. How the GPS provides location information to the user anywhere on earth and then the current advances in navigation, their uses and the need. Then, the presentation will describe the role of GPS receivers in ionospheric research and the current research of the author in this field at RISH, Kyoto University.
The demand for higher data rate wireless communication has increased as wireless communication market has grown. Multiple input multiple output (MIMO) techniques are promising to increase throughput within a limited frequency band. The number of antennas in practical systems is increasing and it is expected that this increase will continue to satisfy the demand of high-speed transmission. When a transmitter has large amount of transmit antennas, precoding techniques using channel state information (CSI) between a transmitter and receiver increases the throughput. As CSI at the transmitter, the unitary matrix corresponding to signal space, which can be defined as eigenvectors or right singular vectors, is important. This talk presents unitary matrix utilization methods for wireless communication systems. The unitary matrices can be used for precoding techniques and channel estimation methods. Computer simulations show the effectiveness of the unitary matrix utilization methods.
Dr. Tetsuo Asano, Professor, School of Information Science, JAIST
講演題目
Designing Algorithms with Limited Work Space
概要
Recent progress in computer systems has provided programmers with virtually unlimited amount of work storage for their programs. This leads to space-inefficient programs that use too much storage and become too slow if sufficiently large memory is not available. Thus, I believe that space-efficient algorithms or memory-constrained algorithms deserve more attention. Constant-work-space algorithms have been extensively studied under a different name, log-space algorithms. Input data are given on a read-only array of $n$ elements, each having O(log n) bits, and work space is limited to O(log n) bits, in other words, a constant number of pointers and counters, each of O(log n) bits. This memory constraint in the log-space algorithms may be too severe for practice applications. For problems related to an image with n pixels, for example, it is quite reasonable to use work space of the order of square root of n, which amounts to a constant number of rows and columns. I will start my talk with a simple problem in this framework. Then, I will introduce some paradigms for designing such memory-constrained algorithms and their applications to interesting problems including those in computational geometry and computer vision.
Management techniques for the energy harvesting embedded system
概要
Energy-harvesting devices are materials that allow ambient energy sources to be converters into usable electrical power. While a battery powers the modern embedded systems, these energy-harvesting devices power the energy-harvesting embedded systems. This claims a new energy efficient management techniques for the energy-harvesting systems dislike the previous management techniques. In this talk, we will review the current management techniques for the energy harvesting embedded system.
科学データ国際事業「ICSU-WDS (World Data System）」をめぐる科学とデータと社会の関わり
A new international data activity ICSU-World Data System (WDS), and its perspective with science, data, and society
概要
近年、ビッグデータ等がしばしば騒がれるなか、科学の基盤としてデータの意味 が見直されつつある。科学と社会との信頼関係を維持するうえで、オープンな証 拠の提示と合理的議論は不可欠である。実験室で再確認できない現象、地球環境 などの自然現象においてはとくに、科学的発見の証拠・根拠として、論文および オープンなデータが必要であるという国際的な議論が行われている。しかし科学 情報の共有手段として、印刷物と比べれば電子メディアの歴史は浅い。2008年、 ICSU（国際科学会議；International Council for Science。1931年発足）は過 去50年以上の蓄積をもとに新たな組織World Data System（WDS）を発足して、長 期的なデータ保全活動等や自然科学・人文社会科学まで分野の偏らない新たなデー タ相互利用システム・流通体制の実現を目指した活動をすすめている。
With a growing interest in data explosion and advancing information technology, the meaning of “data” as the infrastructure of science is being changed. In the international community open sharing of data as well as open access of scholarly research papers are being discussed as crucial components of science. These are important for maintaining trust of science in society, especially for researches of phenomena irreproducible in an laboratory experiment such as the global environment and huge tsunamis for example. ICSU (International Council for Science) has reformed data-related organizations with their >50-year legacy to start a new body ICSU-World Data System (WDS) in 2008. WDS’s objectives includes long-term preservation of scientific data, and interoperable distributed data exchanges on a multidisciplinary basis including social sciences and humanities
Prof. Kohei Suenaga, Associate professor, Kyoto University
講演題目
Formal verification — from software to hybrid systems
概要
We are living in the world that consists of many systems: mechanical systems, electrical systems, computer systems, and so on. Failure of such systems may cause damage; it sometimes costs even lives. Ensuring correctness of a system is an important issue. To this end, various techniques have been studied and used.
Formal verification is one of such techniques. It ensures the correctness of a system by mathematically proving the correctness. Such mathematical proof gives a strong evidence of the correctness.
This talk is intended to be an introduction to formal verification, especially formal verification for software. Because formal verification for software deals with mathematically modeled software, I begin this talk by introducing what it is like to model software mathematically; then, I will pick up one software verification technique as an example: Hoare logic, a logic for reasoning properties of a program.
As an interesting application of software verification, I will also talk about my recent research topic: application of software verification to hybrid systems — systems that exhibit both discrete behavior and continuous behavior — by using nonstandard analysis. In this work, We add a constant “dt” that represents an infinitesimal (i.e., infinitely small) value to a standard programming language and Hoare logic. The outcome is a framework for modeling and verification of hybrid systems. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete. This is a joint work with Ichiro Hasuo at the University of Tokyo.
Prof. Takayuki Nishio, Assistant Professor, Graduate school of Informatics, Kyoto University
講演題目
Heterogeneous Resource Sharing for Mobile Cloud Computing
概要
The recent uptake of cloud computing platforms and mobile devices is converging into mobile cloud computing, which is a new paradigm for mobile applications and services that promises to have a strong impact on our lives. Fog computing is expected to be an enabler of the mobile cloud computing, which extends the cloud computing paradigm to the edge of the network. In the mobile cloud, not only central data centers but also pervasive mobile devices share their heterogeneous resources (e. g. CPUs, bandwidth, content) and support services. The mobile cloud based on such resource sharing is expected to be a powerful platform for mobile cloud applications and services. In this talk, I will introduce a frontier of mobile cloud and research issues. I will briefly introduce an architecture and mathematical frameworks for heterogeneous resource sharing toward the mobile cloud.