arXiv subjects

Pierluigi San Pietro

Publications and source records attributed to Pierluigi San Pietro.

At least 19 recordsLinked to original sources

arXiv2026

Learning Shuffle Ideals with Membership Queries and Contrastive Examples

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 $w$ is in the target language or not, but also provides a most similar word $w'$ that belongs to the target language if %and only if $w$ does not. For both settings, it is shown that even some very simple classes of shuffle ideals cannot be learned efficiently. By contrast, we obtain positive learnability results for classes of shuffle ideals that meet certain structural conditions. In the case of membership queries, these structural conditions are related to the previously studied notion of universal words, and raise new questions in word combinatorics. In the case of contrastive queries, the structural conditions relate to partitioning sets of words that are listed in shortlex order.

cs.FL↗

arXiv2026

Guillotine and Tiling Cofiniteness in Unary Picture Languages

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 vertical concatenations or via tiling operations. In one dimension, the lengths of words in the concatenation closure of a unary language form an additive subsemigroup of positive natural numbers; hence, they are finitely generated. Cofiniteness is characterized by the gcd of these generators being one. Since ordinary cofiniteness in two dimensions is too restrictive and essentially reduces to degenerate one-dimensional conditions on strips, we introduce and study asymptotic cofiniteness: all sufficiently large rectangular pictures are generated. A direct extension of the one-dimensional criterion, requiring the gcd of the tile heights and of the tile widths to be one, is not sufficient, because local congruence obstructions may persist in two dimensions. We give an exact arithmetic characterization of asymptotic cofiniteness for arbitrary, possibly infinite, sets of unary rectangular tiles. The characterization is the same for the guillotine closure, obtained by horizontal and vertical concatenation, and for the full tiling closure. For finite tile sets, the proof combines semigroup arguments and an explicit least-common-multiple stacking construction for sufficiency, while necessity is obtained by a roots-of-unity argument applying also to nonsliceable tilings. The extension to infinite tile sets follows from the finite-basis theorem for Klarner systems.

cs.FL↗

arXiv2026

TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)

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 abstractions have been shown to outperform zones in specific subclasses of TA. To complement and support mature zone-based tools, we introduce TARZAN, a C++ region-based verification library for TA. The algorithms implemented in TARZAN use a novel region abstraction that tracks the order in which clocks become unbounded. This additional ordering induces a finer partitioning of the state space, enabling backward algorithms to avoid the combinatorial explosion associated with enumerating all ordered partitions of unbounded clocks, when computing immediate delay predecessor regions. We validate TARZAN by comparing forward reachability results against the state-of-the-art tools Uppaal and TChecker. The experiments confirm that zones excel when TA have large constants and strict guards. In contrast, TARZAN exhibits superior performance on closed TA and TA with punctual guards. Finally, we demonstrate the efficacy of our backward algorithms, establishing a foundation for region-based analysis in domains like Timed Games, where backward exploration is essential.

cs.FL↗

arXiv2025

On Decidability Timed Automata with 2 Parametric Clocks

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 same transition. The model has the same expressive power of TA, but it may require one more clock than an TA to recognize the same language. We consider the parametric version of nrtTA, where one parameter can appear in clock guards of transitions. The focus of this draft is to prove that the $ω$-language emptiness problem for 2-clock parametric nrtTA is decidable. This result can be compared with the parametric version of TA, where the emptiness problem for 2-clock TA with one parameter is not known to be decidable. Our result, however, extends the known decidability of the case of TA with one clock and one parameter from finite words to infinite words.

cs.FL↗

arXiv2025

Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation

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 to detect, yet a high level of confidence in the outcome is expected. Indeed, these tools are frequently novel and may not have been thoroughly tested. When standard benchmarks may be insufficient or unavailable, random test case generation offers a promising approach. To scale up, random testing requires comparing actual versus expected results, i.e., solving the oracle problem. To address this challenge, this work introduces a novel theoretical framework based on a modular variant of Timed Automata (TA), called Tiled Timed Automata (TTA), for testing model checkers operating with variations of TA, by building oracles based on Weighted Automata. The framework is initially applied to verify model checkers solving the emptiness problem for Parametric TA and it is validated, in this specific scenario, by our tool, TABEC, which randomly generates tests predicting their expected outcome through automated oracle generation. Furthermore, the general nature of TTA facilitates the framework adaptation to model checkers solving other decidable problems on TA, as detailed for the minimum-cost reachability problem of Priced TA.

cs.FL↗

arXiv2023

Two-dimensional Dyck words

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 proposals are based on alternative definitions of a Dyck language, which are equivalent over words but not on pictures. First, the property that any two pairs of matching parentheses are well-nested or disjoint is rephrased for rectangular boxes and leads to the well-nested Dyck, $DW_k$. This is a generalization of the known Chinese box language, but, unlike the Chinese boxes, $DW_k$ is not recognizable by a tiling system. Second, the Dyck cancellation rule is rephrased as a neutralization rule, mapping a quadruple of symbols representing the corners of a subpicture onto neutral symbols.The neutralizable Dyck language $DN_k$ is obtained by iterating neutralizations, starting from 2-by-2 subpictures, until the picture is wholly neutralized. Third, we define the Dyck crossword $DC_k$ as the row-column combination of Dyck word languages, which prescribes that each column and row is a Dyck word. The relation between matching parentheses is represented in $DC_k$ by an edge of a graph situated on the picture grid. Such edges form a circuit, of path length multiple of four, of alternating row and column matches. Length-four circuits have rectangular shape, while longer ones exhibit a large variety of forms. A proper subset of $DC_k$, called quaternate, is also introduced by excluding all circuits of length greater than 4. We prove that $DN_k$ properly includes $DW_k$, and that it coincides with the quaternate $DC_k$ such that the neutralizability relation between subpictures induces a partial order. The 2D languages well-nested, neutralizable, quaternate and Dyck crossword are ordered by strict inclusions. This work can be also seen as a first step towards the definition of context-free picture languages.

cs.FL↗

arXiv2021

Improved Bounded Model Checking of Timed Automata

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, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solved by tools such as Zot, which transforms CLTLoc properties into the input logics of Satisfiability Modulo Theories (SMT) solvers. We present a novel method that preserves TACK's encoding of MITL properties while encoding the TA network directly into the SMT solver language, making use of both the BitVector logic and the logic of real arithmetics. We also introduce several optimizations that allow us to significantly outperform the CLTLoc encoding in many practical scenarios.

cs.LO↗

arXiv2019

Verifying MITL formulae on Timed Automata considering a Continuous Time Semantics

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 formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the full Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts. This paper presents a novel technique to perform model checking of full Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula which is verified through an available decision procedure. The technique is flexible since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures.

cs.LO↗

arXiv2018

Deque languages, automata and planar graphs

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 such automata are given. Deque languages form an AFL but not a full one. We define the characteristic deque language, CDL, which combines Dyck and AntiDyck (or FIFO) languages, and homomorphically characterizes the deque languages. The notion of deque graph, from graph theory, well represents deque computation by means of a planar hamiltonian graph on a cylinder, with edges visualizing producer-consumer relations for deque symbols. We give equivalent definitions of CDL by labelled deque graphs, by cancellation rules, and by means of shuffle and intersection of simpler languages. The labeled deque graph of a sentence generalizes traditional syntax trees. The layout of deque computations on a cylinder is remindful of 3D models used in theoretical (bio)chemistry.

cs.FL↗

arXiv2018

Non-erasing Chomsky-Sch{ü}tzenberger theorem with grammar-independent alphabet

The famous theorem by Chomsky and Schützenberger (CST) says that every context-free language $L$ over an alphabet $Σ$ is representable as $h(D \cap R)$, where $D$ is a Dyck language over a set $Ω$ of brackets, $R$ is a local language and $h$ is an alphabetic homomorphism that erases unboundedly many symbols. Berstel found that the number of erasures can be linearly limited if the grammar is in Greibach normal form; Berstel and Boasson (and later, independently, Okhotin) proved a non-erasing variant of CST for grammars in Double Greibach Normal Form. In all these CST statements, however, the size of the Dyck alphabet $Ω$ depends on the grammar size for $L$. In the Stanley variant of the CST, $|Ω|$ only depends on $|Σ|$ and not on the grammar, but the homomorphism erases many more symbols than in the other versions of CST; also, the regular language $R$ is strictly locally testable but not local. We prove a new version of CST which combines both features of being non-erasing and of using a grammar-independent alphabet. In our construction, $|Ω|$ is polynomial in $|Σ|$, namely $O(|Σ|^{46})$, and the regular language $R$ is strictly locally testable. Using a recent generalization of Medvedev's homomorphic characterization of regular languages, we prove that the degree in the polynomial dependence of $|Ω|$ on $|Σ|$ may be reduced to just 2 in the case of linear grammars in Double Greibach Normal Form.

cs.FL↗

arXiv2017

Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification

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, from the 20th to the 22nd of September 2017. The GandALF symposium was established by a group of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their applications to the specification, design, and verification of complex systems. Its aim is to provide a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact. GandALF has a truly international spirit, as witnessed by the composition of the program and steering committee and by the country distribution of the submitted papers.

cs.GT↗

arXiv2015

Efficient Large-scale Trace Checking Using MapReduce

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 (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs.

cs.SE↗

arXiv2014

Offline Trace Checking of Quantitative Properties of Service-Based Applications

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 partner service, as well as effective techniques to verify these attributes. In previous work, we identified the most common specification patterns related to provisioning service-based applications and developed an expressive specification language (SOLOIST) that supports them. SOLOIST is an extension of metric temporal logic with aggregate temporal modalities that can be used to write quantitative temporal properties. In this paper we address the problem of performing offline checking of service execution traces against quantitative requirements specifications written in SOLOIST. We present a translation of SOLOIST into CLTLB(D), a variant of linear temporal logic, and reduce the trace checking of SOLOIST to bounded satisfiability checking of CLTLB(D), which is supported by ZOT, an SMT-based verification toolkit. We detail the results of applying the proposed offline trace checking procedure to different types of traces, and compare its performance with previous work.

cs.SE↗

arXiv2014

Commutative Languages and their Composition by Consensual Methods

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 languages can be similarly recognized, relying on -- and further developing, our recent results on the family of consensually regular (CREG) languages. A CREG language is defined by a regular language on the alphabet that includes the terminal alphabet and its marked copy. New conditions, for ensuring that the union or concatenation of CREG languages is closed, are presented and applied to the commutative SLIP languages. The paper contributes to the knowledge of the CREG family, and introduces novel techniques for language composition, based on arithmetic congruences that act as language signatures. Open problems are listed.

cs.FL↗

arXiv2014

Constraint LTL Satisfiability Checking without Automata

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 formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier-free equality and uninterpreted functions combined with D. Similarly to standard LTL, where bounded model-checking and SAT-solvers can be used as an alternative to automata-theoretic approaches to model-checking, our approach allows users to solve the satisfiability problem for CLTLB(D) formulae through SMT-solving techniques, rather than by checking the emptiness of the language of a suitable automaton A_ϕ. The technique is effective, and it has been implemented in our Zot formal verification tool.

cs.LO↗

arXiv2013

Deciding the Satisfiability of MITL Specifications

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 that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.

cs.LO↗

arXiv2011

From Regular to Strictly Locally Testable Languages

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-called local alphabet, namely the alphabet of the edges of the transition graph. Local languages are characterized by the value k=2 of the sliding window width in the McNaughton and Papert's infinite hierarchy of strictly locally testable languages (k-slt). We generalize Medvedev's result in a new direction, studying the relationship between the width and the alphabetic ratio telling how much larger the local alphabet is. We prove that every regular language is the image of a k-slt language on an alphabet of doubled size, where the width logarithmically depends on the automaton size, and we exhibit regular languages for which any smaller alphabetic ratio is insufficient. More generally, we express the trade-off between alphabetic ratio and width as a mathematical relation derived from a careful encoding of the states. At last we mention some directions for theoretical development and application.

cs.FL↗

arXiv2010

Bounded Reachability for Temporal Logic over Constraint Systems

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 systems, satisfiability and Model Checking problem of such logic can be undecidable. We introduce suitable restrictions and assumptions that are shown to make the satisfiability problem for the extended logic decidable. Moreover for a large class of constraint systems we propose an encoding that realize an effective decision procedure for the Bounded Reachability problem.

cs.LO↗