Matteo Zavatteri

ECAI Conference 2024 Conference Paper

Automated Synthesis of Certified Neural Networks

• Matteo Zavatteri
• Davide Bresolin
• Nicolò Navarin

Neural networks find applications in many safety-critical systems that raise concerns about their deployment: Are we sure the network will never advise doing anything violating a set of safety constraints? Formal verification has been recently applied to prove whether an existing neural network is certified for some property (i. e. , if it satisfies the property for all possible inputs) or not. Formal verification can prove that a network respects the property, but cannot fix a network that does not respect it. In this paper we focus on the automated synthesis of certified neural networks, that is, on how to automatically build a network that is guaranteed to respect some required properties. We exploit a Counter Example Guided Inductive Synthesis (CEGIS) loop that alternates Deep Learning, Formal Verification, and a novel data generation technique that augments the training data to synthesize certified networks in a fully automatic way. An application of a proof-of-concept implementation of the framework shows the feasibility of the approach.

I&C Journal 2023 Journal Article

Reducing the number of disjuncts in DTPs

• Alice Raffaele
• Matteo Zavatteri

The Disjunctive Temporal Problem (DTP) consists of a finite set of time points and a finite set of constraints, each composed of alternative disjuncts modeling delays and deadlines for possibly different pairs of time points. An instance of DTP is consistent if there exists an assignment of real values to the time points such that all constraints are satisfied. Here we focus on DTPs with at most k ≥ 2 disjuncts per constraint. We define a few polynomial-time encoders to reduce the number of disjuncts to at most k ′, with 2 ≤ k ′ ≤ k, preserving (in)consistency of the original instance. These results generalize previous work in the literature. Anyway, we provide a methodology not related to any specific technology that sticks to DTP.

I&C Journal 2021 Journal Article

Consistency checking of STNs with decisions: Managing temporal and access-control constraints in a seamless way

• Matteo Zavatteri
• Carlo Combi
• Romeo Rizzi
• Luca Viganò

A Simple Temporal Network (STN) consists of time points modeling temporal events and constraints modeling the minimal and maximal temporal distance between them. A Simple Temporal Network with Decisions (STND) extends an STN to model temporal plans with decisions. STNDs label time points and constraints by conjunctions of literals saying for which scenarios (i. e. , complete truth value assignments to the propositions) they are relevant. In this paper, we deal with the use of STNDs for modeling and synthesizing execution strategies. We propose an incremental hybrid SAT-based consistency checking algorithm for STNDs that is faster than the one previously proposed and allows for the synthesis of all consistent scenarios and related early execution schedules (offline temporal planning). We carry out an experimental evaluation with Kappa, a tool that we developed for STNDs. We also show that any STND can be easily translated into a disjunctive temporal network and vice versa.

AAAI Conference 2021 Conference Paper

Faster and Better Simple Temporal Problems

• Dario Ostuni
• Alice Raffaele
• Romeo Rizzi
• Matteo Zavatteri

In this paper we give a structural characterization and extend the tractability frontier of the Simple Temporal Problem (STP) by defining the class of the Extended Simple Temporal Problem (ESTP), which augments STP with strict inequalities and monotone Boolean formulae on inequations (i. e. , formulae involving the operations of conjunction, disjunction and parenthesization). A polynomial-time algorithm is provided to solve ESTP, faster than previous state-of-the-art algorithms for other extensions of STP that had been considered in the literature, all encompassed by ESTP. We show the practical competitiveness of our approach through a proof-ofconcept implementation and an experimental evaluation involving also state-of-the-art SMT solvers.

I&C Journal 2021 Journal Article

Mining CSTNUDs significant for a set of traces is polynomial

• Guido Sciavicco
• Matteo Zavatteri
• Tiziano Villa

A Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism for temporal plans that models controllable and uncontrollable durations as well as controllable and uncontrollable choices simultaneously. In the classic top-down model-based engineering approach, a designer builds CSTNUDs to model, validate and execute some temporal plans of interest. In this paper, we investigate a bottom-up approach by providing a deterministic polynomial time algorithm to mine a CSTNUD from a set of execution traces (i. e. , a log). We provide a prototype implementation and we test it with a set of artificial data. Finally, we elaborate on consistency and controllability of mined networks.

ICAPS Conference 2020 Conference Paper

Dynamic Controllability and (J, K)-Resiliency in Generalized Constraint Networks with Uncertainty

• Matteo Zavatteri
• Romeo Rizzi
• Tiziano Villa

A number of formal models have been proposed to address temporal and resource allocation problems under uncertainty. Such models are typically shipped with an embedded notion of dynamic controllability, enclosing the ability to always make the right decisions, during execution, according to the observed uncontrollable events that always happen. In the business process management community, resource allocation was recently studied to deal with uncontrollable choices, whereas in the security community it was studied to face the uncontrollable availability of resources. The latter is a kind of dynamic controllability known as resiliency where uncontrollable events might also not happen. To the best of our knowledge, approaches handling resiliency on top of dynamic controllability still remain unexplored. To bridge this gap, we propose Generalized Constraint Networks with Uncertainty (GCNUs), a model that we devised to address resource controllability more widely, boosting expressiveness while considering several sources of uncertainty simultaneously. We define dynamic controllability and (J, K)-resiliency of GCNUs. We reason on the structure of these problems, carry out a complexity analysis and provide algorithms to solve them.

TIME Conference 2020 Conference Paper

Mining Significant Temporal Networks Is Polynomial

• Guido Sciavicco
• Matteo Zavatteri
• Tiziano Villa

A Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism that tackles controllable and uncontrollable durations as well as controllable and uncontrollable choices simultaneously. In the classic top-down model-based engineering approach, a designer builds a CSTNUD to model, validate and execute some temporal plan of interest. Instead, in this paper, we investigate the bottom-up approach by providing a deterministic polynomial time algorithm to mine a CSTNUD from a set of execution traces (i. e. , a log). This paper paves the way for the design of controllable temporal networks mined from traces that also contain information on uncontrollable events.

OVERLAY Workshop 2019 Workshop Paper

Complexity of Weak, Strong and Dynamic Controllability of CNCUs

• Matteo Zavatteri
• Romeo Rizzi
• Tiziano Villa

TCS Journal 2019 Journal Article

Conditional simple temporal networks with uncertainty and decisions

• Matteo Zavatteri
• Luca Viganò

A Conditional Simple Temporal Network with Uncertainty (CSTNU) is a formalism able to model temporal plans subject to both conditional constraints and uncertain durations. The combination of these two characteristics represents the uncontrollable part of the network. That is, before the network starts executing, we do not know completely which time points and constraints will be taken into consideration nor how long the uncertain durations will last. Dynamic Controllability (DC) implies the existence of a strategy scheduling the time points of the network in real time depending on how the uncontrollable part behaves. Despite all this, CSTNUs fail to model temporal plans in which a few conditional constraints are under control and may therefore influence (or be influenced by) the uncontrollable part. To bridge this gap, this paper proposes Conditional Simple Temporal Networks with Uncertainty and Decisions (CSTNUDs) which introduce decision time points into the specification in order to operate on this conditional part under control. We model the dynamic controllability checking (DC-checking) of a CSTNUD as a two-player game in which each player makes his moves in his turn at a specific time instant. We give an encoding into timed game automata for a sound and complete DC-checking. We also synthesize memoryless execution strategies for CSTNUDs proved to be DC and carry out an experimental evaluation with Image 1, a tool that we have designed for CSTNUDs to make the approach fully automated.

JAIR Journal 2019 Journal Article

Conditional Simple Temporal Networks with Uncertainty and Resources

• Carlo Combi
• Roberto Posenato
• Luca Viganò
• Matteo Zavatteri

Conditional simple temporal networks with uncertainty (CSTNUs) allow for the representation of temporal plans subject to both conditional constraints and uncertain durations. Dynamic controllability (DC) of CSTNUs ensures the existence of an execution strategy able to execute the network in real time (i.e., scheduling the time points under control) depending on how these two uncontrollable parts behave. However, CSTNUs do not deal with resources. In this paper, we define conditional simple temporal networks with uncertainty and resources (CSTNURs) by injecting resources and runtime resource constraints (RRCs) into the specification. Resources are mandatory for executing the time points and their availability is represented through temporal expressions, whereas RRCs restrict resource availability by further temporal constraints among resources. We provide a fully-automated encoding to translate any CSTNUR into an equivalent timed game automaton in polynomial time for a sound and complete DC-checking.

TIME Conference 2019 Conference Paper

Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions

• Matteo Zavatteri
• Carlo Combi
• Romeo Rizzi
• Luca Viganò 0001

A Simple Temporal Network (STN) consists of time points modeling temporal events and constraints modeling the minimal and maximal temporal distance between them. A Simple Temporal Network with Decisions (STND) extends an STN by adding decision time points to model temporal plans with decisions. A decision time point is a special kind of time point that once executed allows for deciding a truth value for an associated Boolean proposition. Furthermore, STNDs label time points and constraints by conjunctions of literals saying for which scenarios (i. e. , complete truth value assignments to the propositions) they are relevant. Thus, an STND models a family of STNs each obtained as a projection of the initial STND onto a scenario. An STND is consistent if there exists a consistent scenario (i. e. , a scenario such that the corresponding STN projection is consistent). Recently, a hybrid SAT-based consistency checking algorithm (HSCC) was proposed to check the consistency of an STND. Unfortunately, that approach lacks experimental evaluation and does not allow for the synthesis of all consistent scenarios. In this paper, we propose an incremental HSCC algorithm for STNDs that (i) is faster than the previous one and (ii) allows for the synthesis of all consistent scenarios and related early execution schedules (offline temporal planning). Then, we carry out an experimental evaluation with KAPPA, a tool that we developed for STNDs. Finally, we prove that STNDs and disjunctive temporal networks (DTNs) are equivalent.

OVERLAY Workshop 2019 Workshop Paper

Strong Controllability of Temporal Networks with Decisions

• Matteo Zavatteri
• Romeo Rizzi
• Tiziano Villa

TIME Conference 2017 Conference Paper

Conditional Simple Temporal Networks with Uncertainty and Decisions

• Matteo Zavatteri

A conditional simple temporal network with uncertainty (CSTNU) is a framework able to model temporal plans subject to both conditional constraints and uncertain durations. The combination of these two characteristics represents the uncontrollable part of the network. That is, before the network starts executing, we do not know completely which time points and constraints will be taken into consideration nor how long the uncertain durations will last. Dynamic controllability (DC) implies the existence of a strategy scheduling the time points of the network in real time depending on how the uncontrollable part behaves. Despite all this, CSTNUs fail to model temporal plans in which a few conditional constraints are under control and may therefore influence (or be influenced by) the uncontrollable part. To bridge this gap, this paper proposes conditional simple temporal networks with uncertainty and decisions (CSTNUDs) which introduce decision time points into the specification in order to operate on this conditional part under control. We model the dynamic controllability checking (DC-checking) of a CSTNUD as a two-player game in which each player makes his moves in his turn at a specific time instant. We give an encoding into timed game automata for a sound and complete DC-checking. We also synthesize memoryless execution strategies for CSTNUDs proved to be DC. The proposed approach is fully automated.

TIME Conference 2017 Conference Paper

Incorporating Decision Nodes into Conditional Simple Temporal Networks

• Massimo Cairo
• Carlo Combi
• Carlo Comin
• Luke Hunsberger
• Roberto Posenato
• Romeo Rizzi
• Matteo Zavatteri

A Conditional Simple Temporal Network (CSTN) augments a Simple Temporal Network (STN) to include special time-points, called observation time-points. In a CSTN, the agent executing the network controls the execution of every time-point. However, each observation time-point has a unique propositional letter associated with it and, when the agent executes that time-point, the environment assigns a truth value to the corresponding letter. Thus, the agent observes but, does not control the assignment of truth values. A CSTN is dynamically consistent (DC) if there exists a strategy for executing its time-points such that all relevant constraints will be satisfied no matter which truth values the environment assigns to the propositional letters. Alternatively, in a Labeled Simple Temporal Network (Labeled STN) - also called a Temporal Plan with Choice - the agent executing the network controls the assignment of values to the so-called choice variables. Furthermore, the agent can make those assignments at any time. For this reason, a Labeled STN is equivalent to a Disjunctive Temporal Network. This paper incorporates both of the above extensions by augmenting a CSTN to include not only observation time-points but also decision time-points. A decision time-point is like an observation time-point in that it has an associated propositional letter whose value is determined when the decision time-point is executed. It differs in that the agent - not the environment - selects that value. The resulting network is called a CSTN with Decisions (CSTND). This paper shows that a CSTND generalizes both CSTNs and Labeled STNs, and proves that the problem of determining whether any given CSTND is dynamically consistent is PSPACE-complete. It also presents algorithms that address two sub-classes of CSTNDs: (1) those that contain only decision time-points; and (2) those in which all decisions are made before execution begins.