No Arabic abstract
In this paper, emph{diagnosability} is characterized for a labeled max-plus automaton $mathcal{A}^{mathcal{D}}$ over a dioid $mathcal{D}$ as a real-time system. In order to represent time elapsing, a special class of dioids called emph{progressive} are considered, in which there is a total canonical order, there is at least one element greater than $textbf{1}$, the product of sufficiently many elements greater than $textbf{1}$ is arbitrarily large, and the cancellative law is satisfied. Then a notion of diagnosability is formulated for $mathcal{A}^{mathcal{D}}$ over a progressive dioid $mathcal{D}$. By developing a notion of emph{concurrent composition}, a sufficient and necessary condition is given for diagnosability of automaton $mathcal{A}^{mathcal{D}}$. It is also proven that the problem of verifying diagnosability of $mathcal{A}^{underline{mathbb{Q}}}$ is coNP-complete, where coNP-hardness even holds for deterministic, deadlock-free, and divergence-free $mathcal{A}^{underline{mathbb{N}}}$, where $underline{mathbb{Q}}$ and $underline{mathbb{N}}$ are the max-plus dioids having elements in $mathbb{Q}cup{-infty}$ and $mathbb{N}cup{-infty}$, respectively.
In this paper, by developing appropriate methods, we for the first time obtain characterization of four fundamental notions of detectability for general labeled weighted automata over monoids (denoted by $mathcal{A}^{mathfrak{M}}$ for short), where the four notions are strong (periodic) detectability (SD and SPD) and weak (periodic) detectability (WD and WPD). Firstly, we formulate the notions of concurrent composition, observer, and detector for $mathcal{A}^{mathfrak{M}}$. Secondly, we use the concurrent composition to give an equivalent condition for SD, use the detector to give an equivalent condition for SPD, and use the observer to give equivalent conditions for WD and WPD, all for general $mathcal{A}^{mathfrak{M}}$ without any assumption. Thirdly, we prove that for a labeled weighted automaton over monoid $(mathbb{Q}^k,+)$ (denoted by $mathcal{A}^{mathbb{Q}^k}$), its concurrent composition, observer, and detector can be computed in NP, $2$-EXPTIME, and $2$-EXPTIME, respectively, by developing novel connections between $mathcal{A}^{mathbb{Q}^k}$ and the NP-complete exact path length problem (proved by [Nyk{a}nen and Ukkonen, 2002]) and a subclass of Presburger arithmetic. As a result, we prove that for $mathcal{A}^{mathbb{Q}^k}$, SD can be verified in coNP, while SPD, WD, and WPD can be verified in $2$-EXPTIME. Particularly, for $mathcal{A}^{mathbb{Q}^k}$ in which from every state, a distinct state can be reached through some unobservable, instantaneous path, its detector can be computed in NP, and SPD can be verified in coNP. Finally, we prove that the problems of verifying SD and SPD of deterministic $mathcal{A}^{mathbb{N}}$ over monoid $(mathbb{N},+)$ are both NP-hard. The original methods developed in this paper will provide foundations for characterizing other fundamental properties (e.g., diagnosability and opacity) in $mathcal{A}^{mathfrak{M}}$.
We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an emph{adaptive} manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness. To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most $k$ leaves and we provide an $n^{O(k^2)}$ time algorithm for this problem.
We introduce homing vector automata, which are finite automata augmented by a vector that is multiplied at each step by a matrix determined by the current transition, and have to return the vector to its original setting in order to accept the input. The computational power and properties of deterministic, nondeterministic, blind, non-blind, real-time and one-w
We introduce a certain restriction of weighted automata over the rationals, called image-binary automata. We show that such automata accept the regular languages, can be exponentially more succinct than corresponding NFAs, and allow for polynomial complementation, union, and intersection. This compares favourably with unambiguous automata whose complementation requires a superpolynomial state blowup. We also study an infinite-word version, image-binary Buchi automata. We show that such automata are amenable to probabilistic model checking, similarly to unambiguous Buchi automata. We provide algorithms to translate $k$-ambiguous Buchi automata to image-binary Buchi automata, leading to model-checking algorithms with optimal computational complexity.
We present a new model of neural networks called Min-Max-Plus Neural Networks (MMP-NNs) based on operations in tropical arithmetic. In general, an MMP-NN is composed of three types of alternately stacked layers, namely linear layers, min-plus layers and max-plus layers. Specifically, the latter two types of layers constitute the nonlinear part of the network which is trainable and more sophisticated compared to the nonlinear part of conventional neural networks. In addition, we show that with higher capability of nonlinearity expression, MMP-NNs are universal approximators of continuous functions, even when the number of multiplication operations is tremendously reduced (possibly to none in certain extreme cases). Furthermore, we formulate the backpropagation algorithm in the training process of MMP-NNs and introduce an algorithm of normalization to improve the rate of convergence in training.