56 citations · 114 across the 13 of their papers we have counts for
11 papers · 1 filter
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…
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…
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…