Parallel algorithms for reducing derivation time of distinguishing experiments for nondeterministic finite state machines

Many approaches have been proposed for deriving tests from finite state machine (FSM) specifications with respect to some established coverage criteria. A fundamental core problem in FSM-based testing relates to the derivation of input sequences that can distinguish states of an FSM specification, aka distinguishing sequences. A major effort in the construction of these sequences is based on the derivation of a successors search-tree labeled by sets of pairs of states of the given machine. We aim at reducing the time associated with such constructions through the use of state-of-the-art parallel technologies. Namely, we propose a parallel algorithm that we implement and evaluate on multicore CPUs and on many-core GPUs. We evaluate two alternative GPU implementations that use the CUDA and Thrust software platforms and a network of workstations based solution. The latter sports a workload partitioning based on Divisible Load Theory. A rigorous set of experiments highlights the differences of the proposed implementations in terms of execution time and speedup.     

Model matching for finite-state machines

The problem of model matching for finite state machines (FSMs) consists of finding a controller for a given open-loop system so that the resulting closed-loop system matches a desired input-output behavior. In this paper, a set of model matching problems is addressed: strong model matching (where the reference model and the plant are deterministic FSMs and the initial conditions are fixed), strong model matching with measurable disturbances (where disturbances are present in the plant), and strong model matching with nondeterministic reference model (where any behavior out of those in the reference model has to be matched by the closed-loop system). Necessary and sufficient conditions for the existence of controllers for all these problems are given. A characterization of all feasible control laws is derived and an efficient synthesis procedure is proposed. Further, the well-known supervisory control problem for discrete-event dynamical systems (DEDSs) formulated in its basic form is shown to be solvable as a strong model matching problem with measurable disturbances and nondeterministic reference model     

Fast strong planning for fully observable nondeterministic planning problems

The ability to find strong solutions to fully observable nondeterministic (FOND) planning problems, if they exist, is desirable because unlike weak and strong-cyclic solutions, strong solutions are guaranteed to achieve the goal. However, only limited work has been done on FOND planning with strong solutions. In this paper, we present a sound and complete strong planning algorithm and incorporate it into our planner, FIP, which has achieved outstanding performance on strong cyclic planning problems. This new strong planning approach enables FIP to first search for strong solutions, and then search for strong-cyclic solutions only if strong solutions do not exist. We conduct extensive experiments to evaluate the new strong planning approach to (1) find a strong solution if one exists and (2) determine the non-existence of a strong solution. Experimental results demonstrate the superior performance of our planner to Gamer and MBP, the two best-known planners capable of solving strong FOND planning problems, on a variety of benchmark problems. Not only is our planner on average three orders of magnitude faster than Gamer and MBP, but it also scales up to larger problems.     

Generating Conformance Tests for Nondeterministic Protocol Machines

We present a method of generating test cases from the software specifications which are modeled by nondeterministic finite state machines.It is applicable to both nondeterministic and deterministic finite state machines.When applied to deterministic machines,this method yields usually smaller test suites with full fault coverage than the existing methods that also assure full fault coverage.In particular,the proposed method can be used to test the control portion of software specified in the formal specification languages SDL or ESTELLE.     

Reversal-bounded nondeterministic multicounter machines and complementation

It is proved that the family of languages recognized by one-way real-time nondeterministic multicounter machines with constant number of counter reversals is not closed under complementation. This solves an open problem of Wagner and Wechsung (1986).     

On adaptive experiments for nondeterministic finite state machines

Adaptive experiments are well defined in the context of finite state machine (FSM) based analysis, in particular, in FSM based testing where homing and distinguishing experiments with FSMs are used for test derivation. In this paper, we define and propose algorithms for deriving adaptive homing and distinguishing experiments for non-initialized nondeterministic finite state machines (NFSMs). For NFSMs, the construction of adaptive experiments is rather complex as the partition over produced outputs does not define a partition over the set of states but a collection of intersecting subsets, and thus, the refinement of such set system is more difficult than the refinement of a partition. Given a complete non-initialized possibly non-observable NFSM, we establish necessary and sufficient conditions for having adaptive homing and distinguishing experiments and evaluate the height of these experiments.     

Unboundedness detection for a class of communicating finite-state machines

Let M and N be two communicating finite-state machines that exchange one type of message. We discuss an algorithm to decide whether the communication between M and N is bounded. The algorithm is based on constructing a finite representation of the reachability tree of M and N assuming that M and N progress at equal speeds.     

A framework for compositional nonblocking verification of extended finite-state machines

This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.     

Complexity of ideals in finite semigroups and finite-state machines

# _G (S) denotes the complexity of a finite semigroup as introduced by Krohn and Rhodes. IfI is a maximal ideal or maximal left ideal of a semigroupS, then# _G (I) ? # _G (S) ? # _G (I) + 1. Thus, ifV is an ideal ofS with# _G (S) = n ? k = # _G (V), then there is a chain of ideals ofS

$$V = V_k \subset V_{k + 1} \subset ... \subset V_n \subseteq S$$     

An algorithm for calculating indistinguishable states and clusters in finite-state automata with partially observable transitions

This paper presents a new algorithm for efficiently calculating pairs of indistinguishable states in finite-state automata with partially observable transitions. The need to obtain pairs of indistinguishable states occurs in several classes of problems related to control under partial observation, diagnosis, or distributed control with communication for discrete event systems. The algorithm obtains all indistinguishable state pairs in polynomial time in the number of states and events in the system. Another feature of the algorithm is the grouping of states into clusters and the identification of indistinguishable cluster pairs. Clusters can be employed to solve control problems for partially observed systems.     

On deriving test suites for nondeterministic finite state machines with time-outs

In the paper, the non-separability relation for finite state machines with time-outs is studied. A specific feature of such machines is integer-valued delays, or time-outs, which determine how long the finite state machine will stay in one or another state if there are no input actions. If the time-out is over and no input symbol has been applied, then the TFSM state is changed according to the transition under time delay. In the paper, an algorithm for constructing a separating sequence for such finite state machines is presented. Here, the separating sequence is a timed input sequence for which sets of input sequences of the TFSM do not intersect; hence, it is sufficient to apply the separating sequence once in order to distinguish the TFSMs by their output reactions. This algorithm underlies the algorithm for construction of test suites with respect to non-separability relation in the case where the fault domain is specified by means of a mutation machine. Test suite derivation with respect to non-separability relation by way of ??TFSM to FSM?? transformation is discussed.     

On the synthesis of adaptive tests for nondeterministic finite state machines

The paper suggests a method for synthesis of adaptive tests with guaranteed coverage for checking functioning of discrete systems whose behavior is described by nondeterministic finite state machines. In contrast to other known methods, we do not represent the complete test as a tree but list test cases one by one and check functioning of the finite state machine on each test case. The complete test detects all defective systems that are r-distinguishable from the reference system. Besides, the test detects other defective systems containing traces that are not present in the specification; but detection of all such systems that are r-compatible with the specification is not guaranteed.     

Nonconcurrent error detection and correction in fault-tolerant linear finite-state machines

In this paper, we construct fault-tolerant linear finite-state machines (LFSMs) in which error detection and correction can be performed nonconcurrently (e.g., periodically). More specifically, by jointly choosing the state encoding constraints and the redundant dynamics of the fault-tolerant LFSM, we enable an external checker to detect and identify errors due to past faults based on the current, possibly corrupted state of the LFSM. The paper presents systematic constructions of fault-tolerant LFSMs based on a characterization of nonconcurrent error detection/correction in terms of state encoding constraints and redundant dynamics. In particular, we develop a scheme that uses Bose-Chaudhuri-Hocquenghem (BCH) coding and obtains fault-tolerant LFSMs that require 2D additional state variables and have the ability to correct up to D errors in any state variable at any time step in the time interval consisting of the latest N time steps of operation. The construction uses the minimum possible number of additional state variables and requires an error detecting/correcting mechanism with computational complexity that is only linear in N.     

A method for minimizing Moore finite-state machines by merging two states

The problem of minimization of Moore finite-state machines (FSMs) is considered. This problem often arises in designing digital devices based on programmable logic devices. The proposed approach uses the operation of merging of two states of an FSM and the representation of the FSM as a list of transitions. Conditions guaranteeing the identical operation and deterministic behavior of the transformed FSM obtained by merging two states are given. The cases when wait states can emerge are also discussed. Algorithms for minimizing the number of internal states, transition paths, and the number input variables of Moore FSMs are described. Experimental results have shown that the proposed approach reduces the number of internal states by 6% on the average and sometimes by a factor of 1.86; the number of transitions is reduced by 20% on the average and sometimes by a factor of 2.83. The use of the proposed method in combination with the STAMINA computer program reduces the number of internal states by 16% on the average and sometimes by a factor of 2.17; the number of transitions is reduced by 41% on the average and sometimes by a factor of 7.97. In conclusion, important directions of research concerning the minimization of FSMs are discussed.     

Technology for testing nondeterministic client/server database applications

The execution of a client/server application involving database access requires a sequence of database transaction events (or, T-events), called a transaction sequence (or, T-sequence). A client/server database application may have nondeterministic behavior in that multiple executions thereof with the same input may produce different T-sequences. We present a framework for testing all possible T-sequences of a client/server database application. We first show how to define a T-sequence in order to provide sufficient information to detect race conditions between T-events. Second, we design algorithms to change the outcomes of race conditions in order to derive race variants, which are prefixes of other T-sequences. Third, we develop a prefix-based replay technique for race variants derived from T-sequences. We prove that our framework can derive all the possible T-sequences in cases where every execution of the application terminates. A formal proof and an analysis of the proposed framework are given. We describe a prototype implementation of the framework and present experimental results obtained from it.     

Relations among simultaneous complexity classes of nondeterministic and alternating Turing machines

Ruzzo [Tree-size bounded alternation, J. Comput. Syst. Sci. 21] introduced the notion of tree-size for alternating Turing machines (ATMs) and showed that it is a reasonable measure for classification of complexity classes. We establish in this paper that computations by tree-size and space simultaneously bounded ATMs roughly correspond to computations by time and space simultaneously bounded nondeterministic TMs (NTMs).We also show that not every polynomial time bounded and sublinear space simultaneously bounded NTM can be simulated by any deterministic TM with a slightly increased time bound and a slightly decreased space bound simultaneously.     

On the complexity of existence of homing sequences for nondeterministic finite state machines

The paper discusses complexity of the problem of checking existence of a homing sequence for an observable complete finite state machines (FSMs). The minimum length of such a sequence for FSMs of certain class is known to be exponential in the number of the FSM states. It is shown that the problem of checking the existence of such a sequence belongs to class PSPACE.     

Synthesis of distinguishing test cases for timed finite state machines

This paper is devoted to the generation of distinguishing experiments with completely specified timed finite state machines. It is shown, in particular, that two completely specified nondeterministic finite state machines can be distinguished by a multiple preset experiment if and only if these finite state machines are not equivalent. Two finite state machines can be distinguished by a simple adaptive experiment if and only if they are r-distinguishable, i.e., have no common completely specified reduction. The corresponding adaptive experiment is described by a special timed finite state machine. The procedure for constructing such an r-distinguishing timed finite state machine is proposed.