17 citations · 45 across the 18 of their papers we have counts for
20 papers
Learning Shuffle Ideals with Membership Queries and Contrastive Examples
S. Mahmoud Mousawi, Pierluigi San Pietro, Sandra Zilles
This paper studies learning of shuffle ideals with membership queries as well as with contrastive queries---a form of membership query that reveals not only whether a selected word…
Guillotine and Tiling Cofiniteness in Unary Picture Languages
Pierluigi San Pietro, Stefano Crespi Reghizzi, Antonio Restivo
Motivated by the study of closure operations on picture languages, we ask when a set of unary tiles can generate all sufficiently large pictures either via repeated horizontal and…
TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractio…
Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult…
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…
Two-dimensional Dyck words
Stefano Crespi Reghizzi, Antonio Restivo, Pierluigi San Pietro
We propose different ways of lifting the notion of Dyck language from words to 2-dimensional (2D) pictures, by means of new definitions of increasing comprehensiveness. Two of the…
Reducing the local alphabet size in tiling systems by means of 2D comma-free codes
Stefano {Crespi Reghizzi}, Antonio Restivo, Pierluigi {San Pietro}
A recognizable picture language is defined as the projection of a local picture language defined by a set of two-by-two tiles, i.e. by a strictly-locally-testable (SLT) language of…
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…
Deque languages, automata and planar graphs
Stefano Crespi Reghizzi, Pierluigi San Pietro
The memory of a deque (double ended queue) automaton is more general than a queue or two stacks; to avoid overgeneralization, we consider quasi-real-time operation. Normal forms of…
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…
Non-erasing Chomsky-Sch{ü}tzenberger theorem with grammar-independent alphabet
Stefano Crespi Reghizzi, Pierluigi San Pietro
The famous theorem by Chomsky and Schützenberger (CST) says that every context-free language over an alphabet is representable as , where is a Dyck languag…
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification
Patricia Bouyer, Andrea Orlandini, Pierluigi San Pietro
This volume contains the proceedings of the Eighth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2017). The symposium took place in Roma, Italy…
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…
Offline Trace Checking of Quantitative Properties of Service-Based Applications
Domenico Bianculli, Carlo Ghezzi, Srdan Krstic +1
Service-based applications are often developed as compositions of partner services. A service integrator needs precise methods to specify the quality attributes expected by each pa…
Commutative Languages and their Composition by Consensual Methods
Stefano Crespi Reghizzi, Pierluigi San Pietro
Commutative languages with the semilinear property (SLIP) can be naturally recognized by real-time NLOG-SPACE multi-counter machines. We show that unions and concatenations of such…
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…
From Regular to Strictly Locally Testable Languages
Stefano Crespi Reghizzi, Pierluigi San Pietro
A classical result (often credited to Y. Medvedev) states that every language recognized by a finite automaton is the homomorphic image of a local language, over a much larger so-c…
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…