1 citations · 2 across the 4 of their papers we have counts for
5 papers
Reachability in Dynamical Systems with Rounding
Christel Baier, Florian Funke, Simon Jantsch +6
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a…
SWITSS: Computing Small Witnessing Subsystems
Simon Jantsch, Hans Harder, Florian Funke +1
Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as…
Minimal witnesses for probabilistic timed automata
Simon Jantsch, Florian Funke, Christel Baier
Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input t…
Farkas certificates and minimal witnesses for probabilistic reachability constraints
Florian Funke, Simon Jantsch, Christel Baier
This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an…
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Simon Jantsch, David Müller, Christel Baier +1
This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm d…