Ezio Bartocci

ICML Conference 2025 Conference Paper

Exact Upper and Lower Bounds for the Output Distribution of Neural Networks with Random Inputs

• Andrey Kofnov
• Daniel Kapla
• Ezio Bartocci
• Efstathia Bura

We derive exact upper and lower bounds for the cumulative distribution function (cdf) of the output of a neural network (NN) over its entire support subject to noisy (stochastic) inputs. The upper and lower bounds converge to the true cdf over its domain as the resolution increases. Our method applies to any feedforward NN using continuous monotonic piecewise twice continuously differentiable activation functions (e. g. , ReLU, tanh and softmax) and convolutional NNs, which were beyond the scope of competing approaches. The novelty and instrumental tool of our approach is to bound general NNs with ReLU NNs. The ReLU NN-based bounds are then used to derive the upper and lower bounds of the cdf of the NN output. Experiments demonstrate that our method delivers guaranteed bounds of the predictive output distribution over its support, thus providing exact error guarantees, in contrast to competing approaches.

ECAI Conference 2025 Conference Paper

OFTEN-DEEPRL: On-the-Fly Teaching of Ethical Norms to Deep Reinforcement Learning Agents

• Ignacio D. Lopez-Miguel
• Sebastian P. Adam
• Ezio Bartocci
• Thomas Eiter
• Martin Tappler

AI agents trained with reinforcement learning (RL) usually focus on completing their intended tasks without detours, as doing so typically maximizes their reward. However, real-world deployment requires agents that not only achieve their goals but also comply with ethical and societal norms that may conflict with their learned behavior. In this work, we present OFTEN-DEEPRL, an approach to integrate ethical norms into agents trained with deep reinforcement learning. The approach starts by training an RL policy focused on task performance. Building upon such a pre-trained policy, OFTEN-DEEPRL adapts the policy through norm-guided training. For a combination of observations and domain knowledge, we employ a logic program that generates norm-compliant plans for the agent using answer set programming (ASP) within a given planning horizon. These plans serve as demonstrations for fine-tuning the agent’s policy in the norm-guided training phase, guiding it toward behavior that remains effective while respecting the specified norms. We validate our approach with three types of scenarios: Pac-Man, a gardener simulation, and a SUMO-RL traffic control scenario. In all settings, agents fine-tuned with OFTEN-DEEPRL achieve comparable task performance while significantly reducing norm violations.

IJCAI Conference 2025 Conference Paper

Rule-Guided Reinforcement Learning Policy Evaluation and Improvement

• Martin Tappler
• Ignacio D. Lopez-Miguel
• Sebastian Tschiatschek
• Ezio Bartocci

We consider the challenging problem of using domain knowledge to improve deep reinforcement learning policies. To this end, we propose LEGIBLE, a novel approach, following a multi-step process, which starts by mining rules from a deep RL policy, constituting a partially symbolic representation. These rules describe which decisions the RL policy makes and which it avoids making. In the second step, we generalize the mined rules using domain knowledge expressed as metamorphic relations. We adapt these relations from software testing to RL to specify expected changes of actions in response to changes in observations. The third step is evaluating generalized rules to determine which generalizations improve performance when enforced. These improvements show weaknesses in the policy, where it has not learned the general rules and thus can be improved by rule guidance. LEGIBLE supported by metamorphic relations provides a principled way of expressing and enforcing domain knowledge about RL environments. We show the efficacy of our approach by demonstrating that it effectively finds weaknesses, accompanied by explanations of these weaknesses, in eleven RL environments and by showcasing that guiding policy execution with rules improves performance w. r. t. gained reward.

ECAI Conference 2023 Conference Paper

Progression for Monitoring in Temporal ASP

• Davide Soldà
• Ignacio D. Lopez-Miguel
• Ezio Bartocci
• Thomas Eiter

In recent years, there has been growing interest in the application of temporal reasoning approaches and non-monotonic logics from artificial intelligence in dynamic systems that generate data. A well-known approach to temporal reasoning is the use of a progression technique, which allows for the online computation of logical consequences of a logical knowledge base over time. We consider a progression technique for Temporal Here and There and Temporal Equilibrium Logic, which is the logic underlying answer programming over linear-temporal logic (LTL). Compared to usual LTL online computation, where the goal is to check whether a trace is compliant with a temporal specification, our approach provides also the means to compute non-monotonic temporal reasoning over a trace of observations. Besides formal notions and results, we also present an algorithm for performing progression to monitor a dynamic system, which has been implemented as a proof of concept and allows for handling expressive application scenarios.

I&C Journal 2022 Journal Article

Model checking hyperproperties for Markov decision processes

• Oyendrila Dobe
• Erika Ábrahám
• Ezio Bartocci
• Borzoo Bonakdarpour

We study the problem of formalizing and checking probabilistic hyperproperties for Markov decision processes (MDPs). We introduce the temporal logic HyperPCTL that allows explicit and simultaneous quantification over schedulers as well as probabilistic computation trees. We show that the logic can express important quantitative requirements in security and privacy such as probabilistic noninterference, differential privacy, timing side-channel countermeasures, and probabilistic conformance testing. We show that HyperPCTL model checking over MDPs is in general undecidable, but restricting the domain of scheduler quantification to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language. Finally, we demonstrate the applicability of our method by providing experimental results for verification, and we show how it can be used to solve even certain synthesis problems.

TCS Journal 2022 Journal Article

Moment-based analysis of Bayesian network properties

• Miroslav Stankovič
• Ezio Bartocci
• Laura Kovács

We use algebraic reasoning to translate Bayesian network (BN) properties into linear recurrence equations over statistical moments of BN variables. We show that this translation can always be done for various BNs, such as discrete, Gaussian, conditional linear Gaussian, and dynamic BNs. An important part of our work comes with representing BNs as while loops in probabilistic programs with polynomial assignments over random variables and parametrised distributions. We prove that closed-form summaries of probabilistic loops precisely characterize higher-order moments of BN variables. As such, we automatically solve several BN-related problems, including exact inference, sensitivity analysis, filtering, and computing the expected number of rejecting samples in sampling-based procedures. We evaluate our work on a number of BN benchmarks, using automated invariant generation within Prob-solvable loop analysis. This paper is an extended version of the “Analysis of Bayesian Networks via Prob-Solvable Loops” manuscript published at ICTAC 2020 [1].

I&C Journal 2022 Journal Article

Survey on mining signal temporal logic specifications

• Ezio Bartocci
• Cristinel Mateis
• Eleonora Nesterini
• Dejan Nickovic

Formal specifications play an essential role in the life-cycle of modern systems, both at the time of their design and during their operation. Despite their importance, formal specifications are only partially (if at all) available. Specification mining is the process of learning likely system properties from the observation of its behavior and its interaction with the environment. Signal temporal logic (STL) is a popular formalism for expressing properties of cyber-physical systems (CPS). In the last decade, the introduction of first methods for mining STL specifications from time series generated by CPS led to a new vivid area of research. This survey paper overviews methods for mining STL specifications from CPS behaviors, sketches different approaches found in the literature and presents them in an intuitive and didactic manner. It aims at presenting the most influential techniques and covers most important aspects of specification mining: template-based vs. template-free, model-based vs. model-free, passive vs. active, and supervised vs. unsupervised learning.

LPAR Conference 2020 Conference Paper

Parameter Synthesis for Probabilistic Hyperproperties

• Erika Ábrahám
• Ezio Bartocci
• Borzoo Bonakdarpour
• Oyendrila Dobe

In this paper, we study the parameter synthesis problem for probabilistic hyperproper- ties. A probabilistic hyperproperty stipulates quantitative dependencies among a set of executions. In particular, we solve the following problem: given a probabilistic hyperprop- erty ψ and discrete-time Markov chain D with parametric transition probabilities, compute regions of parameter configurations that instantiate D to satisfy ψ, and regions that lead to violation. We address this problem for a fragment of the temporal logic HyperPCTL that allows expressing quantitative reachability relation among a set of computation trees. We illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance.

TCS Journal 2015 Journal Article

Model-order reduction of ion channel dynamics using approximate bisimulation

• Md. Ariful Islam
• Abhishek Murthy
• Ezio Bartocci
• Elizabeth M. Cherry
• Flavio H. Fenton
• James Glimm
• Scott A. Smolka
• Radu Grosu

We show that in the context of the Iyer et al. (IMW) 67-variable cardiac myocycte model, it is possible to replace the detailed 13-state probabilistic subsystem of the sodium channel dynamics with a much simpler Hodgkin-Huxley (HH)-like two-state abstraction, while only incurring a bounded approximation error. We then extend our technique to the 10-state subsystem of the fast-recovering calcium-independent potassium channel. The basis of our results is the construction of an approximate bisimulation between the HH-type abstraction and the corresponding detailed ion channel model, both of which are input-controlled (voltage in this case) CTMCs. The construction of the appropriate approximate bisimulation, as well as the overall result regarding the behavior of this modified IMW model, involves: (1) Identification of the voltage-dependent parameters of the m and h gates in the HH-type models via a two-step fitting process, carried out over more than 20, 000 representative observational traces of the detailed sodium and potassium ion channel models. (2) Proving that the distance between observations of the detailed models and their respective abstraction is bounded. (3) Exploring the sensitivity of the overall IMW model to the HH-type approximations. Our extensive simulation results experimentally validate our findings, for varying IMW-type input stimuli.

TCS Journal 2015 Journal Article

System design of stochastic models using robustness of temporal properties

• Ezio Bartocci
• Luca Bortolussi
• Laura Nenzi
• Guido Sanguinetti

Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem, i. e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to maintain a particular emergent behaviour unaffected by the perturbations, caused e. g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness degrees. By discussing three examples, we show how to approximate the distribution of the robustness degree and the average robustness. Secondly, we show how to exploit this notion to address the system design problem, where the goal is to optimise some control parameters of a stochastic model in order to maximise robustness of the desired specifications.

I&C Journal 2014 Journal Article

Hybrid Systems and Biology

• Ezio Bartocci
• Luca Bortolussi
• Scott A. Smolka

TCS Journal 2010 Journal Article

Detecting synchronisation of biological oscillators by model checking

• Ezio Bartocci
• Flavio Corradini
• EMANUELA MERELLI
• Luca Tesei

We define a subclass of timed automata, called oscillator timed automata, suitable to model biological oscillators. Coupled biological oscillators may synchronise, as emerging behaviour, after a period of time in which they interact through physical or chemical means. We introduce a parametric semantics for their interaction that is general enough to capture the behaviour of different types of oscillators. We instantiate it both to the Kuramoto model, a model of synchronisation based on smooth interaction, and to the Peskin model of pacemaker cells in the heart, a model of synchronisation based on pulse interaction. We also introduce a logic, Biological Oscillators Synchronisation Logic (BOSL), that is able to describe collective synchronisation properties of a population of coupled oscillators. A model checking algorithm is proposed for the defined logic and it is implemented in a model checker. The model checker can be used to detect synchronisation properties of a given population of oscillators. This tool might be the basic step towards the generation of suitable techniques to control and regulate the behaviour of coupled oscillators in order to ensure the reachability of synchronisation.