Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the k-synchronizability of systems
278
0
0.0
(
0
)
Added by
Cinzia Di Giusto
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Authors
Cinzia Di Giusto
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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 whether 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-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.
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 generative 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 adding 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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
