79 citations · 424 across the 54 of their papers we have counts for
17 papers · 1 filter
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
Luca Bortolussi, Giuseppe Maria Gallo, Jan Křetínský +1
We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a kernel function, well known in machine learning as a conceptually and compu…
MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties
Ezio Bartocci, Luca Bortolussi, Michele Loreti +2
We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile and spatially distributed cyber-physical systems (CPS). In the proposed framework, spa…
Monitoring Mobile and Spatially Distributed Cyber-Physical Systems
Ezio Bartocci, Luca Bortolussi, Michele Loreti +1
Cyber-Physical Systems~(CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and te…
Signal Convolution Logic
Simone Silvetti, Laura Nenzi, Ezio Bartocci +1
We introduce a new logic called Signal Convolution Logic (SCL) that combines temporal logic with convolutional filters from digital signal processing. SCL enables to reason about t…
Central Limit Model Checking
Luca Bortolussi, Luca Cardelli, Marta Kwiatkowska +1
We consider probabilistic model checking for continuous-time Markov chains (CTMCs) induced from Stochastic Reaction Networks (SRNs) against a fragment of Continuous Stochastic Logi…
Model Checking Markov Population Models by Stochastic Approximations
Luca Bortolussi, Roberta Lanciani, Laura Nenzi
Many complex systems can be described by population models, in which a pool of agents interacts and produces complex collective behaviours. We consider the problem of verifying for…
Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
L. Nenzi, L. Bortolussi, V. Ciancia +2
In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cybe…
An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
Simone Silvetti, Alberto Policriti, Luca Bortolussi
Search-based testing is widely used to find bugs in models of complex Cyber-Physical Systems. Latest research efforts have improved this approach by casting it as a falsification p…
Efficient Checking of Individual Rewards Properties in Markov Population Models
Luca Bortolussi, Jane Hillston
In recent years fluid approaches to the analysis of Markov populations models have been demonstrated to have great pragmatic value. Initially developed to estimate the behaviour of…
Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems
Nathalie Bertrand, Luca Bortolussi
This volume contains the proceedings of the Twelfth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2014), held in Grenoble, France, on 12 and 13 April,…
Smoothed Model Checking for Uncertain Continuous Time Markov Chains
Luca Bortolussi, Dimitrios Milios, Guido Sanguinetti
We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a sm…
Learning Temporal Logical Properties Discriminating ECG models of Cardiac Arrhytmias
Ezio Bartocci, Luca Bortolussi, Guido Sanguinetti
We present a novel approach to learn the formulae characterising the emergent behaviour of a dynamical system from system observations. At a high level, the approach starts by devi…
On the Robustness of Temporal Properties for Stochastic Models
Ezio Bartocci, Luca Bortolussi, Laura Nenzi +1
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…
A temporal logic approach to modular design of synthetic biological circuits
Ezio Bartocci, Luca Bortolussi, Laura Nenzi
We present a new approach for the design of a synthetic biological circuit whose behaviour is specified in terms of signal temporal logic (STL) formulae. We first show how to chara…
Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems
Luca Bortolussi, Herbert Wiklicky
Quantitative aspects of computation are important and sometimes essential in characterising the behavior and determining the properties of systems. They are related to the use of p…
Fluid Model Checking
Luca Bortolussi, Jane Hillston
In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the be…
HYPE with stochastic events
Luca Bortolussi, Vashti Galpin, Jane Hillston
The process algebra HYPE was recently proposed as a fine-grained modelling approach for capturing the behaviour of hybrid systems. In the original proposal, each flow or influence…