7 Search Results for "Asada, Kazuyuki"

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.6
Causally Deterministic Markov Decision Processes

Authors: S. Akshay, Tobias Meggendorfer, and P. S. Thiagarajan

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Probabilistic systems are often modeled using factored versions of Markov decision processes (MDPs), where the states are composed out of the local states of components and each transition involves only a small subset of the components. Concurrency arises naturally in such systems. Our goal is to exploit concurrency when analyzing factored MDPs (FMDPs). To do so, we first formulate FMDPs in a way that aids this goal and port several notions from concurrency theory to the probabilistic setting of MDPs. In particular, we provide a concurrent semantics for FMDPs based on the classical notion of event structures, thereby cleanly separating causality, concurrency, and conflicts that arise from stochastic choices. We further identify the subclass of causally deterministic FMDPs (CMDPs), where non-determinism arises solely due to concurrency. Using our event structure semantics, we show that in CMDPs, local reachability properties can be computed using a "greedy" strategy. Finally, we implement our ideas in a prototype and apply it to four models, confirming the potential for substantial improvements over state-of-the-art methods.
Cite as

S. Akshay, Tobias Meggendorfer, and P. S. Thiagarajan. Causally Deterministic Markov Decision Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.6,
  author =	{Akshay, S. and Meggendorfer, Tobias and Thiagarajan, P. S.},
  title =	{{Causally Deterministic Markov Decision Processes}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.6},
  URN =		{urn:nbn:de:0030-drops-207781},
  doi =		{10.4230/LIPIcs.CONCUR.2024.6},
  annote =	{Keywords: MDPs, distribution, causal determinism}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.29
Böhm and Taylor for All!

Authors: Aloÿs Dufour and Damiano Mazza

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction.
Cite as

Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for All!. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dufour_et_al:LIPIcs.FSCD.2024.29,
  author =	{Dufour, Alo\"{y}s and Mazza, Damiano},
  title =	{{B\"{o}hm and Taylor for All!}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.29},
  URN =		{urn:nbn:de:0030-drops-203582},
  doi =		{10.4230/LIPIcs.FSCD.2024.29},
  annote =	{Keywords: Linear logic, Differential linear logic, Taylor expansion of lambda-terms, B\"{o}hm trees, Process calculi}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.21
On Average-Case Hardness of Higher-Order Model Checking

Authors: Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We study a mixture between the average case and worst case complexities of higher-order model checking, the problem of deciding whether the tree generated by a given λ Y-term (or equivalently, a higher-order recursion scheme) satisfies the property expressed by a given tree automaton. Higher-order model checking has recently been studied extensively in the context of higher-order program verification. Although the worst-case complexity of the problem is k-EXPTIME complete for order-k terms, various higher-order model checkers have been developed that run efficiently for typical inputs, and program verification tools have been constructed on top of them. One may, therefore, hope that higher-order model checking can be solved efficiently in the average case, despite the worst-case complexity. We provide a negative result, by showing that, under certain assumptions, for almost every term, the higher-order model checking problem specialized for the term is k-EXPTIME hard with respect to the size of automata. The proof is based on a novel intersection type system that characterizes terms that do not contain any useless subterms.
Cite as

Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada. On Average-Case Hardness of Higher-Order Model Checking. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nakamura_et_al:LIPIcs.FSCD.2020.21,
  author =	{Nakamura, Yoshiki and Asada, Kazuyuki and Kobayashi, Naoki and Sin'ya, Ryoma and Tsukada, Takeshi},
  title =	{{On Average-Case Hardness of Higher-Order Model Checking}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.21},
  URN =		{urn:nbn:de:0030-drops-123439},
  doi =		{10.4230/LIPIcs.FSCD.2020.21},
  annote =	{Keywords: Higher-order model checking, average-case complexity, intersection type system}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.22
Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars

Authors: Kazuyuki Asada and Naoki Kobayashi

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Higher-order grammars have recently been studied actively in the context of automated verification of higher-order programs. Asada and Kobayashi have previously shown that, for any order-(n+1) word grammar, there exists an order-n grammar whose frontier language coincides with the language generated by the word grammar. Their translation, however, blows up the size of the grammar, which inhibited complexity-preserving reductions from decision problems on word grammars to those on tree grammars. In this paper, we present a new translation from order-(n+1) word grammars to order-n tree grammars that is size-preserving in the sense that the size of the output tree grammar is polynomial in the size of an input tree grammar. The new translation and its correctness proof are arguably much simpler than the previous translation and proof.
Cite as

Kazuyuki Asada and Naoki Kobayashi. Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{asada_et_al:LIPIcs.FSCD.2020.22,
  author =	{Asada, Kazuyuki and Kobayashi, Naoki},
  title =	{{Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{22:1--22:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.22},
  URN =		{urn:nbn:de:0030-drops-123440},
  doi =		{10.4230/LIPIcs.FSCD.2020.22},
  annote =	{Keywords: higher-order grammar, word language, tree language, complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.14
Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered

Authors: Kazuyuki Asada and Naoki Kobayashi

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Asada and Kobayashi [ICALP 2017] conjectured a higher-order version of Kruskal's tree theorem, and proved a pumping lemma for higher-order languages modulo the conjecture. The conjecture has been proved up to order-2, which implies that Asada and Kobayashi's pumping lemma holds for order-2 tree languages, but remains open for order-3 or higher. In this paper, we prove a variation of the conjecture for order-3. This is sufficient for proving that a variation of the pumping lemma holds for order-3 tree languages (equivalently, for order-4 word languages).
Cite as

Kazuyuki Asada and Naoki Kobayashi. Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{asada_et_al:LIPIcs.FSTTCS.2018.14,
  author =	{Asada, Kazuyuki and Kobayashi, Naoki},
  title =	{{Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.14},
  URN =		{urn:nbn:de:0030-drops-99138},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.14},
  annote =	{Keywords: higher-order grammar, pumping lemma, Kruskal's tree theorem, well-quasi-ordering, simply-typed lambda calculus}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.97
Pumping Lemma for Higher-order Languages

Authors: Kazuyuki Asada and Naoki Kobayashi

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We study a pumping lemma for the word/tree languages generated by higher-order grammars. Pumping lemmas are known up to order-2 word languages (i.e., for regular/context-free/indexed languages), and have been used to show that a given language does not belong to the classes of regular/context-free/indexed languages. We prove a pumping lemma for word/tree languages of arbitrary orders, modulo a conjecture that a higher-order version of Kruskal's tree theorem holds. We also show that the conjecture indeed holds for the order-2 case, which yields a pumping lemma for order-2 tree languages and order-3 word languages.
Cite as

Kazuyuki Asada and Naoki Kobayashi. Pumping Lemma for Higher-order Languages. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 97:1-97:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{asada_et_al:LIPIcs.ICALP.2017.97,
  author =	{Asada, Kazuyuki and Kobayashi, Naoki},
  title =	{{Pumping Lemma for Higher-order Languages}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{97:1--97:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.97},
  URN =		{urn:nbn:de:0030-drops-74323},
  doi =		{10.4230/LIPIcs.ICALP.2017.97},
  annote =	{Keywords: pumping lemma, higher-order grammars, Kruskal's tree theorem}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.111
On Word and Frontier Languages of Unsafe Higher-Order Grammars

Authors: Kazuyuki Asada and Naoki Kobayashi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Higher-order grammars are an extension of regular and context-free grammars, where nonterminals may take parameters. They have been extensively studied in 1980's, and restudied recently in the context of model checking and program verification. We show that the class of unsafe order-(n+1) word languages coincides with the class of frontier languages of unsafe order-n tree languages. We use intersection types for transforming an order-(n+1) word grammar to a corresponding order-n tree grammar. The result has been proved for safe languages by Damm in 1982, but it has been open for unsafe languages, to our knowledge. Various known results on higher-order grammars can be obtained as almost immediate corollaries of our result.
Cite as

Kazuyuki Asada and Naoki Kobayashi. On Word and Frontier Languages of Unsafe Higher-Order Grammars. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 111:1-111:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{asada_et_al:LIPIcs.ICALP.2016.111,
  author =	{Asada, Kazuyuki and Kobayashi, Naoki},
  title =	{{On Word and Frontier Languages of Unsafe Higher-Order Grammars}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{111:1--111:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.111},
  URN =		{urn:nbn:de:0030-drops-62469},
  doi =		{10.4230/LIPIcs.ICALP.2016.111},
  annote =	{Keywords: intersection types, higher-order grammars}
}
  • Refine by Author
  • 5 Asada, Kazuyuki
  • 5 Kobayashi, Naoki
  • 1 Akshay, S.
  • 1 Dufour, Aloÿs
  • 1 Mazza, Damiano
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Lambda calculus
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Linear logic
  • Show More...

  • Refine by Keyword
  • 2 Kruskal's tree theorem
  • 2 higher-order grammar
  • 2 higher-order grammars
  • 2 pumping lemma
  • 1 Böhm trees
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 2 2020
  • 2 2024
  • 1 2016
  • 1 2017
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact