arXiv subjects

Jean-Marc Talbot

Publications and source records attributed to Jean-Marc Talbot.

5 recordsLinked to original sources

arXiv2025

Reasoning about Quality in Hyperproperties

Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.

cs.LO↗

arXiv2021

Weighted Automata and Expressions over Pre-Rational Monoids

The Kleene theorem establishes a fundamental link between automata and expressions over the free monoid. Numerous generalisations of this result exist in the literature. Lifting this result to a weighted setting has been widely studied. Moreover, different monoids can be considered: for instance, two-way automata, and even tree-walking automata, can be described by expressions using the free inverse monoid. In the present work, we aim at combining both research directions and consider weighted extensions of automata and expressions over a class of monoids that we call pre-rational, generalising both the free inverse monoid and graded monoids. The presence of idempotent elements in these pre-rational monoids leads in the weighted setting to consider infinite sums. To handle such sums, we will have to restrict ourselves to rationally additive semirings. Our main result is thus a generalisation of the Kleene theorem for pre-rational monoids and rationally additive semirings. As a corollary, we obtain a class of expressions equivalent to weighted two-way automata, as well as one for tree-walking automata.

cs.FL↗

arXiv2016

Two-Way Visibly Pushdown Automata and Transducers

Automata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but important results have been obtained recently for word-to-word transformations, showing that the three following models are equivalent: deterministic two-way transducers, monadic second-order (MSO) transducers, and deterministic one-way automata equipped with a finite number of registers. Nested words are words with a nesting structure, allowing to model unranked trees as their depth-first-search linearisations. In this paper, we consider transformations from nested words to words, allowing in particular to produce unranked trees if output words have a nesting structure. The model of visibly pushdown transducers allows to describe such transformations, and we propose a simple deterministic extension of this model with two-way moves that has the following properties: i) it is a simple computational model, that naturally has a good evaluation complexity; ii) it is expressive: it subsumes nested word-to-word MSO transducers, and the exact expressiveness of MSO transducers is recovered using a simple syntactic restriction; iii) it has good algorithmic/closure properties: the model is closed under composition with a unambiguous one-way letter-to-letter transducer which gives closure under regular look-around, and has a decidable equivalence problem.

cs.FL↗

arXiv2013

Expressiveness of Visibly Pushdown Transducers

Visibly pushdown transducers (VPTs) are visibly pushdown automata extended with outputs. They have been introduced to model transformations of nested words, i.e. words with a call/return structure. As trees and more generally hedges can be linearized into (well) nested words, VPTs are a natural formalism to express tree transformations evaluated in streaming. This paper aims at characterizing precisely the expressive power of VPTs with respect to other tree transducer models.

cs.FL↗

arXiv2010

On Functionality of Visibly Pushdown Transducers

Visibly pushdown transducers form a subclass of pushdown transducers that (strictly) extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. In this paper, we prove that functionality is decidable in PSpace for visibly pushdown transducers. The proof is done via a pumping argument: if a word with two outputs has a sufficiently large nesting depth, there exists a nested word with two outputs whose nesting depth is strictly smaller. The proof uses technics of word combinatorics. As a consequence of decidability of functionality, we also show that equivalence of functional visibly pushdown transducers is Exptime-Complete.

cs.FL↗