English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

ion of an FSM with timed guards possesses the same features, the same holds for TFSMs. Proposition 3. A complete deterministic FSM with timed guards S is strongly connected if and only if the FSM abstraction AS is a strongly connected FSM. Proposition 4. A complete deterministic FSM with timed guards S is state reduced if and only if the FSM abstraction AS is a reduced FSM. Based on Propositions 2-4, the following statement holds. Proposition 5. Given a complete deterministic reduced and strongly connected FSM with timed guards S, a homing sequence always exists for TFSM S and length of a shortest homing sequence does not exceed n(n – 1)/2 where n is the number of TFSM states. Thus, a HS always exists for a complete reduced and strongly connected deterministic FSM with timed guards. Moreover, according to Proposition 4 and the results in [17], the upper bound of HS length cannot be reduced. Note that for a non-initialized complete observable nondeterministic FSM length of a shortest homing sequence can reach 2 – 1 – 1 [16] and thus, the following statement holds due to Proposition 2. Proposition 6. Given a non-initialized complete observable nondeterministic FSM with timed guards S, length of a shortest homing sequence can reach 2 – 1 – 1 where n is the number of TFSM states. Similar to classical FSMs, a HS does not always exist for a nondeterministic observable FSM with timed guards. Checking the existence and deriving a HS for TFSMs can be performed by a slightly modified algorithm for FSMs [16]. Algorithm 1 for checking the existence and deriving a HS for an FSM with timed guards Input: A complete non-initialized observable possibly nondeterministic FSM with timed guards S = (S, I, O, hS) Output: Message ‘There is no HS for S‘ or a HS  for TFSM S Step 1. Derive the FSM abstraction AS = (S, IA, O, hAS) for TFSM S. Step 2. Construct a truncated successor tree for the FSM AS. The root of the tree is labeled by the set of all pairs of different states while the nodes of the successor tree are labeled by sets of pairs of different states from S or empty set; edges of the tree are labeled by inputs. There exists an edge labeled by an input i from a node labeled by the set P at level j, j  0, to a node at level j+1 labeled System Informatics (Системная информатика), No. 17 (2020) 7 by the set Q where a pair {s1, s2}  Q if and only if this pair is an i/o-successor of some pair of P. Given a node labeled by the set P at the level k, k  0, the node is terminal if P is empty (Rule 1) or P contains a set R that labels a node at a level j, j < k (Rule-2). If the successor tree has no nodes labeled with the empty set, then there is no HS for FSM AS. An input sequence FSM that labels a path with minimal length to a node labeled with the empty set is transformed into a corresponding timed input sequence  that is a shortest HS for S. Nevertheless, the number of successors for each node of a truncated successor tree when checking the HS existence equals the number of inputs of the FSM abstraction, i.e., reaches (2(BS + 1)*|I|) instead of |I| for classical FSMs. In the next section, we consider classes of TFSMs for which the number of the FSM abstraction inputs can be optimized when checking the existence and deriving a HS for a timed FSM. 4. Optimizing the number of the FSM abstraction inputs when checking the existence and deriving a HS for TFSMs Here we notice that when constructing a HS for the FSM abstraction, the number of inputs becomes larger than that for the initial TFSM. In [11], approaches for the FSM abstraction optimization have been proposed in the context of test derivation procedures and in this section, we propose to use some of them for solving the HS problem for TFSMs. Consider the FSM abstraction (Table 1) of the TFSM in Figure 1. As we can see it can well happen that there exist two equal rows for different inputs of the FSM abstraction. For example, the rows of the table for inputs (i1, [0, 0]) and (i1, (0, 1)) coincide and thus, it is sufficient to consider only one of them when looking for a HS. Proposition 7. Given a complete FSM S = (S, I, O, hS) and two inputs i and i', let for each state s it holds that (s, i, o, s')  hS implies (s, i', o, s')  hS. The FSM S has a HS  if and only if a sequence ' obtained from  by the replacement of each input i' in  by i is a HS for the FSM S' = (S, I \{i'}, O, hS') where hS' is obtained from hS by the removing transitions under input i'. Proof. Let there exist HS  = i1 ... il of FSM S. Therefore, for each trace / = i1/o1 ... il/ol the /-successor of S is a singleton or does not exist. According to the statement conditions, for a sequence ' obtained from  by the replacement of each input i' in  by i it holds that the '/successor of S is a subset of the /-successor of S, i.e., is a singleton or does not exist. Thus, ' is a HS for S'. Corollary. The FSM S has a HS  of length l if and only if the FSM S' = (S, I \{i'}, O, hS') a HS

Deriving Homing Sequences for Finite State Machines with Timed Guards