scholarly journals On the Modeling of Sequential Reactive Systems by Means of Real Time Automata

2020 ◽  
Vol 27 (4) ◽  
pp. 396-411
Author(s):  
Evgeney Maximovich Vinarskii ◽  
Vladimir Anatolyevich Zakharov

Sequential reactive systems include hardware devices and software programs which operate in continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of output signals. Systems of this type include controllers, network switches, program interpreters, system drivers. The behavior of some reactive systems is determined not only by the sequence of values of input signals, but also by the time of their arrival at the inputs of the system and the delays in computing the output signals. These aspects of reactive system computations are taken into account by real-time models of computation which include, in particular, realtime finite state machines (TFSMs). However, in most works where this class of real-time automata is studied a simple variant of TFSM semantics is used: the transduction relation computed by a TFSM is defined so that the elements of an output stream, regardless oftheir timestamps, follow in the same order as the corresponding elements ofthe input stream. This straightforward approach makes the model easier to analyze and manipulate, but it misses many important features of real-time computation. In this paper we study a more realistic semantics of TFSMs and show how to represent it by means of Labeled Transition Systems. The use of the new TFSM model also requires new approaches to the solution of verification problems in the framework of this model. For this purpose, we propose an alternative definition of TFSM computations by means of Labeled Transition Systems and show that the two definitions of semantics for the considered class of real-time finite state machines are in good agreement with each other. The use of TFSM semantics based on Labeled Transition Systems opens up the possibility of adapting well known real-time model checking techniques to the verification ofsequential reactive systems.

2009 ◽  
Vol 19 (02) ◽  
pp. 247-264 ◽  
Author(s):  
MARTIN KUTRIB ◽  
ANDREAS MALCHER

Iterative arrays (IAs) are linear arrays of interconnected interacting finite state machines, where one distinguished one is equipped with a one-way read-only input tape. We investigate IAs operating in real time whose inter-cell communication is bounded by a constant number of bits not depending on the number of states. Their capabilities are considered in terms of syntactical pattern recognition. It is known [17] that such devices can recognize rather complicated sets of unary patterns with a minimum amount of communication, namely one-bit communication. Some examples are the sets {a2n | n ≥ 1}, {an2 | n ≥ 1}, and {ap | p is prime}. Here, we consider non-unary patterns and it turns out that the non-unary case is quite different. We present several real-time constructions for certain non-unary syntactical patterns. For example, the sets {anbn | n ≥ 1}, {anbncn | n ≥ 1}, {an(bn)m | n, m ≥ 1}, and {anbamb(ba)n·m | n, m ≥ 1} are recognized in real time by IAs. Moreover, it is shown that real-time one-bit IAs can, in some sense, add and multiply integer numbers. Furthermore, decidability questions of communication restricted IAs are dealt with. Due to the constructions provided, undecidability results can be derived. It turns out that emptiness is still not even semidecidable for one-bit IAs despite their restricted communication. Moreover, also the questions of finiteness, infiniteness, inclusion, and equivalence are non-semidecidable.


2009 ◽  
Vol 2009 ◽  
pp. 1-12 ◽  
Author(s):  
Elmer P. Dadios ◽  
Soo ho Park

This paper presents a new algorithm for real time event detection using Finite State Machines with multiple Fuzzy Logic Probability Evaluators (FLPEs). A machine referee for a robot soccer game is developed and is used as the platform to test the proposed algorithm. A novel technique to detect collisions and other events in microrobot soccer game under inaccurate and insufficient information is presented. The robots' collision is used to determine goalkeeper charging and goal score events which are crucial for the machine referee's decisions. The Main State Machine (MSM) handles the schedule of event activation. The FLPE calculates the probabilities of the true occurrence of the events. Final decisions about the occurrences of events are evaluated and compared through threshold crisp probability values. The outputs of FLPEs can be combined to calculate the probability of an event composed of subevents. Using multiple fuzzy logic system, the FLPE utilizes minimal number of rules and can be tuned individually. Experimental results show the accuracy and robustness of the proposed algorithm.


Author(s):  
Evgeniy Maximovich Vinarskii ◽  
◽  
Vladimir Anatolyevoch Zakharov ◽  

Sequential reactive systems are formal models of programs that interact with the environment by receiving inputs and producing corresponding outputs. Such formal models are widely used in software engineering, computational linguistics, telecommunication, etc. In real life, the behavior of a reactive system depends not only on the flow of input data, but also on the time the input data arrive and the delays that occur when generating responses. To capture these aspects, a timed finite state machine (TFSM) is used as a formal model of a real-time sequential reactive system. However, in most of known previous works, this model was considered in simplified semantics: the responses in the output stream, regardless of their timestamps, follow in the same order in which the corresponding inputs are delivered to the machine. This simplification makes the model easier to analyze and manipulate, but it misses many important aspects of real-time computation. In this paper we study a refined semantics of TFSMs and show how to represent it by means of Labelled Transition Systems. This opens up a possibility to apply traditional formal methods for verifying more subtle properties of real-time reactive behavior which were previously ignored.


2017 ◽  
Vol 16 (5s) ◽  
pp. 1-21 ◽  
Author(s):  
Yecheng Zhao ◽  
Chao Peng ◽  
Haibo Zeng ◽  
Zonghua Gu

Sign in / Sign up

Export Citation Format

Share Document