2 Search Results for "Gaiser, Andreas"

Document
DOI: 10.4230/LIPIcs.STACS.2010.2468
Computing Least Fixed Points of Probabilistic Systems of Polynomials

Authors: Javier Esparza, Andreas Gaiser, and Stefan Kiefer

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
We study systems of equations of the form $X_1 = f_1(X_1, \ldots, X_n), \ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with nonnegative coefficients that add up to~$1$. The least nonnegative solution, say~$\mu$, of such equation systems is central to problems from various areas, like physics, biology, computational linguistics and probabilistic program verification. We give a simple and strongly polynomial algorithm to decide whether $\mu=(1,\ldots,1)$ holds. Furthermore, we present an algorithm that computes reliable sequences of lower and upper bounds on~$\mu$, converging linearly to~$\mu$. Our algorithm has these features despite using inexact arithmetic for efficiency. We report on experiments that show the performance of our algorithms.
Cite as

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing Least Fixed Points of Probabilistic Systems of Polynomials. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 359-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.STACS.2010.2468,
  author =	{Esparza, Javier and Gaiser, Andreas and Kiefer, Stefan},
  title =	{{Computing Least Fixed Points of Probabilistic Systems of Polynomials}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{359--370},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2468},
  URN =		{urn:nbn:de:0030-drops-24685},
  doi =		{10.4230/LIPIcs.STACS.2010.2468},
  annote =	{Keywords: Computing fixed points, numerical approximation, stochastic models, branching processes}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2349
Comparison of Algorithms for Checking Emptiness on Büchi Automata

Authors: Andreas Gaiser and Stefan Schwoon

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract
We re-investigate the problem of LTL model-checking for finite-state systems. Typical solutions, like in Spin, work on the fly, reducing the problem to Büchi emptiness. This can be done in linear time, and a variety of algorithms with this property exist. Nonetheless, subtle design decisions can make a great difference to their actual performance in practice, especially when used on-the-fly. We compare a number of algorithms experimentally on a large benchmark suite, measure their actual run-time performance, and propose improvements. Compared with the algorithm implemented in Spin, our best algorithm is faster by about 33 % on average. We therefore recommend that, for on-the-fly explicit-state model checking, nested DFS should be replaced by better solutions.
Cite as

Andreas Gaiser and Stefan Schwoon. Comparison of Algorithms for Checking Emptiness on Büchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 18-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{gaiser_et_al:OASIcs:2009:DROPS.MEMICS.2009.2349,
  author =	{Gaiser, Andreas and Schwoon, Stefan},
  title =	{{Comparison of Algorithms for Checking Emptiness on B\"{u}chi Automata}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{18--26},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2349},
  URN =		{urn:nbn:de:0030-drops-23494},
  doi =		{10.4230/DROPS.MEMICS.2009.2349},
  annote =	{Keywords: LTL Model checking, Depth first search}
}
  • Refine by Author
  • 2 Gaiser, Andreas
  • 1 Esparza, Javier
  • 1 Kiefer, Stefan
  • 1 Schwoon, Stefan

  • Refine by Classification

  • Refine by Keyword
  • 1 Computing fixed points
  • 1 Depth first search
  • 1 LTL Model checking
  • 1 branching processes
  • 1 numerical approximation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2009
  • 1 2010

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