activity
20122026
most citedDeciding Probabilistic Automata Weak Bisimulation in Polynomial Time

6 citations · 17 across the 16 of their papers we have counts for

collaborators
Showing cs.FLShow all

6 papers · 1 filter

cs.FL2023★ 1 cited

Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)

Vojtěch Havlena, Ondřej Lengál, Yong Li +2

Complementation of nondeterministic Büchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis…

cs.FL2022

Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition

Yong Li, Andrea Turrini, Weizhi Feng +2

The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synth…

cs.FL2021

On the Power of Finite Ambiguity in Büchi Complementation

Weizhi Feng, Yong Li, Andrea Turrini +2

In this work, we exploit the power of \emph{finite ambiguity} for the complementation problem of Büchi automata by using reduced run directed acyclic graphs (DAGs) over infinite wo…

cs.FL2020★ 1 cited

Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling

Yong Li, Andrea Turrini, Xuechao Sun +1

The search for a proof of correctness and the search for counterexamples (bugs) are complementary aspects of verification. In order to maximize the practical use of verification to…

cs.FL2014★ 4 cited

Cost Preserving Bisimulations for Probabilistic Automata

Andrea Turrini, Holger Hermanns

Probabilistic automata constitute a versatile and elegant model for concurrent probabilistic systems. They are equipped with a compositional theory supporting abstraction, enabled…

cs.FL2012★ 6 cited

Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time

Holger Hermanns, Andrea Turrini

Deciding in an efficient way weak probabilistic bisimulation in the context of Probabilistic Automata is an open problem for about a decade. In this work we close this problem by p…