# Open Positions Announcement: Postdoctoral Researchers in Formal Methods and Control Theory for AI-Intensive Cyber-Physical Systems

## Overview

We are excited to announce the availability of three postdoctoral researcher positions within the "CyPhAI: Formal Analysis and Design of AI-intensive Cyber-Physical Systems" project. We seek to develop mathematically rigorous methodologies for the modeling, verification, testing, monitoring, and control of cyber-physical systems (CPS) where artificial intelligence (AI) plays a pivotal role. This pioneering project is a collaborative effort between Japan teams led by Prof. Kohei Suenaga (Kyoto University) and Prof. Masako Kishida (NII) and the France team led by Prof. Thao Dang (CNRS), emphasizing international collaboration and interdisciplinary research in AI-CPS.

In this project, you will help advance the research in formal methods and control theories for AI-CPS and closely work with the leading researchers in Japan, Prof. Kohei Suenaga at Kyoto University in Kyoto or Prof. Masako Kishida at the National Institute of Informatics (NII) in Tokyo. You will also have opportunities to participate in several annual project workshops held in France or Japan to collaborate with the France team as well as other Japan teams.

Candidates must have or be near the completion of a PhD with research in relevant fields and demonstrate a track record of research publications, conference presentations, and software programming skills. Research experience in interdisciplinary collaborations is highly valued. The positions are heavily research-oriented. Selected candidates will be expected to independently conduct research tasks including but not limited to the following:
- Propose and execute research plans
- Present progress and discuss with team members and collaborators regularly
- Prepare submissions to top-tier journals or conferences
- Promote our research outcome at international venues

We welcome applications from foreign (non-Japanese) nationals. This project is funded by the Core Research for Evolutionary Science and Technology (CREST) program from Japan Science and Technology Agency (JST). Positions are to be filled on a rolling basis with flexible start dates. The initial contract will end at March 2025 with the possibility of extension up to March 2026, when the project will conclude. Compensation is determined on the basis of your qualifications according to the employment regulations in Kyoto University or NII, with social insurances covered by the hiring institutions.

Compensation for successful candidate starts from 6M JPY/year before tax. (We would like to remark that living cost in Japan is quite low these days: Big-mac with fries and soda in McDonald's is 750 JPY; you can eat good ramen with 1000 JPY.)

## Position Descriptions

### 1. Two Postdoctoral Researchers in Formal Methods for AI-CPS
- **Workplace:** Onsite at Kyoto University, Kyoto, Japan
- **Qualifications:**
+ Must have or be near the completion of a PhD with research topics in verification and testing of software or hybrid systems, verification and testing of machine-learning systems, or reinforcement learning
+ Full Professional Proficiency in English
+ Strong programming skills in C++, MATLAB, OCaml, or Python
- **Recommended Skill:** Elementary Japanese to help your daily life
- **Principle Investigator**: Prof. Kohei Suenaga
- **Research Focus:** Formal methods applicable to AI-CPS and its application to real-world problems, including but not limited to ones related to our previous publications listed below:
+ [Junya Shijubo, Masaki Waga, Kohei Suenaga: Efficient Black-Box Checking via Model Checking with Strengthened Specifications. RV 2021: 100-120](https://arxiv.org/abs/2109.04656)
+ [Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga, Kohei Suenaga: Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption. CAV (1) 2022: 447-468](https://arxiv.org/abs/2206.03582)
+ [Atsushi Kikuchi, Kotaro Uchida, Masaki Waga, Kohei Suenaga: BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models. ACCV (7) 2022: 274-290](https://arxiv.org/abs/2210.17130)
+ [Amit Gurung, Masaki Waga, Kohei Suenaga: Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data. ATVA (1) 2023: 33-52](https://arxiv.org/abs/2301.03915)
+ [Junya Shijubo, Masaki Waga, Kohei Suenaga: Probabilistic Black-Box Checking via Active MDP Learning. ACM Trans. Embed. Comput. Syst. 22(5s): 148:1-148:26 (2023)](https://arxiv.org/abs/2308.07930)
+ [Étienne André, Masaki Waga, Natsuki Urabe, Ichiro Hasuo: Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior. NFM 2022: 470-488](https://arxiv.org/abs/2203.13247)
+ [Masaki Waga, Ezequiel Castellano, Sasinee Pruekprasert, Stefan Klikovits, Toru Takisaka, Ichiro Hasuo: Dynamic Shielding for Reinforcement Learning in Black-Box Environments. ATVA 2022: 25-41](https://arxiv.org/abs/2207.13446)
+ [Masaki Waga: Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. CAV (1) 2023: 3-26](https://arxiv.org/abs/2305.17742)

### 2. One Postdoctoral Researcher in Control for AI-CPS

- **Workplace:** Onsite at National Institute of Informatics, Tokyo, Japan
- **Qualifications:**
+ Must have or be near the completion of a PhD with research topics in control theory, learning-based control, or hybrid systems
+ Must have excellent verbal and written communication skills in English
+ Must be able to work independently
- **Recommended Skill:** Elementary Japanese to help your daily life
- **Principle Investigator**: Prof. Masako Kishida
- **Research Focus:** Towards controller designs using machine learning techniques and/or safe controller designs for systems with machine-learning-based components

## Application Process

Please send your application to `application-cyphai [at] fos.kuis.kyoto-u.ac.jp` with the subject "CREST Job Application". Your application must include:
- A brief CV,
- A list of your publications (A link to your dblp or Google Scholar profile will be sufficient.),
- Softcopies of your representative publications,
- Contact information for two references,
- For applicants to Kishida's group at NII: a short research proposal (at most one page including figures/illustrations).

We will reach out for further materials and interview arrangements if your application aligns with our project needs.

If you have questions regarding the positions, please send your inquiries to `application-cyphai [at] fos.kuis.kyoto-u.ac.jp` with the subject "CREST Job Inquiry".

###### tag: `CyPhAI`