Search

• < Previous
• 1
• Next >

---

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

Naoki Kobayashi ; C. -H. Luke Ong.

Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees generated by order-n recursion schemes is n-EXPTIME complete. We consider two subclasses of APT and investigate the&nbsp;[&hellip;]

---

Resource Usage Analysis for the Pi-Calculus

Naoki Kobayashi ; Kohei Suenaga ; Lucian Wischik.

We propose a type-based resource usage analysis for the &#960;-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a program accesses resources such as files and memory in a valid manner. Our type system is an extension of&nbsp;[&hellip;]

---

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence

Kazuyuki Asada ; Naoki Kobayashi ; Ryoma Sin'ya ; Takeshi Tsukada.

It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst&nbsp;[&hellip;]

---

On the Termination Problem for Probabilistic Higher-Order Recursive Programs

Naoki Kobayashi ; Ugo Dal Lago ; Charles Grellois.

In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study&nbsp;[&hellip;]

---

A Probabilistic Higher-order Fixpoint Logic

Yo Mitani ; Naoki Kobayashi ; Takeshi Tsukada.

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is strictly more expressive than the $\mu^p$-calculus, and that the PHFL&nbsp;[&hellip;]

---