Author name cluster

Sylvain Schmitz

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

CSL Conference 2021 Conference Paper

Branching in Well-Structured Transition Systems (Invited Talk)

Sylvain Schmitz

The framework of well-structured transition systems has been highly successful in providing generic algorithms to show the decidability of verification problems for infinite-state systems. In some of these applications, the executions in the system at hand are actually trees, and need to be "lifted" to executions over sets of configurations in order to fit in the framework. The downside of this approach is that we might lose precision when analysing the computational complexity of the algorithms, compared to reasoning over branching executions.

Details

I&C Journal 2021 Journal Article

The ideal view on Rackoff's coverability technique

Ranko Lazić
Sylvain Schmitz

Well-structured transition systems form a large class of infinite-state systems, for which safety verification is decidable thanks to a generic backward coverability algorithm. However, for several classes of systems, the generic upper bounds one can extract from the algorithm are far from optimal. In particular, in the case of vector addition systems (VAS) and several of their extensions, the known tight upper bounds were rather derived thanks to ad-hoc arguments based on Rackoff's small witness property. We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. This reasoning offers a uniform setting for all well-structured transition systems, including branching ones, and we further apply it to several VAS extensions, deriving optimal upper bounds.

Details DOI

Highlights Conference 2017 Conference Abstract

Perfect Half Space Games

Thomas Colcombet
Marcin Jurdziński
Ranko Lazić
Sylvain Schmitz

We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwiński, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi- dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2-EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary. Abstract available in PDF; paper presented at LICS 2017 and available from arXiv.

PDF Details

CSL Conference 2016 Conference Paper

A Sequent Calculus for a Modal Logic on Finite Data Trees

David Baelde
Simon Lunel
Sylvain Schmitz

We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i. e. , over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.

Details

TCS Journal 2016 Journal Article

Forward analysis and model checking for trace bounded WSTS

Pierre Chambart
Alain Finkel
Sylvain Schmitz

We investigate a subclass of well-structured transition systems (WSTS), the trace bounded—in the sense of Ginsburg and Spanier (1964), [1]—complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (2012), [2]. Indeed, we prove that, unlike other conditions considered previously for the termination of forward analysis, trace boundedness is decidable. Trace boundedness turns out to be a valuable restriction for WSTS verification, as we show that it further allows to decide all ω-regular properties on the set of infinite traces of the system.

Details DOI

Highlights Conference 2013 Conference Abstract

Complexity hierarchies beyond elementary

Sylvain Schmitz

Decision problems with a non-elementary complexity occur naturally in logic, combinatorics, formal language, verification, etc. , with complexities ranging from simple towers of exponentials to Ackermannian and beyond. Somewhat surprisingly, we lack the definitions of classes and reductions that would allow to state completeness results at such high complexities. We introduce a hierarchy of fast-growing complexity classes and discuss its suitability for completeness statements of non-elementary problems. 16: 48 17: 12 Coffee Break

Details

MFCS Conference 2011 Conference Paper

Model Checking Coverability Graphs of Vector Addition Systems

Michel Blockelet
Sylvain Schmitz

Abstract A large number of properties of a vector addition system—for instance coverability, boundedness, or regularity—can be decided using its coverability graph, by looking for some characteristic pattern. We propose to unify the known exponential-space upper bounds on the complexity of such problems on vector addition systems, by seeing them as instances of the model-checking problem for a suitable extension of computation tree logic, which allows to check for the existence of these patterns. This provides new insights into what constitutes a “coverability-like” property.

Details

TCS Journal 2010 Journal Article

Parametric random generation of deterministic tree automata

Pierre-Cyrille Héam
Cyril Nicaud
Sylvain Schmitz

Uniform random generators deliver a simple empirical means to estimate the average complexity of an algorithm. We present a general rejection algorithm that generates sequential letter-to-letter transducers up to isomorphism. We also propose an original parametric random generation algorithm to produce sequential letter-to-letter transducers with a fixed number of transitions. We tailor this general scheme to randomly generate deterministic tree walking automata and deterministic top–down tree automata. We apply our implementation of the generator to the estimation of the average complexity of a deterministic tree walking automata to nondeterministic top–down tree automata construction we also implemented.

Details DOI