Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userProving Non-Inclusion of Buchi Automata based on Monte Carlo Sampling
102
0
0.0
(
0
)
Added by
Yong Li
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
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 tools it is better to pursue them at the same time. While this is well-understood in the termination analysis of programs, this is not the case for the language inclusion analysis of Buchi automata, where research mainly focused on improving algorithms for proving language inclusion, with the search for counterexamples left to the expensive complementation operation. In this paper, we present $mathsf{IMC}^2$, a specific algorithm for proving Buchi automata non-inclusion $mathcal{L}(mathcal{A}) otsubseteq mathcal{L}(mathcal{B})$, based on Grosu and Smolkas algorithm $mathsf{MC}^2$ developed for Monte Carlo model checking against LTL formulas. The algorithm we propose takes $M = lceil ln delta / ln (1-epsilon) rceil$ random lasso-shaped samples from $mathcal{A}$ to decide whether to reject the hypothesis $mathcal{L}(mathcal{A}) otsubseteq mathcal{L}(mathcal{B})$, for given error probability $epsilon$ and confidence level $1 - delta$. With such a number of samples, $mathsf{IMC}^2$ ensures that the probability of witnessing $mathcal{L}(mathcal{A}) otsubseteq mathcal{L}(mathcal{B})$ via further sampling is less than $delta$, under the assumption that the probability of finding a lasso counterexample is larger than $epsilon$. Extensive experimental evaluation shows that $mathsf{IMC}^2$ is a fast and reliable way to find counterexamples to Buchi automata inclusion.
rate research
Read More
We revisit here congruence relations for Buchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{mathcal{O}(n^2)}$, where $n$ is the number of states of a given Buchi automaton $mathcal{A}$. Here we present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptotically optimal congruence relations of size $2^{mathcal{O}(n log n)}$. Based on these optimal congruence relations, we obtain an optimal translation from Buchi automata to a family of deterministic finite automata (FDFW) that accepts the complementary language. To the best of our knowledge, our construction is the first direct and optimal translation from Buchi automata to FDFWs.
In this work, we exploit the power of emph{unambiguity} for the complementation problem of Buchi automata by utilizing reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor. We then show how to use this type of reduced run DAGs as a emph{unified tool} to optimize emph{both} rank-based and slice-based complementation constructions for Buchi automata with a finite degree of ambiguity. As a result, given a Buchi automaton with $n$ states and a finite degree of ambiguity, the number of states in the complementary Buchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved, respectively, to $2^{O(n)}$ from $2^{O(nlog n)}$ and to $O(4^n)$ from $O((3n)^n)$.
The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run DAG contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally.
Complementation of Buchi automata has been studied for over five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. Regarding the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all of the four approaches to see how they perform in practice. In this paper, we review the four approaches, propose several optimization heuristics, and perform comparative experimentation on four representative constructions that are considered the most efficient in each approach. The experimental results show that (1) the determinization-based Safra-Piterman construction outperforms the other three in producing smaller complements and finishing more tasks in the allocated time and (2) the proposed heuristics substantially improve the Safra-Piterman and the slice-based constructions.
Complementation of Buchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kahler and Wilke. This approach tracks levels of split trees - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves the tight bound of Schewes construction
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
