56 citations · 114 across the 13 of their papers we have counts for
14 papers
Lecture Notes on Monadic First- and Second-Order Logic on Strings
Dino Mandrioli, Davide Martinenghi, Angelo Morzenti +2
These notes present the essentials of first- and second-order monadic logics on strings with introductory purposes. We discuss Monadic First-Order logic and show that it is strictl…
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…
Co-Simulation of Human-Robot Collaboration: from Temporal Logic to 3D Simulation
Mehrnoosh Askarpour, Matteo Rossi, Omer Tiryakiler
Human-Robot Collaboration (HRC) is rapidly replacing the traditional application of robotics in the manufacturing industry. Robots and human operators no longer have to perform the…
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…
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…
Non-null Infinitesimal Micro-steps: a Metric Temporal Logic Approach
Luca Ferrucci, Dino Mandrioli, Angelo Morzenti +1
Many systems include components interacting with each other that evolve with possibly very different speeds. To deal with this situation many formal models adopt the abstraction of…
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…
A Theory of Sampling for Continuous-time Metric Temporal Logic
Carlo A. Furia, Matteo Rossi
This paper revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiabili…
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…
Modeling Time in Computing: A Taxonomy and a Comparative Survey
Carlo A. Furia, Dino Mandrioli, Angelo Morzenti +1
The increasing relevance of areas such as real-time and embedded systems, pervasive computing, hybrid systems control, and biological and social systems modeling is bringing a grow…
Practical Automated Partial Verification of Multi-Paradigm Real-Time Models
Carlo A. Furia, Matteo Pradella, Matteo Rossi
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational…