5 Search Results for "Urabe, Natsuki"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.6
Omega-Regular Verification and Control for Distributional Specifications in MDPs

Authors: S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
A classical approach to studying Markov decision processes (MDPs) is to view them as state transformers. However, MDPs can also be viewed as distribution transformers, where an MDP under a strategy generates a sequence of probability distributions over MDP states. This view arises in several applications, even as the probabilistic model checking problem becomes much harder compared to the classical state transformer counterpart. It is known that even distributional reachability and safety problems become computationally intractable (Skolem- and positivity-hard). To address this challenge, recent works focused on sound but possibly incomplete methods for verification and control of MDPs under the distributional view. However, existing automated methods are applicable only to distributional reachability, safety and reach-avoidance specifications. In this work, we present the first automated method for verification and control of MDPs with respect to distributional omega-regular specifications. To achieve this, we propose a novel notion of distributional certificates, which are sound and complete proof rules for proving that an MDP under a distributionally memoryless strategy satisfies some distributional omega-regular specification. We then use our distributional certificates to design the first fully automated algorithms for verification and control of MDPs with respect to distributional omega-regular specifications. Our algorithms follow a template-based synthesis approach and provide soundness and relative completeness guarantees, while running in PSPACE. Our prototype implementation demonstrates practical applicability of our algorithms to challenging examples collected from the literature.
Cite as

S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić. Omega-Regular Verification and Control for Distributional Specifications in MDPs. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2025.6,
  author =	{Akshay, S. and Neysari, Ouldouz and \v{Z}ikeli\'{c}, Ðor{\d}e},
  title =	{{Omega-Regular Verification and Control for Distributional Specifications in MDPs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.6},
  URN =		{urn:nbn:de:0030-drops-239562},
  doi =		{10.4230/LIPIcs.CONCUR.2025.6},
  annote =	{Keywords: MDPs, Distributional objectives, \omega-regularity, Certificates}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.30
A Complete Inference System for Probabilistic Infinite Trace Equivalence

Authors: Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.
Cite as

Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova. A Complete Inference System for Probabilistic Infinite Trace Equivalence. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CSL.2025.30,
  author =	{C\^{i}rstea, Corina and Moss, Lawrence S. and Noquez, Victoria and Schmid, Todd and Silva, Alexandra and Sokolova, Ana},
  title =	{{A Complete Inference System for Probabilistic Infinite Trace Equivalence}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{30:1--30:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.30},
  URN =		{urn:nbn:de:0030-drops-227870},
  doi =		{10.4230/LIPIcs.CSL.2025.30},
  annote =	{Keywords: Coalgebra, infinite trace, semantics, logic, convex sets}
}
Document
Early Ideas
DOI: 10.4230/LIPIcs.CALCO.2021.21
Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)

Authors: Koko Muroya, Takahiro Sanada, and Natsuki Urabe

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We describe our ongoing work on generalizing some quantitatively constrained notions of weak simulation up-to that are recently introduced for deterministic systems modeling program execution. We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison between words using a preorder, instead of equality.
Cite as

Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{muroya_et_al:LIPIcs.CALCO.2021.21,
  author =	{Muroya, Koko and Sanada, Takahiro and Urabe, Natsuki},
  title =	{{Preorder-Constrained Simulation for Nondeterministic Automata}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{21:1--21:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio 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.CALCO.2021.21},
  URN =		{urn:nbn:de:0030-drops-153762},
  doi =		{10.4230/LIPIcs.CALCO.2021.21},
  annote =	{Keywords: simulation, weak simulation, up-to technique, language inclusion, preorder}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.24
Coalgebraic Trace Semantics for Buechi and Parity Automata

Authors: Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic notion in the theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's.
Cite as

Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic Trace Semantics for Buechi and Parity Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{urabe_et_al:LIPIcs.CONCUR.2016.24,
  author =	{Urabe, Natsuki and Shimizu, Shunsuke and Hasuo, Ichiro},
  title =	{{Coalgebraic Trace Semantics for Buechi and Parity Automata}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.24},
  URN =		{urn:nbn:de:0030-drops-61867},
  doi =		{10.4230/LIPIcs.CONCUR.2016.24},
  annote =	{Keywords: coalgebra, Buechi automaton, parity automaton, probabilistic automaton, tree automaton}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.320
Coalgebraic Infinite Traces and Kleisli Simulations

Authors: Natsuki Urabe and Ichiro Hasuo

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various types of systems. A generic categorical theory behind Kleisli simulation has been developed and it guarantees the soundness of those simulations wrt. finite trace semantics. Moreover, those simulations can be aided by forward partial execution (FPE) - a categorical transformation of systems previously introduced by the authors. In this paper, we give Kleisli simulation a theoretical foundation that assures its soundness also wrt. infinite trace. There, following Jacobs' work, infinite trace semantics is characterized as the "largest homomorphism." It turns out that soundness of forward simulations is rather straightforward; that of backward simulation holds too, although it requires certain additional conditions and its proof is more involved. We also show that FPE can be successfully employed in the infinite trace setting to enhance the applicability of Kleisli simulations as witnesses of trace inclusion. Our framework is parameterized in the monad for branching as well as in the functor for linear-time behaviors; for the former we use the powerset monad (for nondeterminism) as well as the sub-Giry monad (for probability).
Cite as

Natsuki Urabe and Ichiro Hasuo. Coalgebraic Infinite Traces and Kleisli Simulations. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 320-335, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{urabe_et_al:LIPIcs.CALCO.2015.320,
  author =	{Urabe, Natsuki and Hasuo, Ichiro},
  title =	{{Coalgebraic Infinite Traces and Kleisli Simulations}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{320--335},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.320},
  URN =		{urn:nbn:de:0030-drops-55424},
  doi =		{10.4230/LIPIcs.CALCO.2015.320},
  annote =	{Keywords: category theory, coalgebra, simulation, verification, trace semantics}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2021
  • 1 2016
  • 1 2015

  • Refine by Author
  • 3 Urabe, Natsuki
  • 2 Hasuo, Ichiro
  • 1 Akshay, S.
  • 1 Cîrstea, Corina
  • 1 Moss, Lawrence S.
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Verification by model checking
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic

  • Refine by Keyword
  • 2 coalgebra
  • 2 simulation
  • 1 Buechi automaton
  • 1 Certificates
  • 1 Coalgebra
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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