17 citations · 45 across the 18 of their papers we have counts for
6 papers · 1 filter
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…
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…
Dense-choice Counter Machines revisited
Florent Bouchy, Alain Finkel, Pierluigi San Pietro
This paper clarifies the picture about Dense-choice Counter Machines, which have been less studied than (discrete) Counter Machines. We revisit the definition of "Dense Counter Mac…
A Metric Encoding for Bounded Model Checking (extended version)
Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro
In Bounded Model Checking both the system model and the checked property are translated into a Boolean formula to be analyzed by a SAT-solver. We introduce a new encoding technique…