22 citations · 31 across the 14 of their papers we have counts for
15 papers
Synthesizing Probabilistic Saturating Counters with Differentially Private Formal Guarantees
Zhiming Chi, Lutan Zhao, Depeng Liu +8
Branch predictors improve instruction-level parallelism in modern processors and are commonly modeled using saturating counters. However, classical saturating counters are determin…
A novel family of finite automata for recognizing and learning -regular languages
Yong Li, Sven Schewe, Qiyi Tang
Families of DFAs (FDFAs) have recently been introduced as a new representation of -regular languages. They target ultimately periodic words, with acceptors revolving around acce…
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata
Yong Li, Sven Schewe, Moshe Y. Vardi
We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA).…
Model Checking Strategies from Synthesis Over Finite Traces
Suguman Bansal, Yong Li, Lucas Martinelli Tabajara +2
The innovations in reactive synthesis from {\em Linear Temporal Logics over finite traces} (LTLf) will be amplified by the ability to verify the correctness of the strategies gener…
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…
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…
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…
Congruence Relations for Büchi Automata
Yong Li, Yih-Kuen Tsay, Andrea Turrini +2
We revisit here congruence relations for Büchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{\math…
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…
On the Power of Unambiguity in Büchi Complementation
Yong Li, Moshe Y. Vardi, Lijun Zhang
In this work, we exploit the power of \emph{unambiguity} for the complementation problem of Büchi automata by utilizing reduced run directed acyclic graphs (DAGs) over infinite wor…
Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications
Suguman Bansal, Yong Li, Lucas M. Tabajara +1
LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its finite-horizon behavior. So far, the conversion of LTLf f…
A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees
Yong Li, Yu-Fang Chen, Lijun Zhang +1
In this paper, we propose a novel algorithm to learn a Büchi automaton from a teacher who knows an -regular language. The algorithm is based on learning a formalism named family…
Verify LTL with Fairness Assumptions Efficiently
Yong Li, Lei Song, Yuan Feng +1
This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness…
An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties
Yong Li, Wanwei Liu, Andrea Turrini +2
In this paper, we propose an efficient algorithm for the parameter synthesis of PLTL formulas with respect to parametric Markov chains. The PLTL formula is translated to an almost…
Precise Request Tracing and Performance Debugging for Multi-tier Services of Black Boxes
Zhihong Zhang, Jianfeng Zhan, Yong Li +3
As more and more multi-tier services are developed from commercial components or heterogeneous middleware without the source code available, both developers and administrators need…