اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدProfile Trees for Buchi Word Automata, with Application to Determinization
163
0
0.0
(
0
)
تأليف
Seth Fogarty
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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 autom
aton $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.
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 approache
s. 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.
Automata for unordered unranked trees are relevant for defining schemas and queries for data trees in Json or Xml format. While the existing notions are well-investigated concerning expressiveness, they all lack a proper notion of determinism, which
makes it difficult to distinguish subclasses of automata for which problems such as inclusion, equivalence, and minimization can be solved efficiently. In this paper, we propose and investigate different notions of horizontal determinism, starting from automata for unranked trees in which the horizontal evaluation is performed by finite state automata. We show that a restriction to confluent horizontal evaluation leads to polynomial-time emptiness and universality, but still suffers from coNP-completeness of the emptiness of binary intersections. Finally, efficient algorithms can be obtained by imposing an order of horizontal evaluation globally for all automata in the class. Depending on the choice of the order, we obtain different classes of automata, each of which has the same expressiveness as CMso.
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-u
nderstood 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.
The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynchs probabilistic bisimilarity for probabilistic automata. In this paper, we present a characterization of the bisimilar
ity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condons simple policy iteration on these games. The correctness of Condons approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in $textbf{UP} cap textbf{coUP}$ and textbf{PPAD}. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to Memoli. As an additional contribution, in this paper we show that Memolis result can be used also to prove that the bisimilarity distance bounds the difference in the maximal (or minimal) probability of two states to satisfying arbitrary $omega$-regular properties, expressed, eg., as LTL formulas.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
