Author name cluster

Naoki Kobayashi

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

NeurIPS Conference 2025 Conference Paper

Learning Simple Interpolants for Linear Integer Arithmetic

Minchao Wu
Naoki Kobayashi

Craig interpolation plays a central role in formal verification tasks such as model checking, invariant generation, and abstraction refinement. In the domain of linear integer arithmetic (LIA), interpolants are crucial for deriving inductive invariants that characterize unreachable or safe program states, enabling scalable and precise reasoning about software and hardware correctness. Despite progress in interpolation algorithms, generating concise and interpretable interpolants remains a key challenge. We propose a lightweight learning-based approach to generating simple interpolants for LIA. Our model learns to lazily sample input problems directly and is complementary to existing logical methods. When Z3 is guided by our learned model, the complexity of the interpolants it produces can be reduced by up to 47. 3%. For older solvers, the reduction rate can reach up to 69. 1%.

PDF Details

IROS Conference 2022 Conference Paper

Integration of Variable-height and Hopping Strategies for Humanoid Push Recovery

Ko Yamamoto 0001
Naoki Kobayashi
Taiki Ishigaki
Yuichi Sakemi

In this study, we present a framework to en-sure seamless transition in humanoid push recovery involving hopping strategy. We propose a method to adaptively change the time constant that integrated the ankle strategy and variable height strategy. This framework excites a hopping motion against a large disturbance, which provides a seamless transition from the variable height to the hopping strategies. We analyze the applicable region of each strategy based on the simplified model. Moreover, we show that the hopping strategy prevents falling through whole-body dynamic simulations.

Details

AAAI Conference 2020 Conference Paper

Top-Down RST Parsing Utilizing Granularity Levels in Documents

Naoki Kobayashi
Tsutomu Hirao
Hidetaka Kamigaito
Manabu Okumura
Masaaki Nagata

Some downstream NLP tasks exploit discourse dependency trees converted from RST trees. To obtain better discourse dependency trees, we need to improve the accuracy of RST trees at the upper parts of the structures. Thus, we propose a novel neural top-down RST parsing method. Then, we exploit three levels of granularity in a document, paragraphs, sentences and Elementary Discourse Units (EDUs), to parse a document accurately and efﬁciently. The parsing is done in a top-down manner for each granularity level, by recursively splitting a larger text span into two smaller ones while predicting nuclearity and relation labels for the divided spans. The results on the RST-DT corpus show that our method achieved the state-of-the-art results, 87. 0 unlabeled span score, 74. 6 nuclearity labeled span score, and the comparable result with the state-of-the-art, 60. 0 relation labeled span score. Furthermore, discourse dependency trees converted from our RST trees also achieved the state-of-the-art results, 64. 9 unlabeled attachment score and 48. 5 labeled attachment score.

PDF Details

TCS Journal 2019 Journal Article

Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable

Naoki Kobayashi

In 1970's, Nivat studied recursive program schemes (a. k. a order-1 higher-order recursion schemes in modern terminology), first-order tree grammars for generating possibly infinite trees. We consider the inclusion problem between the frontier language of a non-deterministic recursive program scheme (equivalently, an order-2 word language or indexed language) and the Dyck language, and prove that it is undecidable by a reduction from the undecidability of Hilbert's 10th problem. Essentially the same result has recently been proved by Uezato and Minamide, but our proof is arguably more direct, demonstrating the expressive power of higher-order grammars.

Details DOI

I&C Journal 2017 Journal Article

Deadlock analysis of unbounded process networks

Naoki Kobayashi
Cosimo Laneve

Deadlock detection in concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale. To enable the analysis of such programs, (1) we define an algorithm for detecting deadlocks of a basic model featuring recursion and fresh name generation: the lam programs, and (2) we design a type system for value-passing CCS that returns lam programs. We show the soundness of the type system, and develop a type inference algorithm for it. The resulting algorithm is able to check deadlock-freedom of programs that cannot be handled by previous analyses, such as those that build unbounded networks.

Details DOI

I&C Journal 2009 Journal Article

Undecidable equivalences for basic parallel processes

Hans Hüttel
Naoki Kobayashi
Takashi Suto

The trace equivalence of BPP was shown to be undecidable by Hirshfeld. We show that all the preorders and equivalences except bisimulation in Glabbeek’s linear time-branching time spectrum are undecidable for BPP. The results are obtained by extending Hirshfeld’s encoding of Minsky machines into BPP. We also show that those preorders and equivalences are undecidable even for a restriction of BPP to 2-labels.

Details DOI

TCS Journal 2004 Journal Article

A generic type system for the Pi-calculus

Atsushi Igarashi
Naoki Kobayashi

We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express types and type environments as abstract processes: We can check various properties of a process by checking the corresponding properties of its type environment. The framework clarifies the essence of recent complex type systems, and it also enables sharing of a large amount of work such as a proof of type preservation, making it easy to develop new type systems.

Details DOI

I&C Journal 2002 Journal Article

A Type System for Lock-Free Processes

Naoki Kobayashi

Advanced type systems for the π-calculus have recently been proposed to guarantee deadlock-freedom in the sense that certain communications will eventually succeed unless the whole process diverges. Although such guarantees are useful for reasoning about the behavior of concurrent programs, there still remains the weakness that the success of a communication is not completely guaranteed due to the possibility of divergence. For example, although a server process that has received a request message cannot discard the request, it is allowed to infinitely delegate the request to other processes, causing a livelock. In this paper, we present a type system which guarantees that certain communications will eventually succeed under fair scheduling, regardless of whether processes diverge. We also present a variant of the type system which guarantees that a communication will succeed within a given number of reduction steps.

Details DOI

I&C Journal 2000 Journal Article

Type Reconstruction for Linear π-Calculus with I/O Subtyping

Atsushi Igarashi
Naoki Kobayashi

Powerful concurrency primitives in recent concurrent languages and thread libraries provide great flexibility about implementation of high-level features like concurrent objects. However, they are so low-level that they often make it difficult to check global correctness of programs or to perform nontrivial code optimization, such as elimination of redundant communication. In order to overcome those problems, advanced type systems for input-only/output-only channels and linear (use-once) channels have been recently studied, but the type reconstruction problem for those type systems remained open, and therefore, their applications to concurrent programming languages have been limited. In this paper, we develop type reconstruction algorithms for variants of Kobayashi, Pierce, and Turner's linear channel type system with Pierce and Sangiorgi's subtyping based on input-only/output-only channel types and prove correctness of the algorithms. To our knowledge, no complete type reconstruction algorithm has been previously known for those type systems. We have implemented one of the algorithms and incorporated it into the compiler of the concurrent language HACL. This paper also shows some experimental results on the algorithm and its application to compile-time optimizations.

Details DOI

TCS Journal 1999 Journal Article

Distributed concurrent linear logic programming

Naoki Kobayashi
Toshihiro Shimizu
Akinori Yonezawa

We propose a framework of distributed concurrent linear logic programming, which can elegantly capture the essential features of distributed computation: location-dependence/independence of names and movement of computation. We first define the syntax and semantics of a modal linear logic that is suitable for expressing distributed computation, and then show that there is a close relationship between formulas of a fragment of the modal linear logic and distributed processes.

Details DOI