14 citations · 31 across the 13 of their papers we have counts for
14 papers
FormIDEAble: Safe and Socially-aware Autonomous Systems
Livia Lestingi, Amel Bennaceur, Marcello M. Bersani +5
Autonomous agents operating in socio-critical settings must coordinate with humans under uncertainty while respecting explicit safety constraints. Existing approaches either accoun…
Automated Detection and Mitigation of Dependability Failures in Healthcare Scenarios through Digital Twins
Bruno Guindani, Matteo Camilli, Livia Lestingi +1
Medical Cyber-Physical Systems (CPSs) integrating Patients, Devices, and healthcare personnel (Physicians) form safety-critical PDP triads whose dependability is challenged by syst…
On Decidability Timed Automata with 2 Parametric Clocks
Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the…
Improved Bounded Model Checking of Timed Automata
Robert L. Smith, Marcello M. Bersani, Matteo Rossi +1
Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usua…
Statistical Model Checking of Human-Robot Interaction Scenarios
Livia Lestingi, Mehrnoosh Askarpour, Marcello M. Bersani +1
Robots are soon going to be deployed in non-industrial environments. Before society can take such a step, it is necessary to endow complex robotic systems with mechanisms that make…
Verifying MITL formulae on Timed Automata considering a Continuous Time Semantics
Claudio Menghi, Marcello Bersani, Matteo Rossi +1
Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalis…
Efficient Large-scale Trace Checking Using MapReduce
Marcello M. Bersani, Domenico Bianculli, Carlo Ghezzi +2
The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL…
Proceedings First Workshop on Logics and Model-checking for Self-* Systems
Marcello Maria Bersani, Davide Bresolin, Luca Ferrucci +1
This volume contains the proceedings of the First Workshop on Logics and Model-checking for self-* systems (MOD* 2014). The worshop took place in Bertinoro, Italy, on 12th of Septe…
An LTL Semantics of Business Workflows with Recovery
Luca Ferrucci, Marcello M. Bersani, Manuel Mazzara
We describe a business workflow case study with abnormal behavior management (i.e. recovery) and demonstrate how temporal logics and model checking can provide a methodology to ite…
Deciding the Satisfiability of MITL Specifications
Marcello Maria Bersani, Matteo Rossi, Pierluigi San Pietro
In this paper we present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL th…
Constraint LTL Satisfiability Checking without Automata
Marcello M. Bersani, Achille Frigeri, Angelo Morzenti +3
This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with Both future and past operators and atomic for…
Bounded Reachability for Temporal Logic over Constraint Systems
Marcello M. Bersani, Achille Frigeri, Angelo Morzenti +3
We present CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. Even for decidable constraint…
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
Marcello M. Bersani, Luca Cavallaro, Achille Frigeri +2
An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a d…
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms
Marcello M. Bersani, Carlo A. Furia, Matteo Pradella +1
Complex systems typically have many different parts and facets, with different characteristics. In a multi-paradigm approach to modeling, formalisms with different natures are used…