Armando Tacchella

Enrico Ghiorzi, Christian Henkel, Matteo Palmas et al.

Behavior Trees (BTs) have found a widespread adoption in robotics due to appealing features, their ease of use as a conceptual model of control policies and the availability of software tooling for BT-based design of control software. However, BTs don't have formal execution semantics and, furthermore, subtle differences among implementations can make the same model behave differently depending on the underlying software. This paper aims at defining the execution semantics of behavior trees (BTs) as used in robotics applications. To this purpose, we present an abstract data type that formalizes the structure and execution of BTs. While our formalization is inspired by existing contributions in the scientific literature and state-of-the art implementations, we strive to provide an unambiguous treatment of most features that find incomplete or inconsistent treatment across other works.

Enrico Ghiorzi, Armando Tacchella

This paper lays out the formal foundations upon which the SCAN statistical model checker is built.

Michele Colledanchise, Giuseppe Cicala, Daniele E. Domenichelli et al.

In this paper, we present a toolchain to design, execute, and verify robot behaviors. The toolchain follows the guidelines defined by the EU H2020 project RobMoSys and encodes the robot deliberation as a Behavior Tree (BT), a directed tree where the internal nodes model behavior composition and leaf nodes model action or measurement operations. Such leaf nodes take the form of a statechart (SC), which runs in separate threads, whose states perform basic arithmetic operations and send commands to the robot. The toolchain provides the ability to define a runtime monitor for a given system specification that warns the user whenever a given specification is violated. We validated the toolchain in a simulated experiment that we made reproducible in an OS-virtualization environment.

Michele Colledanchise, Giuseppe Cicala, Daniele E. Domenichelli et al.

In this paper, we enable automated property verification of deliberative components in robot control architectures. We focus on formalizing the execution context of Behavior Trees (BTs) to provide a scalable, yet formally grounded, methodology to enable runtime verification and prevent unexpected robot behaviors. To this end, we consider a message-passing model that accommodates both synchronous and asynchronous composition of parallel components, in which BTs and other components execute and interact according to the communication patterns commonly adopted in robotic software architectures. We introduce a formal property specification language to encode requirements and build runtime monitors. We performed a set of experiments, both on simulations and on the real robot, demonstrating the feasibility of our approach in a realistic application and its integration in a typical robot software architecture. We also provide an OS-level virtualization environment to reproduce the experiments in the simulated scenario.

Dario Guidotti, Luca Pulina, Armando Tacchella

In this work, we present an early prototype of NeVer 2.0, a new system for automated synthesis and analysis of deep neural networks.NeVer 2.0borrows its design philosophy from NeVer, the first package that integrated learning, automated verification and repair of (shallow) neural networks in a single tool. The goal of NeVer 2.0 is to provide a similar integration for deep networks by leveraging a selection of state-of-the-art learning frameworks and integrating them with verification algorithms to ease the scalability challenge and make repair of faulty networks possible.

Massimo Narizzano, Luca Pulina, Armando Tacchella et al.

We present a new approach to conformance testing of black-box reactive systems. We consider system specifications written as linear temporal logic formulas to generate tests as sequences of input/output pairs: inputs are extracted from the Buchi automata corresponding to the specifications, and outputs are obtained by feeding the inputs to the systems. Conformance is checked by comparing input/output sequences with automata traces to detect violations of the specifications. We consider several criteria for extracting tests and for stopping generation, and we compare them experimentally using both indicators of coverage and error-detection. The results show that our methodology can generate test suites with good system coverage and error-detection capability.

Dario Guidotti, Francesco Leofante, Luca Pulina et al.

Verification of deep neural networks has witnessed a recent surge of interest, fueled by success stories in diverse domains and by abreast concerns about safety and security in envisaged applications. Complexity and sheer size of such networks are challenging for automated formal verification techniques which, on the other hand, could ease the adoption of deep networks in safety- and security-critical contexts. In this paper we focus on enabling state-of-the-art verification tools to deal with neural networks of some practical interest. We propose a new training pipeline based on network pruning with the goal of striking a balance between maintaining accuracy and robustness while making the resulting networks amenable to formal analysis. The results of our experiments with a portfolio of pruning algorithms and verification tools show that our approach is successful for the kind of networks we consider and for some combinations of pruning and verification techniques, thus bringing deep neural networks closer to the reach of formally-grounded methods.

Arthur Bit-Monnot, Francesco Leofante, Luca Pulina et al.

Smart factories are on the verge of becoming the new industrial paradigm, wherein optimization permeates all aspects of production, from concept generation to sales. To fully pursue this paradigm, flexibility in the production means as well as in their timely organization is of paramount importance. AI is planning a major role in this transition, but the scenarios encountered in practice might be challenging for current tools. Task planning is one example where AI enables more efficient and flexible operation through an online automated adaptation and rescheduling of the activities to cope with new operational constraints and demands. In this paper we present SMarTplan, a task planner specifically conceived to deal with real-world scenarios in the emerging smart factory paradigm. Including both special-purpose and general-purpose algorithms, SMarTplan is based on current automated reasoning technology and it is designed to tackle complex application domains. In particular, we show its effectiveness on a logistic scenario, by comparing its specialized version with the general purpose one, and extending the comparison to other state-of-the-art task planners.

Francesco Leofante, Nina Narodytska, Luca Pulina et al.

Neural networks are one of the most investigated and widely used techniques in Machine Learning. In spite of their success, they still find limited application in safety- and security-related contexts, wherein assurance about networks' performances must be provided. In the recent past, automated reasoning techniques have been proposed by several researchers to close the gap between neural networks and applications requiring formal guarantees about their behavior. In this work, we propose a primer of such techniques and a comprehensive categorization of existing approaches for the automated verification of neural networks. A discussion about current limitations and directions for future investigation is provided to foster research on this topic at the crossroads of Machine Learning and Automated Reasoning.

Svyatoslav Korneev, Nina Narodytska, Luca Pulina et al.

We consider the problem of binary image generation with given properties. This problem arises in a number of practical applications, including generation of artificial porous medium for an electrode of lithium-ion batteries, for composed materials, etc. A generated image represents a porous medium and, as such, it is subject to two sets of constraints: topological constraints on the structure and process constraints on the physical process over this structure. To perform image generation we need to define a mapping from a porous medium to its physical process parameters. For a given geometry of a porous medium, this mapping can be done by solving a partial differential equation (PDE). However, embedding a PDE solver into the search procedure is computationally expensive. We use a binarized neural network to approximate a PDE solver. This allows us to encode the entire problem as a logical formula. Our main contribution is that, for the first time, we show that this problem can be tackled using decision procedures. Our experiments show that our model is able to produce random constrained images that satisfy both topological and process constraints.

Francesco Leofante, Erika Ábrahám, Tim Niemueller et al.

In manufacturing, the increasing involvement of autonomous robots in production processes poses new challenges on the production management. In this paper we report on the usage of Optimization Modulo Theories (OMT) to solve certain multi-robot scheduling problems in this area. Whereas currently existing methods are heuristic, our approach guarantees optimality for the computed solution. We do not only present our final method but also its chronological development, and draw some general observations for the development of OMT-based approaches.

Marco Menapace, Armando Tacchella

In recent years ontologies enjoyed a growing popularity outside specialized AI communities. System engineering is no exception to this trend, with ontologies being proposed as a basis for several tasks in complex industrial implements, including system design, monitoring and diagnosis. In this paper, we consider four different contributions to system engineering wherein ontologies are instrumental to provide enhancements over traditional ad-hoc techniques. For each application, we briefly report the methodologies, the tools and the results obtained with the goal to provide an assessment of merits and limits of ontologies in such domains.

Ali Khalili, Lorenzo Natale, Armando Tacchella

We consider the problem of automating the verification of distributed control software relying on publish-subscribe middleware. In this scenario, the main challenge is that software correctness depends intrinsically on correct usage of middleware components, but structured models of such components might not be available for analysis, e.g., because they are too large and complex to be described precisely in a cost-effective way. To overcome this problem, we propose to identify abstract models of middleware as finite-state automata, and then to perform verification on the combined middleware and control software models. Both steps are carried out in a computer-assisted way using state-of-the-art techniques in automata-based identification and verification. Our main contribution is to show that the combination of identification and verification is feasible and useful when considering typical issues that arise in the implementation of distributed control software.