Hardness of Deriving Invertible Sequences from Finite State Machines | Springer Nature Link

Hardness of Deriving Invertible Sequences from Finite State Machines | Springer Nature Link
Advertisement
Hardness of Deriving Invertible Sequences from Finite State Machines
Conference paper
First Online:
11 January 2017
pp 147–160
Cite this conference paper
SOFSEM 2017: Theory and Practice of Computer Science
(SOFSEM 2017)
Abstract
Many test generation algorithms use unique input/output sequences (UIOs) that identify states of the finite state machine specification
. However, it is known that UIO checking the existence of UIO sequences is PSPACE-complete. As a result, some UIO generation algorithms utilise what are called invertible sequences; these allow one to construct additional UIOs once a UIO has been found. We consider three optimisation problems associated with invertible sequences: deciding whether there is a (proper) invertible sequence of length at least
; deciding whether there is a set of invertible sequences for state set
\(S'\)
that contains at most
input sequences; and deciding whether there is a single input sequence that defines invertible sequences that take state set
\(S''\)
to state set
\(S'\)
. We prove that the first two problems are NP-complete and the third is PSPACE-complete. These results imply that we should investigate heuristics for these problems.
This is a preview of subscription content,
log in via an institution
to check access.
Access this chapter
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Chapter
EUR 29.95
Price includes VAT (France)
eBook
EUR 42.79
Price includes VAT (France)
Softcover Book
EUR 52.74
Price includes VAT (France)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Institutional subscriptions
Similar content being viewed by others
A Randomized Parallel Algorithm for Efficiently Finding Near-Optimal Universal Hitting Sets
Chapter
State Identification and Verification with Satisfaction
Chapter
On the Convergence of Secant-Like Methods
Chapter
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Algorithmic Complexity
Algorithms
Computational Complexity
Data Structures
Data Structures and Information Theory
Sequencing
Automata Theory and Formal Languages
Notes
1.
An invertible sequence is a walk
\(\rho \)
with the property that if one determines the ending state of
\(\rho \)
then one also determines the starting state of
\(\rho \)
. In the following sections we formally define invertible sequences.
2.
Recall that we restrict attention to invertible sequences that are not redundant.
3.
Recall that
\(\varGamma _i\)
is the set of input portions of labels of the walks in
\(\varGamma \)
4.
A path is a sequence of consecutive edges that, between them, do not visit any vertex more than once.
5.
Note that in some cases the initial state of each automaton is an accepting state. Clearly, for such cases an empty input sequence defines a solution to the FA INT problem instance, hence we do not consider such cases.
References
Moore, E.P.: Gedanken-experiments. In: Shannon, C., McCarthy, J. (eds.) Automata Studies. Princeton University Press (1956)
Google Scholar
Hennie, F.C.: Fault-detecting experiments for sequential circuits. In: Proceedings of Fifth Annual Symposium on Switching Circuit Theory and Logical Design, Princeton, New Jersey, pp. 95–110, November 1964
Google Scholar
Aho, A.V., Dahbura, A.T., Lee, D., Uyar, M.U.: An optimization technique for protocol conformance test generation based on UIO sequences and rural chinese postman tours. IEEE Trans. Commun.
39
(11), 1604–1615 (1991)
Article
Google Scholar
Chow, T.S.: Testing software design modelled by finite state machines. IEEE Trans. Soft. Eng.
, 178–187 (1978)
Article
MATH
Google Scholar
Hierons, R.M., Ural, H.: Generating a checking sequence with a minimum number of reset transitions. Autom. Softw. Eng.
17
(3), 217–250 (2010)
Article
Google Scholar
Ural, H., Zhu, K.: Optimal length test sequence generation using distinguishing sequences. IEEE/ACM Trans. Network.
(3), 358–371 (1993)
Article
Google Scholar
Luo, G.L., von Bochmann, G., Petrenko, A.: Test selection based on communicating nondeterministic finite-state machines using a generalized Wp-method. IEEE Trans. Softw. Eng.
20
(2), 149–161 (1994)
Article
Google Scholar
Petrenko, A., Yevtushenko, N., von Bochmann, G.: Testing deterministic implementations from nondeterministic FSM specifications. In: Baumgarten, B., Burkhardt, H.-J., Giessler, A. (eds.) IFIP TC6 9th International Workshop on Testing of Communicating Systems, Darmstadt, Germany, 9–11 September 1996, pp. 125–141. Chapman and Hall (1996)
Google Scholar
Gill, A.: Introduction to The Theory of Finite State Machines. McGraw-Hill, New York (1962)
MATH
Google Scholar
Kohavi, Z.: Switching and Finite State Automata Theory. McGraw-Hill, New York (1978)
MATH
Google Scholar
Boute, R.T.: Distinguishing sets for optimal state identification in checking experiments. IEEE Trans. Comput.
23
, 874–877 (1974)
Article
Google Scholar
Ural, H., Wu, X., Zhang, F.: On minimizing the lengths of checking sequences. IEEE Trans. Comput.
46
(1), 93–99 (1997)
Article
Google Scholar
Aho, A.V., Dahbura, A.T., Lee, D., Uyar, M.U.: An optimization technique for protocol conformance test generation based on UIO sequences and rural chinese postman tours. In: Protocol Specification, Testing, and Verification VIII, pp. 75–86. Elsevier (North-Holland), Atlantic City (1988)
Google Scholar
Chan, W.Y.L., Vuong, C.T., Otp, M.R.: An improved protocol test generation procedure based on UIOs. SIGCOMM Comput. Commun. Rev.
19
(4), 283–294 (1989)
Article
Google Scholar
Chen, W.-H., Ural, H.: Synchronizable test sequences based on multiple UIO sequence. IEEE/ACM Trans. Netw.
(2), 152–157 (1995)
Article
Google Scholar
Guyot, S., Ural, H.: Synchronizable checking sequences based on UIO sequences. In: Protocol Test Systems, VIII, Evry, France, September 1995, pp. 385–397. Chapman and Hall (1995)
Google Scholar
Motteler, H., Chung, A., Sidhu, D.: Fault coverage of UIO-based methods for protocol testing. In: Proceedings of Protocol Test Systems VI, pp. 21–33 (1994)
Google Scholar
Ramalingam, T., Thulasiraman, K., Das, A.: A generalization of the multiple UIO method of test sequence selection for protocols represented in FSM. In: The 7th International workshop on Protocol Test Systems, Japan, pp. 209–224. Chapman and Hall (1994)
Google Scholar
Ural, H., Wang, Z.: Synchronizable test sequence generation using UIO sequences. Comput. Commun.
16
(10), 653–661 (1993)
Article
Google Scholar
Vuong, S.T., Chan, W.W.L., Ito, M.R.: The UIOv-method for protocol test sequence generation. In: The 2nd International Workshop on Protocol Test Systems, Berlin (1989)
Google Scholar
Lee, D., Yannakakis, M.: Testing finite-state machines: state identification and verification. IEEE Trans. Comput.
43
(3), 306–320 (1994)
Article
MathSciNet
Google Scholar
Vasilevskii, M.P.: Failure diagnosis of automata. Cybernetics
, 653–665 (1973)
Google Scholar
Hierons, R.M., Türker, U.C.: Parallel algorithms for generating harmonised state identifiers, characterising sets (accepted). IEEE Trans. Softw. Eng. (2016)
Google Scholar
Gonenc, G.: A method for the design of fault detection experiments. IEEE Trans. Comput.
19
, 551–558 (1970)
Article
MATH
Google Scholar
Hierons, R.M., Ural, H.: Optimizing the length of checking sequences. IEEE Trans. Comput.
55
, 618–629 (2006)
Article
Google Scholar
Hierons, R.M., Ural, H.: Reduced length checking sequences. IEEE Trans. Comput.
51
(9), 1111–1117 (2002)
Article
MathSciNet
Google Scholar
Hierons, R.M.: Extending test sequence overlap by invertibility. Comput. J.
39
(4), 325–330 (1996)
Article
Google Scholar
Naik, K.: Efficient computation of unique input/output sequences in finite-state machines. IEEE/ACM Trans. Netw.
(4), 585–599 (1997)
Article
Google Scholar
Hopcroft, J.E.: An n log n algorithm for minimizing the states in a finite automaton. In: Kohavi, Z. (ed.) The Theory of Machines and Computation, pp. 189–196. Academic Press, New York (1971)
Chapter
Google Scholar
Garey, M.R., Johnson, D.S.: Computers and Intractability. W.H. Freeman and Company, New York (1979)
MATH
Google Scholar
Kozen, D.: Lower bounds for natural proof systems. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 254–266. IEEE Computer Society, Washington (1977)
Google Scholar
Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci.
(2), 177–192 (1970)
Article
MathSciNet
MATH
Google Scholar
Download references
Acknowledgments
This work is supported by the COST Action under Grant #IC1405.
Author information
Authors and Affiliations
Department of Computer Science, Brunel University London, Uxbridge, UK
Robert M. Hierons
School of IT, Center for Research on Embedded Systems (CERES), Halmstad University, Halmstad, Sweden
Mohammad Reza Mousavi
Department of Computer Science, University of Copenhagen, Copenhagen, Denmark
Michael Kirkedal Thomsen
Computer Engineering, Faculty of Engineering, Gebze Technical University, Kocaeli, Turkey
Uraz Cengiz Türker
Authors
Robert M. Hierons
View author publications
Search author on:
PubMed
Google Scholar
Mohammad Reza Mousavi
View author publications
Search author on:
PubMed
Google Scholar
Michael Kirkedal Thomsen
View author publications
Search author on:
PubMed
Google Scholar
Uraz Cengiz Türker
View author publications
Search author on:
PubMed
Google Scholar
Corresponding author
Correspondence to
Uraz Cengiz Türker
Editor information
Editors and Affiliations
TU Dortmund , Dortmund, Germany
Bernhard Steffen
TU Dresden , Dresden, Germany
Christel Baier
Eindhoven University of Technology , Eindhoven, The Netherlands
Mark van den Brand
Alpen Adria University Klagenfurt , Klagenfurt, Austria
Johann Eder
Lero - Irish Software Research Center , Limerick, Ireland
Mike Hinchey
Lero - Irish Software Research Center , Limerick, Ireland
Tiziana Margaria
Appendix
Appendix
Lemma 3
Let
\(\bar{x}/\bar{y}\)
be a UIO for state
\(\rho \)
be a proper invertible sequence for
and also let
\(\psi =\{ (s', \rho ') | s' \in S, \rho ' \in post(\rho )\, \text {and}\, s'\, \text {is the initial state of}\, \rho ' \}\)
be the set of pairs of suffixes of
\(\rho \)
and states from which they originate, then for each pair
\((s',\rho ')\)
in
\(\psi \)
\(in(\rho ')\bar{x}/out(\rho ')\bar{y}\)
is a UIO for
\(s'\)
Proof
We use proof by contradiction. Let
\(\psi \)
be the set of pairs of suffixes and states of some invertible sequence
\(\rho \)
for state
. Consider a pair
\((s',\rho ')\)
and let us suppose that
\(in(\rho ')\bar{x}/out(\rho ')\bar{y}\)
is not a UIO for
\(s'\)
. This implies that there exists a state
\(s''\ne s'\)
such that there exists a walk from
\(s''\)
labeled with input/output sequence
\(in(\rho ')\bar{x}/out(\rho ')\bar{y}\)
. Now consider the state
\(s'''\)
reached from
\(s''\)
with walk
\(in(\rho ')/out(\rho ')\)
. As the underlying FSM is deterministic we have two options:
we have
\(s'''=s\)
or we have
\(s''' \in S{\setminus }\{s\}\)
In the first case,
\(\rho '\)
cannot be an invertible sequence. Otherwise, if the second case holds, then
\(\bar{x}/\bar{y}\)
cannot be a UIO for
. The result thus follows.
\(\square \)
Proposition 1
The longest path problem instance (
) has a solution if and only if state
\(s_{\star }\)
of
) has a proper invertible sequence
\(\rho \)
of length
\(K+1\)
Proof
First we prove that if
has a path
\(\mathcal {P} = e_1 e_2 \ldots e_{K}\)
of length
, then
) has a proper invertible sequence for
\(s_{\star }\)
whose input portion has length
\(K+1\)
. First note that for every vertex and edge of
there exists a state and a transition in
) respectively. Let
\(\rho =x_1/y_1 x_2/y_2 \ldots x_{K}/y_{K}\)
be the label of the walk corresponding to
\(\mathcal {P}\)
. Since every transition of
) is labelled with unique input/output values,
\(\rho = x_1/y_1 x_2/y_2 \ldots x_{K}/y_{K}\)
defines an invertible sequence for a state of
). Finally, if we concatenate
\(\rho \)
with some
\(\rho '=\star /y_j\)
, which is the label of a walk that starts from the ending state of walk
\(\rho \)
, then
\(\rho ''= \rho \rho '\)
defines an invertible sequence for
\(s_{\star }\)
Now assume that
\(s_{\star }\)
has a proper invertible sequence
\(\rho = x_1/y_1x_2/y_2\ldots x_{K+1}/y_{K+1} \)
of length
\(K+1\)
and we are required to prove that
has a path of length
. Note that since
\(\rho \)
is an invertible sequence for
\(s_{\star }\)
, the last input/output pair belongs to a transition that takes
) to state
\(s_{\star }\)
. Besides, since
\(\rho \)
is a proper invertible sequence, the first
symbols of the input portion of
\(\rho \)
should visit
\(K+1\)
different states of
). Since for every state and transition of
), there exists a corresponding vertex and edge in
, the first
inputs of
\(\rho \)
define a path of
with length
. Thus the result follows.
\(\square \)
Theorem 1
The LPIS problem is
NP-complete
Proof
We first show that the LPIS problem is in
NP
. A non-deterministic Turing machine can guess an input sequence
\(\bar{x}\)
of length
. It can then apply
\(\bar{x}\)
to every state and record the resultant output sequence and state reached. Afterwards, it can compare the outputs to decide whether
\(\bar{x}\)
defines an invertible sequence for a specific state
The problem is
NP-hard
due to Proposition
and the fact that the longest path problem with directed graphs is
NP-hard
. Therefore the result follows.
\(\square \)
Proposition 2
The minimum covering problem instance
\((G,\mathcal{I}, K)\)
has a solution if and only if
\(S'=\{s_{\star }\}\)
of
\(M(U,\mathcal{I}, K)\)
has a minimum spanning invertible sequence
\(\varGamma \)
with
\(|\varGamma _i|\le K\)
Proof
First we prove that if
\(U, \mathcal{I}, K\)
has a minimum covering
\(\mathcal {I}' = \{I_1, I_2, \ldots , I_{K}\}\)
then
\(M(U, \mathcal{I}, K)\)
has a set of invertible sequences
\(\varGamma \)
for
\(S'=\{s_{\star }\}\)
such that
\(\varGamma _i=\{x_1,x_2,\ldots ,x_K\}\)
. Note that the transitions and output functions of the FSM
\(M(U, \mathcal{I}, K)\)
dictates that for a given input
\(x_i\)
and output
\(y_j\)
pair, there exists at most one transition with ending state
\(s^{\star }\)
and label
\(x_i/y_j\)
. Therefore, each transition with ending state
\(s_{\star }\)
is an invertible transition and hence there is a set
\(\varGamma \)
of invertible sequences that take
from
\(S {\setminus } \{s_{\star }\}\)
to
\(s_{\star }\)
. Further, for every set
\(I_i\)
in
\(\mathcal I\)
there exists a single corresponding input symbol
\(x_i\)
and so
\(\varGamma _i = \{x_1, \dots , x_K\}\)
. Thus,
\(\varGamma \)
defines a spanning invertible sequence for
\(S'\)
with
\(|\varGamma _i| =K\)
as required.
Now we assume that
\(S'=\{s_{\star }\}\)
has a maximum spanning invertible sequence
\(\varGamma \)
such that
\(|\varGamma _i|= K\)
and we are required to prove that
has a minimum covering with at most
sets. First note that as we only consider invertible sequences that are not redundant, the length of each input sequence in set
\(\varGamma _i\)
is one. Let
\(\varGamma _i=\{ \bar{x}_1,\bar{x}_2, \ldots , \bar{x}_K \}\)
. Therefore, there is a set
\(\mathcal{I}'=\{I_1, I_2, \ldots ,I_K \}\)
of sets derived from
\(\varGamma _I\)
. The result thus follows.
\(\square \)
Theorem 2
The MINSIS problem is
NP-complete.
Proof
The proof of being in
NP
is almost similar to that of Theorem
. However this time Turing machine should guess at most
input sequences. The problem is
NP-hard
due to Proposition
, thus the result follows.
\(\square \)
Theorem 3
PRSIS problem is
PSPACE-complete.
Proof
We first show that the PRSIS problem is in
PSPACE
. The working principle of the Turing machine for the PRSIS problem is as follows. First note that a non-deterministic Turing machine
\(\mathcal {T}\)
can take
\(S''\)
to
\(S'\)
input by input as follows: Let
be the sequences of inputs guessed by
\(\mathcal {T}\)
so far, and
\(\mathcal {T}\)
guesses an input
. After this point
\(\mathcal {T}\)
applies
to states
\(\delta (S'',w)\)
\(\mathcal {T}\)
should then check whether (a)
\(\delta (S'',wx)=S'\)
, and (b) For all
\(s \in S''\)
and
\(s' \in S\)
, if
\(\delta (s,wx) = \delta (s',wx)\)
then
\(\lambda (s,wx) \ne \lambda (s',wx)\)
If these three conditions hold
\(\mathcal {T}\)
returns at accepting state. Otherwise it returns at rejecting state.
To achieve this
\(\mathcal {T}\)
maintains (and updates on each iteration) the following information (given input sequence
): (1) a partition
of
\(S''\)
saying which pairs of states from
\(S''\)
are not distinguished by
. (2) For each state
\(s \in S''\)
, the pair
\((s',S''')\)
where:
\(s' = \delta (s,w)\)
is the current state corresponding to
and
\(S'''\)
is the set of current states from states in
\(S{\setminus } S''\)
that are not distinguished from
. Thus
\(S''' = \{\delta (s'',w) | s'' \in S {\setminus } S'' \wedge \lambda (s,w) = \lambda (s'',w)\}\)
Clearly, it is straightforward to update this information if we extend
to
wx
(guessing
). It is also easy to spot when one should not extend further by
(either the current states reached from states of
\(S''\)
not distinguished by
‘converge’ or there is some
\((s',S''')\)
such that
\(s'\)
and a state from
\(S'''\)
‘converge’).
The above can clearly be stored in polynomial space. In addition to the terminating conditions mentioned above,
\(\mathcal {T}\)
should terminate when the upper bound is reached. First note that the number of possible values for a pair
\((s',S''')\)
is bounded above by
\(n.2^n\)
and so the number of possible such pairs is bounded above by:
\((n2^n)^K = n^K.2^{nK}\)
. Second, initially
contains
sets. The only way we can change
is by merging two or more sets, with this reducing the number of sets in
. Thus, the value of
can change at most
\(K-1\)
times.
Therefore the upper bound for the PRSIS is
\((K-1).n^K.2^{(nK)}\)
. Note that this information can be stored in polynomial space, i.e.
\(O(log((K-1).n^K.2^{(nK)}))= O(log(K-1)+ Klog(n)+ nKlog(2))\)
space and the Turing machine
\(\mathcal {T}\)
can hold a counter and increment this by one after an input is guessed. Therefore when the value stored in the counter exceeds the upper bound value,
\(\mathcal {T}\)
terminates.
Therefore, the entire search in this way can be performed in
NPSPACE
. Based on Savitch’s Theorem [
32
], the PRSIS problem is in
PSPACE
as required.
Now we prove that if the automata accept a common word
\(w \in \varSigma \)
then
\(M(\mathbb {A})\)
has an invertible sequence that takes
\(S''\)
to
\(S'\)
. Clearly the application of
\(fwf'\)
from a state of
\(S''\)
brings
\(M(\mathbb {A})\)
to one of states in
\(S'\)
. As the output produced as a response to input
is unique,
\(fwf'\)
is a PRSIS for
\(S'\)
as required.
Now we assume that there are invertible sequences with common input sequence
\(\bar{x}\)
that take
\(S''\)
to
\(S'\)
and we are required to prove that there is a common element for the automata in
\(\mathbb {A}\)
. Note since
\(\bar{x}\)
takes
\(S''\)
to
\(S'\)
, the input sequence
\(\bar{x}\)
should contain at least one
and must end with
\(f'\)
. Let
\(\bar{x}'f'\)
be the suffix of
\(\bar{x}\)
after the first input
. After the application of
, the FSM is in a state that corresponds to an initial state of the corresponding automaton. Since
\(\bar{x}\)
takes
\(S''\)
to
\(S'\)
\(\bar{x}'f'\)
must takes set
\(\delta (S'',f)\)
to
\(S'\)
and so
\(\bar{x}\)
must take initial states of the
\(A_i\)
to final states. The result thus follows setting
\(w = \bar{x}\)
\(\square \)
Rights and permissions
Reprints and permissions
Copyright information
About this paper
Cite this paper
Hierons, R.M., Mousavi, M.R., Thomsen, M.K., Türker, U.C. (2017). Hardness of Deriving Invertible Sequences from Finite State Machines.

In: Steffen, B., Baier, C., van den Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds) SOFSEM 2017: Theory and Practice of Computer Science. SOFSEM 2017. Lecture Notes in Computer Science(), vol 10139. Springer, Cham. https://doi.org/10.1007/978-3-319-51963-0_12
Download citation
.RIS
.ENW
.BIB
DOI
Published
11 January 2017
Publisher Name
Springer, Cham
Print ISBN
978-3-319-51962-3
Online ISBN
978-3-319-51963-0
eBook Packages
Computer Science
Computer Science (R0)
Springer Nature Proceedings Computer Science
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Input Sequence
Finite State Machine
Finite Automaton
System Under Test
Generate Test Case
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Publish with us
Policies and ethics
Access this chapter
Log in via an institution
Subscribe and save
Springer+
from €37.37 /Month
Starting from 10 chapters or articles per month
Access and download chapters and articles from more than 300k books and 2,500 journals
Cancel anytime
View plans
Buy Now
Chapter
EUR 29.95
Price includes VAT (France)
eBook
EUR 42.79
Price includes VAT (France)
Softcover Book
EUR 52.74
Price includes VAT (France)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Institutional subscriptions