The concept of Strong Backdoor Sets (SBS) for Constraint Satisfaction Problems is well known as one of the attempts to exploit structural peculiarities in hard instances. However, in practice, finding an SBS for a particular instance is often harder than solving it. Recently, a probabilistic weakened variant of the SBS was introduced: in the SBS, all subproblems must be polynomially solvable, whereas in the probabilistic SBS only a large fraction ρ of them should have this property. This new variant of backdoors called ρ-backdoors makes it possible to use the Monte Carlo method and metaheuristic optimization to find ρ-backdoors with ρ very close to 1, and relatively fast. Despite the fact that in a ρ-backdoor-based decomposition a portion of hard subproblems remain, in practice the narrowing of the search space often allows solving the problem faster with such a backdoor than without it. In this paper, we significantly improve on the concept of ρ-backdoors by extending this concept to backdoor trees: we introduce ρ-backdoor trees, show the interconnections between SBS, ρ-backdoors, and the corresponding backdoor trees, and establish some new theoretical properties of backdoor trees. In the experimental part of the paper, we show that moving from the metaheuristic search for ρ-backdoors to that of ρ-backdoor trees allows drastically reducing the time required to construct the required decompositions without compromising their quality.

The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set (SBS) concept applied to the Boolean Satisfiability Problem (SAT). We call a set of Boolean variables B a ρ-backdoor, if for a fraction of at least ρ of possible assignments of variables from B, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas. Clearly, a ρ-backdoor with ρ=1 is an SBS. For a given set B it is possible to efficiently construct an (ε, δ)-approximation of parameter ρ using the Monte Carlo method. Thus, we define an (ε, δ)-SBS as such a set B for which the conclusion "parameter ρ deviates from 1 by no more than ε" is true with probability no smaller than 1 - δ. We consider the problems of finding the minimum SBS and the minimum (ε, δ)-SBS. To solve the former problem, one can use the algorithm described by R. Williams, C. Gomes and B. Selman in 2003. In the paper we propose a new probabilistic algorithm to solve the latter problem, and show that the asymptotic estimation of the worst-case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams et al. For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal (ε, δ)-SBS. Results of computational experiments show that the use of (ε, δ)-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.

In this work we propose an asynchronous parallel evolutionary algorithm that is efficient for a specific type of gray-box optimization problems, in which the calculation of the fitness function may be split into a set of several independent calculations. An example of such an optimization problem is the search for backdoors (hidden structures) in the Boolean satisfiability problem: subsets of variables that allow an efficient splitting of the problem into a set of independent subproblems. Our experiments show that the proposed asynchronous approach allows speeding up the algorithm considerably, while also effi-ciently utilizing comnuting cluster time.

Model checking allows rigorously checking the compliance of a software model with a given formal specification described with temporal logics. In control applications, model checking is used for formal verification of controller code, and temporal logic is used as a formal specification language. However, not all industrial projects start with the creation of a formal specification. On the contrary, often model checking is introduced at later stages of project development, and formal specifications need to be written for already existing legacy code.In this work we developed a framework for automating the process of formal specification preparation for IEC 61499 function blocks, a programming language used in the area of industrial automation. The developed framework is based on multiobjective evolutionary algorithms and model checking, and allows inference of linear temporal logic formulas for basic IEC 61499 function blocks. Our experiments show that the temporal specifications generated by the proposed framework sufficiently approximate existing, manually prepared specifications.

Propositional satisfiability (SAT) solvers are deemed to be among the most efficient reasoners, which have been successfully used in a wide range of practical applications. As this contrasts the well-known NP-completeness of SAT, a number of attempts have been made in the recent past to assess the hardness of propositional formulas in conjunctive normal form (CNF). The present paper proposes a CNF formula hardness measure which is close in conceptual meaning to the one based on Backdoor set notion: in both cases some subset B of variables in a CNF formula is used to define the hardness of the formula w.r.t. this set. In contrast to the backdoor measure, the new measure does not demand the polynomial decidability of CNF formulas obtained when substituting assignments of variables from B to the original formula. To estimate this measure the paper suggests an adaptive (ε,δ)-approximation probabilistic algorithm. The problem of looking for the subset of variables which provides the minimal hardness value is reduced to optimization of a pseudo-Boolean black-box function. We apply evolutionary algorithms to this problem and demonstrate applicability of proposed notions and techniques to tests from several families of unsatisfiable CNF formulas.

Nowadays an increasing number of industries are considering moving toward being Industry 4.0 compliant. But this transition is not straightforward: transfer to new system can lead to significant production downtime, resulting in delays and cost overruns. The best way is systematic seamless transition to newer and advanced technologies that Industry 4.0 offers. This article proposes a framework based on automatic synthesis methods that learns the behavior of an existing legacy programmable logic controller (PLC) and generates state machines that can be incorporated into IEC 61499 function blocks. Proposed algorithms are based on Boolean satisfiability (SAT) solvers. The first algorithm accepts a set of noisy PLC traces and produces a set of candidate state machines that satisfy the traces. The second algorithm accepts error-free traces and synthesizes a modular controller that may be distributed across several physical devices. The toolchain architecture is exemplified on a laboratory scale Festo mechatronic system.

Today, more and more industries are considering moving towards being Industry 4.0 compliant. But this transition is not straightforward due to many reasons: in particular, transfer to new system can lead to significant production downtime and could result in delays and cost overruns. The best way is systematic seamless transition to newer and advanced technologies that Industry 4.0 offers. This paper proposes an automated synthesis framework that learns the behavior of existing legacy and often black-box programmable logic controllers and generates state machines that can be incorporated into IEC 61499 function blocks. The paper presents the toolchain architecture and exemplifies it on a laboratory scale Festo didactic mechatronic system.

We propose a two-stage exact approach for identifying finite-state models of function blocks based on given execution traces. First, a base finite-state model is inferred with a method based on translation to the Boolean satisfiability problem, and then, the base model is generalized by inferring minimal guard conditions of the state machine with a method based on translation to the constraint satisfaction problem.

We developed an algorithm for inferring controller logic for cyber-physical systems (CPS) in the form of a state machine from given execution traces and linear temporal logic formulas. The algorithm implements an iterative counterexample-guided strategy: constraint programming is employed for constructing a minimal state machine from positive and negative traces (counterexamples) while formal verification is used for discovering new counterexamples. The proposed approach extends previous work by (1) considering a more intrinsic model of a state machine making the algorithm applicable to synthesizing CPS controller logic, and (2) using closed-loop verification which allows considering more expressive temporal properties.

As the world becomes more and more automated, the degree of cyber-physical systems involvement cannot be overestimated. A large part of them are safety-critical, thus, it is especially important to ensure their correctness before start of operation or reconfiguration. For this purpose the model checking approach should be used since it allows rigorously proving system correctness by checking all possible states. To ensure the compliance of controller-plant properties with system requirements, the closed-loop verification approach should be chosen, which requires not only a formal model of the controller, but also a formal model of the plant. In this paper we propose an approach for constructing formal models of context-free deterministic plants automatically using active learning algorithms. The case study shows its successful application to plant model generation for the elevator cyber-physical system.

Cyber-physical systems are spread among multiple domains of human activity. Their behavior should be strictly validated as most of them are critical. One perspective direction of ensuring system correctness is verification using model checking. A new method for closed-loop model checking of cyber-physical systems has recently been introduced that involves automatic formal plant model synthesis followed by temporal properties verification. The formal model is inferred based on traces gathered from the simulation model. Then, verification of temporal properties for the whole closed-loop system can be performed using the NuSMV tool. The main purpose of this paper is to investigate the applicability of the aforementioned method by performing a case study on the example of a compensating group drive simulation model provided by our industrial partners.

Cyber-physical system correctness can be ensured by employing formal methods, including model inference. A rather new direction of research is using formal plant models for closed-loop verification and inferring these models from execution traces of the system. Since the quality of the resulting model heavily depends on trace coverage, in this paper we propose efficient methods for automatic plant trace generation. A method of checking the conformance between system and generated models is suggested and is used to analyze traces generation and model inference methods. Modifications of plant model inference approaches are proposed and comparison of the resulting models is performed.

A method for inferring finite-state models of function blocks from given execution traces based on translation to the constraint satisfaction problem (CSP) is proposed. In contrast to the previous method based on a metaheuristic algorithm, the approach suggested in this paper is exact: it allows to find a solution if it exists or to prove the opposite. The proposed method is evaluated on the example of constructing a finite-state model of a controller for a Pick-and-Place manipulator and is shown to be significantly faster then the metaheuristic algorithm.

An approach for automatic reconstruction of automation logic from execution scenarios using a metaheuristic algorithm is proposed. IEC 61499 basic function blocks are chosen as implementation language and reconstruction of Execution Control Charts for basic function blocks is addressed. The synthesis method is based on a metaheuristic algorithm that combines ideas from ant colony optimization and evolutionary computation. Execution scenarios can be recorded from testing legacy software solutions. At this stage results are only limited to generation of basic function blocks having only Boolean input/output variables.

The paper addresses the problem of reverse engineering a function block (FB) in situations when its source code is either not available or is too complex to understand. The proposed approach builds up on a recent method for reconstructing FBs based on testing and a search-based optimization algorithm. In our work the method is augmented with candidate solution verification using the NuSMV model checker. Verification is done in a closed-loop way using a manually constructed surrogate model of the plant and environment.

This paper presents an approach for automatic reconstruction of automation logic from execution scenarios using a metaheuristic algorithm. The IEC 61499 basic function blocks is chosen as implementation language and reconstruction of Execution Control Charts for basic function blocks is addressed. The synthesis method is based on a metaheuristic algorithm most closely related to ant colony optimization and evolutionary computation. Execution scenarios can be recorded from testing legacy software solutions. At this stage results are only limited to generation of basic function blocks having only Boolean input/output variables.

This paper addresses the problem of learning extended finite-state machines (EFSMs) from user-specified behavior examples (test scenarios) and temporal properties. We show how to combine exact EFSM inference algorithms (that always find a solution if it exists) and metaheuristics to derive an efficient combined EFSM learning algorithm. We also present a new exact EFSM inference algorithm based on Constraint Satisfaction Problem (CSP) solvers. Experimental results are reported showing that the new combined algorithm significantly outperforms a previously used metaheuristic.

In this paper we present MuACOsm - a new method of learning Finite-State Machines (FSM) based on Ant Colony Optimization (ACO) and a graph representation of the search space. The input data is a set of events, a set of actions and the number of states in the target FSM. The goal is to maximize the given fitness function, which is defined on the set of all FSMs with given parameters. The new algorithm is compared with evolutionary algorithms and a genetic programming related approach on the well-known Artificial Ant problem.

This paper is dedicated to the problem of learning finite-state machines (FSMs), which plays a key role in automata-based programming. Metaheuristic algorithms commonly applied to this problem often use FSM mutations (small changes in the FSM structure) for solution construction. Most of them do not employ the specifics of FSMs in their work. We propose a new simple method for improving performance of these algorithms. The basic idea is to mark those transitions of FSMs that were used during fitness evaluation. Then, if a FSM mutation changes a transition that was not used in fitness evaluation, the fitness function value need not be calculated for the mutated FSM. This observation allows to conserve fitness evaluations, which often have high computational costs. The proposed method has been incorporated into several traditional and recent FSM learning algorithms based on evolutionary strategies, genetic algorithms and ant colony optimization. Experimental results are reported showing that the new method significantly improves performance of two methods based on evolutionary strategies and ant colony optimization.