Większość systemów informatycznych można modelować z wykorzystaniem różnego rodzaju automatów skończonych: deterministycznych, niedeterministycznych, probabilistycznych itp. Automaty te można badać pod kątem osiągalności określonych stanów i dzięki temu sprawdzać, czy system może znaleźć się w stanie krytycznym, błędnym, niechcianym. Mamy również możliwość dokonania operacji minimalizacji automatów. Praktycznie ogranicza się to do znalezienia stanów nadmiarowych i nieosiągalnych – dzięki czemu mamy również sposobność zminimalizować oryginalny, modelowany system, zaoszczędzić na dokonywanych operacjach, pamięci, a nawet sprzęcie.
EN
Most IT systems can be modeled with the use of various types of finite automata: deterministic, non-deterministic, probabilistic, etc. These automatons can be tested for reachability of certain states and thus we can check whether the system can be in a critical, erroneous or unwanted state. We also have the ability to perform the operation of automata minimization. Practically, this is limited to finding redundant and unreachable states – so we also have the opportunity to minimize the original, modeled system, save on operations amount, memory, and even hardware.
The first step to make transitional systems more efficient is to minimize the number of their states. A bisimulation relation is a mathematical tool that helps in searching for equivalent systems, what is useful in the minimization of algorithms. For two transition systems bisimulation is a binary relation associating systems which behave in the same way in the sense that one system simulates the other and viceversa. The definition for classical systems is clear and simple, but what happens with nondeterministic, probabilistic and quantum systems? This will be the main topic of this article.
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We investigate and compare the descriptional power of unary probabilistic and nondeterministic automata (pfa's and nfa's, respectively). We show the existence of a family of languages hard for pfa’s in the following sense: For any positive integer d, there exists a unary d-cyclic language such that any pfa accepting it requires d states, as the smallest deterministic automaton. On the other hand, we prove that there exist infinitely many languages having pfa’s which from one side do not match a known optimal state lower bound and, on the other side, they are smaller than nfa’s which, in turn, are smaller than deterministic automata.
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
This paper deals with the problem of checking reachability for timed automata with diagonal constraints. Such automata are needed in many applications e.g. to model scheduling problems. We introduce a new discretization for timed automata which enables SAT based reachability analysis for timed automata for which comparisons between two clocks are allowed. In our earlier papers SAT based reachability analysis was restricted to the so called diagonal-free timed automata, where only comparisons between clocks and constants are allowed.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.