-
Equivalence Checking and Intersection of Deterministic Timed Finite State Machines
Authors:
Davide Bresolin,
Khaled El-Fakih,
Tiziano Villa,
Nina Yevtushenko
Abstract:
There has been a growing interest in defining models of automata enriched with time, such as finite automata extended with clocks (timed automata). In this paper, we study deterministic timed finite state machines (TFSMs), i.e., finite state machines with a single clock, timed guards and timeouts which transduce timed input words into timed output words. We solve the problem of equivalence checkin…
▽ More
There has been a growing interest in defining models of automata enriched with time, such as finite automata extended with clocks (timed automata). In this paper, we study deterministic timed finite state machines (TFSMs), i.e., finite state machines with a single clock, timed guards and timeouts which transduce timed input words into timed output words. We solve the problem of equivalence checking by defining a bisimulation from timed FSMs to untimed ones and viceversa. Moreover, we apply these bisimulation relations to build the intersection of two timed finite state machines by untiming them, intersecting them and transforming back to the timed intersection.
△ Less
Submitted 8 March, 2021;
originally announced March 2021.
-
Preventive Model-based Verification and Repairing for SDN Requests
Authors:
Igor Burdonov,
Alexandre Kossachev,
Nina Yevtushenko,
Jorge López,
Natalia Kushik,
Djamal Zeghlache
Abstract:
Software Defined Networking (SDN) is a novel network management technology, which currently attracts a lot of attention due to the provided capabilities. Recently, different works have been devoted to testing / verifying the (correct) configurations of SDN data planes. In general, SDN forwarding devices (e.g., switches) route (steer) traffic according to the configured flow rules; the latter ident…
▽ More
Software Defined Networking (SDN) is a novel network management technology, which currently attracts a lot of attention due to the provided capabilities. Recently, different works have been devoted to testing / verifying the (correct) configurations of SDN data planes. In general, SDN forwarding devices (e.g., switches) route (steer) traffic according to the configured flow rules; the latter identifies the set of virtual paths implemented in the data plane. In this paper, we propose a novel preventive approach for verifying that no misconfigurations (e.g., infinite loops), can occur given the requested set of paths. We discuss why such verification is essential, namely, how, when synthesizing a set of data paths, other not requested and undesired data paths (including loops) may be unintentionally configured. Furthermore, we show that for some cases the requested set of paths cannot be implemented without adding such undesired behavior, i.e., only a superset of the requested set can be implemented. Correspondingly, we present a verification technique for detecting such issues of potential misconfigurations and estimate the complexity of the proposed method; its polynomial complexity highlights the applicability of the obtained results. Finally, we propose a technique for debugging and repairing a set of paths in such a way that the corrected set does not induce undesired paths into the data plane, if the latter is possible.
△ Less
Submitted 21 September, 2020; v1 submitted 7 June, 2019;
originally announced June 2019.
-
Source Code Optimization using Equivalent Mutants
Authors:
Jorge López,
Natalia Kushik,
Nina Yevtushenko
Abstract:
A mutant is a program obtained by syntactically modifying a program's source code; an equivalent mutant is a mutant, which is functionally equivalent to the original program. Mutants are primarily used in \emph{mutation testing}, and when deriving a test suite, obtaining an equivalent mutant is considered to be highly negative, although these equivalent mutants could be used for other purposes. We…
▽ More
A mutant is a program obtained by syntactically modifying a program's source code; an equivalent mutant is a mutant, which is functionally equivalent to the original program. Mutants are primarily used in \emph{mutation testing}, and when deriving a test suite, obtaining an equivalent mutant is considered to be highly negative, although these equivalent mutants could be used for other purposes. We present an approach that considers equivalent mutants valuable, and utilizes them for source code optimization. Source code optimization enhances a program's source code preserving its behavior. We showcase a procedure to achieve source code optimization based on equivalent mutants and discuss proper mutation operators. Experimental evaluation with Java and C programs demonstrates the applicability of the proposed approach. An algorithmic approach for source code optimization using equivalent mutants is proposed. It is showcased that whenever applicable, the approach can outperform traditional compiler optimizations.
△ Less
Submitted 2 July, 2018; v1 submitted 26 March, 2018;
originally announced March 2018.
-
Adaptive Homing is in P
Authors:
Natalia Kushik,
Nina Yevtushenko
Abstract:
Homing preset and adaptive experiments with Finite State Machines (FSMs) are widely used when a non-initialized discrete event system is given for testing and thus, has to be set to the known state at the first step. The length of a shortest homing sequence is known to be exponential with respect to the number of states for a complete observable nondeterministic FSM while the problem of checking t…
▽ More
Homing preset and adaptive experiments with Finite State Machines (FSMs) are widely used when a non-initialized discrete event system is given for testing and thus, has to be set to the known state at the first step. The length of a shortest homing sequence is known to be exponential with respect to the number of states for a complete observable nondeterministic FSM while the problem of checking the existence of such sequence (Homing problem) is PSPACE-complete. In order to decrease the complexity of related problems, one can consider adaptive experiments when a next input to be applied to a system under experiment depends on the output responses to the previous inputs. In this paper, we study the problem of the existence of an adaptive homing experiment for complete observable nondeterministic machines. We show that if such experiment exists then it can be constructed with the use of a polynomial-time algorithm with respect to the number of FSM states.
△ Less
Submitted 9 April, 2015;
originally announced April 2015.
-
Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power
Authors:
Davide Bresolin,
Khaled El-Fakih,
Tiziano Villa,
Nina Yevtushenko
Abstract:
There has been a growing interest in defining models of automata enriched with time. For instance, timed automata were introduced as automata extended with clocks. In this paper, we study models of timed finite state machines (TFSMs), i.e., FSMs enriched with time, which accept timed input words and generate timed output words. Here we discuss some models of TFSMs with a single clock: TFSMs with…
▽ More
There has been a growing interest in defining models of automata enriched with time. For instance, timed automata were introduced as automata extended with clocks. In this paper, we study models of timed finite state machines (TFSMs), i.e., FSMs enriched with time, which accept timed input words and generate timed output words. Here we discuss some models of TFSMs with a single clock: TFSMs with timed guards, TFSMs with timeouts, and TFSMs with both timed guards and timeouts. We solve the problem of equivalence checking for all three models, and we compare their expressive power, characterizing subclasses of TFSMs with timed guards and of TFSMs with timeouts that are equivalent to each other.
△ Less
Submitted 25 August, 2014;
originally announced August 2014.
-
Discussion on Supervisory Control by Solving Automata Equation
Authors:
Victor Bushkov,
Nina Yevtushenko,
Tiziano Villa
Abstract:
In this paper we consider the supervisory control problem through language equation solving. The equation solving approach allows to deal with more general topologies and to find a largest supervisor which can be used as a reservoir for deriving an optimal controller. We introduce the notions of solutions under partial controllability and partial observability, and we show how supervisory contro…
▽ More
In this paper we consider the supervisory control problem through language equation solving. The equation solving approach allows to deal with more general topologies and to find a largest supervisor which can be used as a reservoir for deriving an optimal controller. We introduce the notions of solutions under partial controllability and partial observability, and we show how supervisory control problems with partial controllability and partial observability can be solved by employing equation solving methods.
△ Less
Submitted 4 December, 2009;
originally announced December 2009.
-
Efficient Solution of Language Equations Using Partitioned Representations
Authors:
Alan Mishchenko,
Robert Brayton,
Roland Jiang,
Tiziano Villa,
Nina Yevtushenko
Abstract:
A class of discrete event synthesis problems can be reduced to solving language equations f . X ⊆ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs when the automata for F and S are prefix closed, and are naturally represented by multi-level networks with latches. For this special case, we present an efficient computation, using partitioned repr…
▽ More
A class of discrete event synthesis problems can be reduced to solving language equations f . X ⊆ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs when the automata for F and S are prefix closed, and are naturally represented by multi-level networks with latches. For this special case, we present an efficient computation, using partitioned representations, of the most general prefix-closed solution of the above class of language equations. The transition and the output relations of the FSMs for F and S in their partitioned form are represented by the sets of output and next state functions of the corresponding networks. Experimentally, we show that using partitioned representations is much faster than using monolithic representations, as well as applicable to larger problem instances.
△ Less
Submitted 25 October, 2007;
originally announced October 2007.
