Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the Control of Asynchronous Automata
210
0
0.0
(
0
)
Added by
Hugo Gimbert
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Authors
Hugo Gimbert
Ask ChatGPT about the research
No Arabic abstract
The decidability of the distributed version of the Ramadge and Wonham controller synthesis problem,where both the plant and the controllers are modeled as asynchronous automataand the controllers have causal memoryis a challenging open problem.There exist three classes of plants for which the existence of a correct controller with causal memory has been shown decidable: when the dependency graph of actions is series-parallel, when the processes are connectedly communicating and when the dependency graph of processes is a tree. We design a class of plants, called decomposable games, with a decidable controller synthesis problem.This provides a unified proof of the three existing decidability results as well as new examples of decidable plants.
rate research
Read More
Subzero automata is a class of tree automata whose acceptance condition can express probabilistic constraints. Our main result is that the problem of determining if a subzero automaton accepts some regular tree is decidable.
A register automaton is a finite automaton with finitely many registers ranging from an infinite alphabet. Since the valuations of registers are infinite, there are infinitely many configurations. We describe a technique to classify infinite register automata configurations into finitely many exact representative configurations. Using the finitary representation, we give an algorithm solving the reachability problem for register automata. We moreover define a computation tree logic for register automata and solve its model checking problem.
We introduce MK-fuzzy automata over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Buchi type theorem.
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 bisimilarity 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.
We propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into control states, unlike the naive approach, and thus produces much smaller deterministic automata. We also develop a simplified and faster version of the general algorithm for the sub-class of so-called monadic CAs (MCAs), i.e., CAs with counting loops on character classes, which are common in practice. Our main motivation is (besides applications in verification and decision procedures of logics) the application of deterministic (M)CAs in pattern matching regular expressions with counting, which are very common in e.g. network traffic processing and log analysis. We have evaluated our algorithm against practical benchmarks from these application domains and concluded that compared to the naive approach, our algorithm is much less prone to explode, produces automata that can be several orders of magnitude smaller, and is overall faster.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
