WP1:Verification, Synthesis, and Autonomy
Task Lead: FBK, PI: Alessandro Cimatti, Co-PI: Roberto Sebastiani
We will research algorithms and tools for automated reasoning, optimization, verification and validation, synthesis and planning for highly expressive logical formalisms. The purpose is to increase automation and efficiency by integrating heterogeneous symbolic and subsymbolic approaches to AI. The foundations of trustworthy autonomous architectures will be investigated.
Connected to TP Adjustable Autonomy and Physical Embodied Intelligence (TP4).
Effort 36p/m + cascading funds.
Description of work
Task 2.1.1 - Automated Reasoning, Enumeration/counting and Optimization Task leader: Roberto Sebastiani
The goal of this task is to develop the core backend reasoning engines. The reference framework is Satisfiability Modulo Theories (SMT), that combines numerical and Boolean reasoning to achieve expressiveness and automation. We will improve the efficiency in current SMT-solving procedures for the theories of interest; we will investigate and develop novel efficient SMT procedures for non-linear arithmetic with transcendental functions, and for Rectified Linear Units (ReLUs), a fundamental ingredient of Neural Networks (NNs). Important extensions of SMT will also be investigated: the effective and efficient enumeration/counting of all assignments/models of an SMT formula (AllSMT/#SMT), and Weighted Model Integration (WMI), a procedure for probabilistic reasoning, combining AllSMT and numerical integration; the capability of finding efficiently optimal models for SMT formulas wrt. objective functions (Optimization Modulo Theories, OMT), providing the capability to handle formulas & objectives in non-linear arithmetic with transcendental functions and on ReLUs.
Remarkably, all these procedures will combine symbolic reasoning (e.g. SAT, Computer Algebra) with sub-symbolic procedures (e.g. linear programming, numerical solving and optimization, numerical integration). We will also investigate an integration of these procedures with reinforcement learning procedures.
Task 2.1.2 Formal Verification, Planning and Synthesis Task leader: Alessandro Cimatti
The goal of this task is to investigate techniques and tools for the analysis of dynamical models, describing the behavior over time of complex systems. The activity is set in the framework of model checking, where behaviors are modeled by means of transition systems and temporal logics. An integration of heterogeneous reasoning engines is necessary to increase expressiveness to model cyber-physical systems equipped with complex data structures, timing constraints, continuous dynamics and resource consumption. Several challenges will be tackled.
The first one is the development of automated reasoning engines able to deal with the exploration of large state spaces, using abstraction/refinement and hierarchical decomposition; particularly interesting are complete or probabilistic verification procedures for recurrent Neural Networks, exploiting SMT on ReLUs and WMI.
The second challenge is the definition of procedures for the analysis of highly parameterized systems and requirements, where the space of possible features is formally described with ontologies, and to leverage heterogeneous approaches to devise possible/ optimal configurations, and analysis of fault propagation and safety assessment.
The third challenge is to investigate the problems of automatic synthesis of design models from specifications, and temporal planning under resource constraints.
The fourth challenge is to investigate the problem of synthesis of input programs for quantum annealers/computers to solve computationally hard problems (e.g. SAT, prime factorization).
Task 2.1.3 – Reasoning, Verification & Synthesis for Autonomy Task leader: Alessandro Cimatti
The goal is to integrate several reasoning techniques within a trustworthy autonomous architecture. The trustworthiness of the architecture will rely on the logical reasoning methods by combining off-line self-certifying design methods, and on numerical, run-time verification for model alignment. The architecture will be able to generate suitable action plans from goals, monitor the execution, detect and identify faults, and plan for appropriate reconfiguration. It will include features like model discovery, diagnosis and the ability to explain the choices to support mix-initiative operation.
The resulting functions will be integrated and evaluated in the realization of digital twins and AI-based architectures for autonomy.
The activities of the work package will be arranged along three different but related dimensions: research results, development of assets, and applications.
The research activities will include the investigation of the following topics.
● Foundations and reasoning algorithms for SMT, AllSMT, OMT, WMI.
● Foundations and reasoning algorithms for probabilistic reasoning, and the probabilistic verification of DNN.
● Algorithms for abstraction of infinite-state transition systems, and for the effective verification of invariant and temporal properties. The algorithms will be equipped with the ability to produce proofs that can be independently verified to address the tool qualification problem.
● Algorithms for the synthesis of reactive modules from temporal logic specifications, with particular reference to the framework of contract-based design.
● Algorithms for the specification, verification and synthesis of Fault Detection, Identification and Recovery (FDIR) modules in a distributed setting. The problem will be tackled by resorting to a framework on multi-agent temporal epistemic logic.
● Algorithms for temporal planning based on reinforcement learning.
The asset-related activities will include the implementation of the proposed algorithms, resulting in the development, maintenance and enhancement of new and existing software systems:
● SMT/AllSMT and OMT: MathSAT (https://mathsat.fbk.eu/) and OptiMathSAT (https://optimathsat.disi.unitn.it/)
● WMI and probabilistic reasoning: pyWMI (https://pypi.org/project/pywmi/)
● Formal verification: nuXmv (https://nuxmv.fbk.eu/), Kratos (https://kratos.fbk.eu/), HyCOMP (https://hycomp.fbk.eu/), OCRA (https://ocra.fbk.eu/).
● Planning and Synthesis: TAMER (https://tamer.fbk.eu/), UPF (https://github.com/aiplan4eu/unified-planning).
● Design of autonomous systems: COMPASS (https://www.compass-toolset.org/), TASTE (https://taste.tools/)
In order to experimentally validate the proposed techniques, the activity will include the experimentation of practical case studies, derived in specific application domain, including:
● Abstraction for reengineering of legacy control software
● Automatic problem compilation for Quantum Annealing
● Verification of critical railways interlocking systems
● Safety assessment, Fault propagation, FDIR, diagnosis of aerospace systems
● Temporal planning for factory automation and optimization