اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn the k-synchronizability of systems
278
0
0.0
(
0
)
تأليف
Cinzia Di Giusto
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In this paper, we work on the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata.
قيم البحث
اقرأ أيضاً
A communicating system is $k$-synchronizable if all of the message sequence charts representing the executions can be divided into slices of $k$ sends followed by $k$ receptions. It was previously shown that, for a fixed given $k$, one could decide w
hether a communicating system is $k$-synchronizable. This result is interesting because the reachability problem can be solved for $k$-synchronizable systems. However, the decision procedure assumes that the bound $k$ is fixed. In this paper we improve this result and show that it is possible to decide if such a bound $k$ exists.
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 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.
We investigate the descriptional complexity of limited propagating Lindenmayer systems and their deterministic and tabled variants with respect to the number of rules and the number of symbols. We determine the decrease of complexity when the generat
ive capacity is increased. For incomparable families, we give languages that can be described more efficiently in either of these families than in the other.
We investigate the effects of structural perturbations of both, undirected and directed diffusive networks on their ability to synchronize. We establish a classification of directed links according to their impact on synchronizability. We focus on ad
ding directed links in weakly connected networks having a strongly connected component acting as driver. When the connectivity of the driver is not stronger than the connectivity of the slave component, we can always make the network strongly connected while hindering synchronization. On the other hand, we prove the existence of a perturbation which makes the network strongly connected while increasing the synchronizability. Under additional conditions, there is a node in the driving component such that adding a single link starting at an arbitrary node of the driven component and ending at this node increases the synchronizability.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
