Natsuki Urabe（卜部 夏木）

I am a postdoctoral researcher at National Institute of Informatics, Japan.
My reserach interests are in the areas of category theory, coalgebras, quantitative systems, probabilistic systems and fixed-point logic.

Papers

• Natsuki Urabe and Rupak Majumdar.
  Verifying Asymptotic Temporal Properties of Continuous-State Probabilistic Systems.
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume 40, Number 9, 2021. [doi]
• Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe and Ichiro Hasuo.
  Ranking and Repulsing Supermartingales for Reachability in Randomized Programs.
  Extended version of [Takisaka, Oyabu, Urabe & Hasuo, ATVA 2018].
  ACM Transactions on Programming Languages and Systems, Volume 43, Number 2, 2021. [doi]
• Satoshi Kura, Natsuki Urabe and Ichiro Hasuo.
  Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments.
  Proc. TACAS 2019. [doi | arXiv]
• Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe and Ichiro Hasuo.
  Ranking and Repulsing Supermartingales for Approximating Reachability.
  Proc. ATVA 2018. [doi | arXiv (extended version with appendices)]
• Natsuki Urabe and Ichiro Hasuo.
  Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors.
  Proc. CMCS 2018. [doi | arXiv (extended version with appendices)]
• Natsuki Urabe and Ichiro Hasuo.
  Coalgebraic Infinite Traces and Kleisli Simulations.
  Extended version of [Urabe & Hasuo, CALCO 2015].
  Logical Methods in Computer Science, Volume 14, Issue 3, 2018. [doi | arXiv]
• Natsuki Urabe and Ichiro Hasuo.
  Fair Simulation for Nondeterministic and Probabilistic Büchi Automata: a Coalgebraic Perspective.
  Logical Methods in Computer Science, Volume 13, Issue 3, 2017. [doi | arXiv]
• Natsuki Urabe, Masaki Hara and Ichiro Hasuo.
  Categorical Liveness Checking by Corecursive Algebras.
  Proc. LICS 2017. [doi | arXiv (extended version with appendices)]
• Natsuki Urabe and Ichiro Hasuo.
  Quantitative Simulations by Matrices.
  Extended version of [Urabe & Hasuo, CONCUR 2014].
  Information and Computation, Volume 252, 2017. [doi]
  • implementations for plus-times, max-plus and plus-times tree weighted automata
• Natsuki Urabe, Shunsuke Shimizu and Ichiro Hasuo.
  Coalgebraic Trace Semantics for Büchi and Parity Automata.
  Proc. CONCUR 2016. [doi | arXiv (extended version with appendices)]
  
• Natsuki Urabe and Ichiro Hasuo.
  Coalgebraic Infinite Traces and Kleisli Simulations.
  Proc. CALCO 2015. [doi | arXiv (extended version)]
• Natsuki Urabe and Ichiro Hasuo.
  Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices.
  Proc. CONCUR 2014. [doi | pdf (extended version with appendices)]
  
  • implementation for plus-times semiring weighted automata
  • implementation for max-plus semiring weighted automata

Talks

• Preorder-Constrained Simulation (Early Idea).
  CALCO 2021, online/hybrid event from Salzburg, Austria. 2 Sep 2021. Slides: [key | pdf]
• Probabilistic Verification via Category Theory:
  Categorical Generalization of Fair Simulation and Ranking Function by Kleisli Coalgebras, and Its Concretization.
  PhD thesis presentation, University of Tokyo, Tokyo, Japan. 31 Jan 2019. Slides: [key | pdf]
  
• Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors.
  CMCS 2018, Thessaloniki, Greece. 14 Apr 2018. Slides: [key | pdf]
• Categorical Liveness Checking by Corecursive Algebras.
  LICS 2017, Reykjavik, Iceland. 21 Jun 2017. Slides: [key | pdf]
• Coalgebraic Trace Semantics for Büchi and Parity Automata.
  CONCUR 2016, Quebec City, Canada. 25 Aug 2016. Slides: [key | pdf]
• Extension of Kleisli Simulation to Infinite Traces.
  MSc thesis presentation, University of Tokyo, Tokyo, Japan. 1 Feb 2016. Slides: [key | pdf]
  
• Coalgebraic Infinite Traces and Kleisli Simulations.
  CALCO 2015, Nijmegen, the Netherlands. 26 Jun 2015. Slides: [key | pdf]
• Kleisli Simulation for Infinite Trace.
  CSCAT 2015, Kagoshima, Japan. 14 Mar 2015. Slides: [key | pdf]
• Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices.
  ALGI 25, Kanagawa, Japan. 19 Aug 2014.
  CONCUR 2014, Rome, Italy. 5 Sep 2014. Slides: [key | pdf]
• Kleisli Simulation for Real-Weighted Automata and its Algorithm.
  BSc thesis presentation, University of Tokyo, Tokyo, Japan. 12 Feb 2014. Slides: [key | pdf]
  CSCAT 2014, Kanagawa, Japan. 18 Mar 2014. Slides: [key | pdf]

Theses

• Natsuki Urabe.
  Probabilistic Verification via Category Theory:
  Categorical Generalization of Fair Simulation and Ranking Function by Kleisli Coalgebras, and Its Concretization.
  PhD thesis, University of Tokyo, 2019. [pdf]
• Natsuki Urabe.
  Extension of Kleisli Simulation to Infinite Traces.
  MSc thesis, University of Tokyo, 2016.
• Natsuki Urabe.
  Kleisli Simulation for Real-Weighted Automata and its Algorithm.
  BSc thesis, University of Tokyo, 2014.

Work History

• Postdoctral Researcher at National Institute of Informatics, Japan (June 2021 – present).
• Postdoctral Researcher at Max Planck Institute for Software Systems, Germany (May 2019 – May 2021).

Contact

• Office:
  • ERATO Hasuo Project, Palace Side Building 3F, Hitotsubashi 1-1-1, Tokyo 100-1003, Japan
• Email: