6 citations · 9 across the 5 of their papers we have counts for
5 papers
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Krishnendu Chatterjee, Andreas Gaiser, Jan Křetínský
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation for the LTL(…
Proving Termination of Probabilistic Programs Using Patterns
Javier Esparza, Andreas Gaiser, Stefan Kiefer
Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The a…
Probabilistic Abstractions with Arbitrary Domains
Javier Esparza, Andreas Gaiser
Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to pr…
Computing Least Fixed Points of Probabilistic Systems of Polynomials
Javier Esparza, Andreas Gaiser, Stefan Kiefer
We study systems of equations of the form X1 = f1(X1, ..., Xn), ..., Xn = fn(X1, ..., Xn), where each fi is a polynomial with nonnegative coefficients that add up to 1. The least n…
Comparison of Algorithms for Checking Emptiness on Buechi Automata
Andreas Gaiser, Stefan Schwoon
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 Buechi emptiness. This can b…