Showing 1–29 of 29 results for author: Schmitz, S

Verifying Unboundedness via Amalgamation

Authors: Ashwani Anand, Sylvain Schmitz, Lia Schütze, Georg Zetzsche

Abstract: Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is noto… ▽ More Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS' scope entirely, such as pushdown systems (PDS). Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete. Moreover, this abstract setting enables simple and general algorithmic solutions to unboundedness problems, which have received much attention in recent years. We present algorithms for the (i) simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii) computing priority downward closures, (iii) deciding whether a language is bounded, meaning included in $w_1^*\cdots w_k^*$ for some words $w_1,\ldots,w_k$, and (iv) effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems. △ Less

Submitted 20 June, 2024; v1 submitted 16 May, 2024; originally announced May 2024.

Comments: Erratum: Updated test for negative SUP instances in Section 4.1

ACM Class: F.4.3

Measuring well quasi-ordered finitary powersets

Authors: Sergio Abriola, Simon Halfon, Aliaume Lopez, Sylvain Schmitz, Philippe Schnoebelen, Isa Vialard

Abstract: The complexity of a well-quasi-order (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the "finitary powerset" construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo… ▽ More The complexity of a well-quasi-order (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the "finitary powerset" construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo. The width, height and maximal order type of Pf(X) cannot be expressed as a function of the invariants of X, and we provide tight upper and lower bounds for the three invariants. The article also identifies an algebra of well-behaved wqos, that include finitary powersets as well as other more classical constructions, and for which the ordinal invariants can be computed compositionnally. This relies on a new ordinal invariant called the approximated maximal order type. △ Less

Submitted 22 December, 2023; originally announced December 2023.

Comments: 33 pages

MSC Class: 06 ACM Class: F.2.2; G.2

On the Length of Strongly Monotone Descending Chains over $\mathbb{N}^d$

Authors: Sylvain Schmitz, Lia Schütze

Abstract: A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in $d$-dimensional vector addition systems under unary encoding to $n^{2^{O(d)}}$, improving on Rackoff's $n^{2^{O(d\lg d)}}$ upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds. In this paper, we revisit Laz… ▽ More A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in $d$-dimensional vector addition systems under unary encoding to $n^{2^{O(d)}}$, improving on Rackoff's $n^{2^{O(d\lg d)}}$ upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazić and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput., 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over $\mathbb{N}^d$ that arise from the dual backward coverability algorithm of Lazić and Schmitz on $d$-dimensional unary vector addition systems also enjoy this tight $n^{2^{O(d)}}$ upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazić and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS, 2017) for the coverability problem in invertible affine nets. △ Less

Submitted 20 April, 2024; v1 submitted 4 October, 2023; originally announced October 2023.

ACM Class: F.3.1; F.2

Journal ref: Proceedings of ICALP 2024

Games on Graphs

Authors: Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, Mateusz Skomra

Abstract: The objective of this collaborative textbook is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph. The objective of this collaborative textbook is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph. △ Less

Submitted 17 May, 2023; originally announced May 2023.

Comments: 490 pages. Coordinator: Nathanaël Fijalkow

Defining Cases and Variants for Object-Centric Event Data

Authors: Jan Niklas Adams, Daniel Schuster, Seth Schmitz, Günther Schuh, Wil M. P. van der Aalst

Abstract: The execution of processes leaves traces of event data in information systems. These event data can be analyzed through process mining techniques. For traditional process mining techniques, one has to associate each event with exactly one object, e.g., the company's customer. Events related to one object form an event sequence called a case. A case describes an end-to-end run through a process. Th… ▽ More The execution of processes leaves traces of event data in information systems. These event data can be analyzed through process mining techniques. For traditional process mining techniques, one has to associate each event with exactly one object, e.g., the company's customer. Events related to one object form an event sequence called a case. A case describes an end-to-end run through a process. The cases contained in event data can be used to discover a process model, detect frequent bottlenecks, or learn predictive models. However, events encountered in real-life information systems, e.g., ERP systems, can often be associated with multiple objects. The traditional sequential case concept falls short of these object-centric event data as these data exhibit a graph structure. One might force object-centric event data into the traditional case concept by flattening it. However, flattening manipulates the data and removes information. Therefore, a concept analogous to the case concept of traditional event logs is necessary to enable the application of different process mining tasks on object-centric event data. In this paper, we introduce the case concept for object-centric process mining: process executions. These are graph-based generalizations of cases as considered in traditional process mining. Furthermore, we provide techniques to extract process executions. Based on these executions, we determine equivalent process behavior with respect to an attribute using graph isomorphism. Equivalent process executions with respect to the event's activity are object-centric variants, i.e., a generalization of variants in traditional process mining. We provide a visualization technique for object-centric variants. The contribution's scalability and efficiency are extensively evaluated. Furthermore, we provide a case study showing the most frequent object-centric variants of a real-life event log. △ Less

Submitted 5 August, 2022; originally announced August 2022.

SMART: a Technology Readiness Methodology in the Frame of the NIS Directive

Authors: Archana Kumari, Stefan Schiffner, Sandra Schmitz

Abstract: An ever shorter technology lifecycle engendered the need for assessing new technologies w.r.t. their market readiness. Knowing the Technology readiness level (TRL) of a given target technology proved to be useful to mitigate risks such as cost overrun, product roll out delays, or early launch failures. Originally developed for space programmes by NASA, TRL became a de facto standard among technolo… ▽ More An ever shorter technology lifecycle engendered the need for assessing new technologies w.r.t. their market readiness. Knowing the Technology readiness level (TRL) of a given target technology proved to be useful to mitigate risks such as cost overrun, product roll out delays, or early launch failures. Originally developed for space programmes by NASA, TRL became a de facto standard among technology and manufacturing companies and even among research funding agencies. However, while TRL assessments provide a systematic evaluation process resulting in meaningful metric, they are one dimensional: they only answer the question if a technology can go into production. Hence they leave an inherent gap, i.e., if a technology fulfils requirements with a certain quality. This gap becomes intolerable when this metric is applied software such as technological cybersecurity measures. With legislation such as the General Data Protection Regulation4 (GDPR) and the Network and Information Systems Directive5 (NIS-D) making reference to state of the art when requiring appropriate protection measures, software designers are faced with the question how to measure if a technology is suitable to use. We argue that there is a potential mismatch of legal aim and technological reality which not only leads to a risk of non-compliance, but also might lead to weaker protected systems than possible. In that regard, we aim to address the gaps identified with existing Technology Readiness Assessment (TRA)s and aim to overcome these by develo** standardised method which is suitable for assessing software w.r.t. its market readiness and quality (in sum maturity). △ Less

Submitted 3 January, 2022; originally announced January 2022.

Comments: 1 figure

QoS Prediction for 5G Connected and Automated Driving

Authors: Apostolos Kousaridas, Ramya Panthangi Manjunath, Jose Mauricio Perdomo, Chan Zhou, Ernst Zielinski, Steffen Schmitz, Andreas Pfadler

Abstract: 5G communication system can support the demanding quality-of-service (QoS) requirements of many advanced vehicle-to-everything (V2X) use cases. However, the safe and efficient driving, especially of automated vehicles, may be affected by sudden changes of the provided QoS. For that reason, the prediction of the QoS changes and the early notification of these predicted changes to the vehicles have… ▽ More 5G communication system can support the demanding quality-of-service (QoS) requirements of many advanced vehicle-to-everything (V2X) use cases. However, the safe and efficient driving, especially of automated vehicles, may be affected by sudden changes of the provided QoS. For that reason, the prediction of the QoS changes and the early notification of these predicted changes to the vehicles have been recently enabled by 5G communication systems. This solution enables the vehicles to avoid or mitigate the effect of sudden QoS changes at the application level. This article describes how QoS prediction could be generated by a 5G communication system and delivered to a V2X application. The tele-operated driving use case is used as an example to analyze the feasibility of a QoS prediction scheme. Useful recommendations for the development of a QoS prediction solution are provided, while open research topics are identified. △ Less

Submitted 11 July, 2021; originally announced July 2021.

Comments: 7 pages, 5 figures, accepted for publication in the IEEE Communications Magazine

On the Computation of the Zariski Closure of Finitely Generated Groups of Matrices

Authors: Klara Nosan, Amaury Pouly, Sylvain Schmitz, Mahsa Shirmohammadi, James Worrell

Abstract: We investigate the complexity of computing the Zariski closure of a finitely generated group of matrices. The Zariski closure was previously shown to be computable by Derksen, Jeandel, and Koiran, but the termination argument for their algorithm appears not to yield any complexity bound. In this paper we follow a different approach and obtain a bound on the degree of the polynomials that define th… ▽ More We investigate the complexity of computing the Zariski closure of a finitely generated group of matrices. The Zariski closure was previously shown to be computable by Derksen, Jeandel, and Koiran, but the termination argument for their algorithm appears not to yield any complexity bound. In this paper we follow a different approach and obtain a bound on the degree of the polynomials that define the closure. Our bound shows that the closure can be computed in elementary time. We also obtain upper bounds on the length of chains of linear algebraic groups, where all the groups are generated over a fixed number field. △ Less

Submitted 7 June, 2022; v1 submitted 3 June, 2021; originally announced June 2021.

Journal ref: Proceedings of the 2022 International Symposium on Symbolic and Algebraic Computation (ISSAC'22), pp. 129--138

Robust Minimum Cost Flow Problem Under Consistent Flow Constraints

Authors: Christina Büsing, Arie M. C. A. Koster, Sabrina Schmitz

Abstract: The robust minimum cost flow problem under consistent flow constraints (RobMCF$\equiv$) is a new extension of the minimum cost flow (MCF) problem. In the RobMCF$\equiv$ problem, we consider demand and supply that are subject to uncertainty. For all demand realizations, however, we require that the flow value on an arc needs to be equal if it is included in the predetermined arc set given. The obje… ▽ More The robust minimum cost flow problem under consistent flow constraints (RobMCF$\equiv$) is a new extension of the minimum cost flow (MCF) problem. In the RobMCF$\equiv$ problem, we consider demand and supply that are subject to uncertainty. For all demand realizations, however, we require that the flow value on an arc needs to be equal if it is included in the predetermined arc set given. The objective is to find feasible flows that satisfy the equal flow requirements while minimizing the maximum occurring cost among all demand realizations. In the case of a discrete set of scenarios, we derive structural results which point out the differences with the polynomial time solvable MCF problem on networks with integral capacities. In particular, the Integral Flow Theorem of Dantzig and Fulkerson does not hold. For this reason, we require integral flows in the entire paper. We show that the RobMCF$\equiv$ problem is strongly $\mathcal{NP}$-hard on acyclic digraphs by a reduction from the $(3,B2)$-Sat problem. Further, we demonstrate that the RobMCF$\equiv$ problem is weakly $\mathcal{NP}$-hard on series-parallel digraphs by providing a reduction from Partition and a pseudo-polynomial algorithm based on dynamic programming. Finally, we propose a special case on series-parallel digraphs for which we can solve the RobMCF$\equiv$ problem in polynomial time. △ Less

Submitted 5 August, 2020; originally announced August 2020.

GivEn -- Shape Optimization for Gas Turbines in Volatile Energy Networks

Authors: Jan Backhaus, Matthias Bolten, Onur Tanil Doganay, Matthias Ehrhardt, Benedikt Engel, Christian Frey, Hanno Gottschalk, Michael Günther, Camilla Hahn, Jens Jäschke, Peter Jaksch, Kathrin Klamroth, Alexander Liefke, Daniel Luft, Lucas Mäde, Vincent Marciniak, Marco Reese, Johanna Schultes, Volker Schulz, Sebastian Schmitz, Johannes Steiner, Michael Stiglmayr

Abstract: This paper describes the project GivEn that develops a novel multicriteria optimization process for gas turbine blades and vanes using modern "adjoint" shape optimization algorithms. Given the many start and shut-down processes of gas power plants in volatile energy grids, besides optimizing gas turbine geometries for efficiency, the durability understood as minimization of the probability of fail… ▽ More This paper describes the project GivEn that develops a novel multicriteria optimization process for gas turbine blades and vanes using modern "adjoint" shape optimization algorithms. Given the many start and shut-down processes of gas power plants in volatile energy grids, besides optimizing gas turbine geometries for efficiency, the durability understood as minimization of the probability of failure is a design objective of increasing importance. We also describe the underlying coupling structure of the multiphysical simulations and use modern, gradient based multicriteria optimization procedures to enhance the exploration of Pareto-optimal solutions. △ Less

Submitted 20 February, 2020; originally announced February 2020.

ACM Class: G.1.6; G.3; G.1.8

Automatic Co-Registration of Aerial Imagery and Untextured Model Data Utilizing Average Shading Gradients

Authors: Sylvia Schmitz, Martin Weinmann, Boitumelo Ruf

Abstract: The comparison of current image data with existing 3D model data of a scene provides an efficient method to keep models up to date. In order to transfer information between 2D and 3D data, a preliminary co-registration is necessary. In this paper, we present a concept to automatically co-register aerial imagery and untextured 3D model data. To refine a given initial camera pose, our algorithm comp… ▽ More The comparison of current image data with existing 3D model data of a scene provides an efficient method to keep models up to date. In order to transfer information between 2D and 3D data, a preliminary co-registration is necessary. In this paper, we present a concept to automatically co-register aerial imagery and untextured 3D model data. To refine a given initial camera pose, our algorithm computes dense correspondence fields using SIFT flow between gradient representations of the model and camera image, from which 2D-3D correspondences are obtained. These correspondences are then used in an iterative optimization scheme to refine the initial camera pose by minimizing the reprojection error. Since it is assumed that the model does not contain texture information, our algorithm is built up on an existing method based on Average Shading Gradients (ASG) to generate gradient images based on raw geometry information only. We apply our algorithm for the co-registering of aerial photographs to an untextured, noisy mesh model. We have investigated different magnitudes of input error and show that the proposed approach can reduce the final reprojection error to a minimum of 1.27 plus-minus 0.54 pixels, which is less than 10 % of its initial value. Furthermore, our evaluation shows that our approach outperforms the accuracy of a standard Iterative Closest Point (ICP) implementation. △ Less

Submitted 21 September, 2019; v1 submitted 26 June, 2019; originally announced June 2019.

Journal ref: Int. Arch. Photogramm. Remote Sens. Spatial Inf. Sci., XLII-2/W13, 581-588, 2019

Coverability is Undecidable in One-dimensional Pushdown Vector Addition Systems with Resets

Authors: Sylvain Schmitz, Georg Zetzsche

Abstract: We consider the model of pushdown vector addition systems with resets. These consist of vector addition systems that have access to a pushdown stack and have instructions to reset counters. For this model, we study the coverability problem. In the absence of resets, this problem is known to be decidable for one-dimensional pushdown vector addition systems, but decidability is open for general push… ▽ More We consider the model of pushdown vector addition systems with resets. These consist of vector addition systems that have access to a pushdown stack and have instructions to reset counters. For this model, we study the coverability problem. In the absence of resets, this problem is known to be decidable for one-dimensional pushdown vector addition systems, but decidability is open for general pushdown vector addition systems. Moreover, coverability is known to be decidable for reset vector addition systems without a pushdown stack. We show in this note that the problem is undecidable for one-dimensional pushdown vector addition systems with resets. △ Less

Submitted 17 June, 2019; originally announced June 2019.

Comments: 8 pages

Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension

Authors: Jérôme Leroux, Sylvain Schmitz

Abstract: The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomp… ▽ More The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomposition algorithm of Mayr, Kosaraju, and Lambert and to its termination proof, which yield an ACKERMANN upper bound in the general case, and primitive-recursive upper bounds in fixed dimension. While this does not match the currently best known TOWER lower bound for reachability, it is optimal for related problems. △ Less

Submitted 20 March, 2019; originally announced March 2019.

Journal ref: 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)

Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete

Authors: Petr Jančar, Sylvain Schmitz

Abstract: Checking whether two pushdown automata with restricted silent actions are weakly bisimilar was shown decidable by Sénizergues (1998, 2005). We provide the first known complexity upper bound for this famous problem, in the equivalent setting of first-order grammars. This ACKERMANN upper bound is optimal, and we also show that strong bisimilarity is primitive-recursive when the number of states of t… ▽ More Checking whether two pushdown automata with restricted silent actions are weakly bisimilar was shown decidable by Sénizergues (1998, 2005). We provide the first known complexity upper bound for this famous problem, in the equivalent setting of first-order grammars. This ACKERMANN upper bound is optimal, and we also show that strong bisimilarity is primitive-recursive when the number of states of the automata is fixed. △ Less

Submitted 21 January, 2019; originally announced January 2019.

Journal ref: 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)

Perfect Half Space Games

Authors: Thomas Colcombet, Marcin Jurdziński, Ranko Lazić, Sylvain Schmitz

Abstract: 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… ▽ More 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. △ Less

Submitted 20 April, 2017; v1 submitted 19 April, 2017; originally announced April 2017.

Comments: Accepted at LICS 2017

Journal ref: 32nd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2017)

Demystifying Reachability in Vector Addition Systems

Authors: Jérôme Leroux, Sylvain Schmitz

Abstract: More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition tech… ▽ More More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural embedding relation between runs as well quasi ordering. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain a cubic Ackermann upper bound for the decomposition algorithms, thus providing the first known upper bounds for general VAS reachability. △ Less

Submitted 13 May, 2015; v1 submitted 2 March, 2015; originally announced March 2015.

Comments: To appear in the Proceedings of LICS 2015

Journal ref: Proceedings of LICS 2015, pp. 56--67, IEEE Press

Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time

Authors: Marcin Jurdziński, Ranko Lazić, Sylvain Schmitz

Abstract: We generalise the hyperplane separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polyn… ▽ More We generalise the hyperplane separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polynomial time for fixed dimensions 3 or larger (Chaloupka, 2013). It also improves the complexity of solving multi-dimensional energy games with given initial credit from non-elementary (Brázdil, Jančar, and Kučera, 2010) to 2EXPTIME, thus establishing their 2EXPTIME-completeness. △ Less

Submitted 6 September, 2021; v1 submitted 24 February, 2015; originally announced February 2015.

Comments: Corrected proofs in former Section 3.3 Energy Games with Given Initial Credit

Journal ref: Proceedings of ICALP 2015, Lecture Notes in Computer Science vol. 9135, pp. 260--272, Springer

Complexity Bounds for Ordinal-Based Termination

Authors: Sylvain Schmitz

Abstract: `What more than its truth do we know if we have a proof of a theorem in a given formal system?' We examine Kreisel's question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program running times. Our main tool for this are length function theorems, which provide complexity bounds on the use of well quasi orders. We illustrate how to prove su… ▽ More `What more than its truth do we know if we have a proof of a theorem in a given formal system?' We examine Kreisel's question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program running times. Our main tool for this are length function theorems, which provide complexity bounds on the use of well quasi orders. We illustrate how to prove such theorems in the simple yet until now untreated case of ordinals. We show how to apply this new theorem to derive complexity bounds on programs when they are proven to terminate thanks to a ranking function into some ordinal. △ Less

Submitted 22 July, 2014; originally announced July 2014.

Comments: Invited talk at the 8th International Workshop on Reachability Problems (RP 2014, 22-24 September 2014, Oxford)

ACM Class: F.2.0; F.3.1

Journal ref: Proceedings of RP 2014, Lecture Notes in Computer Science 8762, pp. 1--19, 2014

The Power of Well-Structured Systems

Authors: Sylvain Schmitz, Philippe Schnoebelen

Abstract: Well-structured systems, aka WSTSs, are computational models where the set of possible configurations is equipped with a well-quasi-ordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields. This paper recalls the basic theory underlying well-structured systems… ▽ More Well-structured systems, aka WSTSs, are computational models where the set of possible configurations is equipped with a well-quasi-ordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields. This paper recalls the basic theory underlying well-structured systems and shows how two classic decision algorithms can be formulated as an exhaustive search for some "bad" sequences. This lets us describe new powerful techniques for the complexity analysis of WSTS algorithms. Recently, these techniques have been successful in precisely characterising the power, in a complexity-theoretical sense, of several important WSTS models like unreliable channel systems, monotonic counter machines, or networks of timed systems. △ Less

Submitted 12 February, 2014; originally announced February 2014.

Comments: Invited talk

Journal ref: Proceedings of Concur 2013, Lecture Notes in Computer Science vol. 8052, pp. 5--24

Implicational Relevance Logic is 2-EXPTIME-Complete

Authors: Sylvain Schmitz

Abstract: We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems. We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems. △ Less

Submitted 16 May, 2022; v1 submitted 4 February, 2014; originally announced February 2014.

Comments: Fixed Fig. 6 as pointed out by Hiromi Tanaka

ACM Class: F.2.2; F.4.1

Journal ref: Proceedings of RTA-TLCA 2014, Lecture Notes in Computer Science 8560, pp. 395--409, Springer, 2014; journal version in Journal of Symbolic Logic 81(2), pages 641--661, 2016

Non-Elementary Complexities for Branching VASS, MELL, and Extensions

Authors: Ranko Lazić, Sylvain Schmitz

Abstract: We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case -- and hence non-elementary. We match this lower bound for the full p… ▽ More We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case -- and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete. △ Less

Submitted 16 May, 2022; v1 submitted 27 January, 2014; originally announced January 2014.

Comments: Fixed Fig. 3 thanks to Hiromi Tanaka

ACM Class: F.2.2; F.4.1

Journal ref: ACM Transactions on Computational Logic, vol. 16, issue 3, article 20, 2015

Complexity Hierarchies Beyond Elementary

Authors: Sylvain Schmitz

Abstract: We introduce a hierarchy of fast-growing complexity classes and show its suitability for completeness statements of many non elementary problems. This hierarchy allows the classification of many decision problems with a non-elementary complexity, which occur naturally in logic, combinatorics, formal languages, verification, etc., with complexities ranging from simple towers of exponentials to Acke… ▽ More We introduce a hierarchy of fast-growing complexity classes and show its suitability for completeness statements of many non elementary problems. This hierarchy allows the classification of many decision problems with a non-elementary complexity, which occur naturally in logic, combinatorics, formal languages, verification, etc., with complexities ranging from simple towers of exponentials to Ackermannian and beyond. △ Less

Submitted 4 February, 2016; v1 submitted 19 December, 2013; originally announced December 2013.

Comments: Version 3 is the published version in TOCT 8(1:3), 2016. I will keep updating the catalogue of problems from Section 6 in future revisions

ACM Class: F.1.3

Journal ref: ACM Transactions on Computation Theory vol. 8, number 1, article 3, 2016

The Power of Priority Channel Systems

Authors: Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen

Abstract: We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been use… ▽ More We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing functions and prove that the aforementioned verification problems are $\mathbf{F}_{\varepsilon_{0}}$-complete. △ Less

Submitted 2 December, 2014; v1 submitted 23 January, 2013; originally announced January 2013.

Comments: Extended version of an article presented at CONCUR 2013, LNCS 8052, pp. 319--333, Springer, doi:10.1007/978-3-642-40184-8_23

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 4 (December 3, 2014) lmcs:1049

The Parametric Ordinal-Recursive Complexity of Post Embedding Problems

Authors: Prateek Karandikar, Sylvain Schmitz

Abstract: Post Embedding Problems are a family of decision problems based on the interaction of a rational relation with the subword embedding ordering, and are used in the literature to prove non multiply-recursive complexity lower bounds. We refine the construction of Chambart and Schnoebelen (LICS 2008) and prove parametric lower bounds depending on the size of the alphabet. Post Embedding Problems are a family of decision problems based on the interaction of a rational relation with the subword embedding ordering, and are used in the literature to prove non multiply-recursive complexity lower bounds. We refine the construction of Chambart and Schnoebelen (LICS 2008) and prove parametric lower bounds depending on the size of the alphabet. △ Less

Submitted 22 November, 2012; originally announced November 2012.

Comments: 16 + vii pages

ACM Class: F.2

Journal ref: FoSSaCS 2013, LNCS 7794, pp. 273--288, Springer

Model Checking Parse Trees

Authors: Anudhyan Boral, Sylvain Schmitz

Abstract: Parse trees are fundamental syntactic structures in both computational linguistics and compilers construction. We argue in this paper that, in both fields, there are good incentives for model-checking sets of parse trees for some word according to a context-free grammar. We put forward the adequacy of propositional dynamic logic (PDL) on trees in these applications, and study as a sanity check the… ▽ More Parse trees are fundamental syntactic structures in both computational linguistics and compilers construction. We argue in this paper that, in both fields, there are good incentives for model-checking sets of parse trees for some word according to a context-free grammar. We put forward the adequacy of propositional dynamic logic (PDL) on trees in these applications, and study as a sanity check the complexity of the corresponding model-checking problem: although complete for exponential time in the general case, we find natural restrictions on grammars for our applications and establish complexities ranging from nondeterministic polynomial time to polynomial space in the relevant cases. △ Less

Submitted 25 March, 2013; v1 submitted 22 November, 2012; originally announced November 2012.

Comments: 21 + x pages

ACM Class: F.4; D.3.1; I.2.7

Journal ref: LICS 2013, pp. 153-162, IEEE Computer Society Press

Multiply-Recursive Upper Bounds with Higman's Lemma

Authors: Sylvain Schmitz, Philippe Schnoebelen

Abstract: We develop a new analysis for the length of controlled bad sequences in well-quasi-orderings based on Higman's Lemma. This leads to tight multiply-recursive upper bounds that readily apply to several verification algorithms for well-structured systems. We develop a new analysis for the length of controlled bad sequences in well-quasi-orderings based on Higman's Lemma. This leads to tight multiply-recursive upper bounds that readily apply to several verification algorithms for well-structured systems. △ Less

Submitted 19 July, 2011; v1 submitted 22 March, 2011; originally announced March 2011.

ACM Class: D.2.4; F.1.3; F.2; F.4.2

Journal ref: In Aceto, L., Henzinger, M., and Sgall, J., editors, ICALP 2011, 38th International Colloquium on Automata, Languages and Programming, volume 6756 of Lecture Notes in Computer Science, pages 441--452. Springer Heidelberg

Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

Authors: Diego Figueira, Santiago Figueira, Sylvain Schmitz, Philippe Schnoebelen

Abstract: Dickson's Lemma is a simple yet powerful tool widely used in termination proofs, especially when dealing with counters or related data structures. However, most computer scientists do not know how to derive complexity upper bounds from such termination proofs, and the existing literature is not very helpful in these matters. We propose a new analysis of the length of bad sequences over (N^k,\leq… ▽ More Dickson's Lemma is a simple yet powerful tool widely used in termination proofs, especially when dealing with counters or related data structures. However, most computer scientists do not know how to derive complexity upper bounds from such termination proofs, and the existing literature is not very helpful in these matters. We propose a new analysis of the length of bad sequences over (N^k,\leq) and explain how one may derive complexity upper bounds from termination proofs. Our upper bounds improve earlier results and are essentially tight. △ Less

Submitted 19 July, 2011; v1 submitted 18 July, 2010; originally announced July 2010.

ACM Class: D.2.4; F.1.3; F.2; F.4.1; G.2.1

Journal ref: In LICS 2011, 26th Annual IEEE Symposium on Logic in Computer Science, pages 269--278. IEEE Press

Forward Analysis and Model Checking for Trace Bounded WSTS

Authors: Pierre Chambart, Alain Finkel, Sylvain Schmitz

Abstract: We investigate a subclass of well-structured transition systems (WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans. AMS 1964)---complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (Logic. Meth. Comput. Sci. 2012). Indeed, we prove that, unlike other conditions considered previously for th… ▽ More We investigate a subclass of well-structured transition systems (WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans. AMS 1964)---complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (Logic. Meth. Comput. Sci. 2012). Indeed, we prove that, unlike other conditions considered previously for the termination of forward analysis, boundedness is decidable. 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. △ Less

Submitted 4 March, 2016; v1 submitted 16 April, 2010; originally announced April 2010.

Report number: RR-LSV-10-08 ACM Class: D.2.4; F.4.1; F.4.3

Journal ref: 32nd International Conference on Application and Theory of Petri Nets, volume 6709 of Lecture Notes in Computer Science, pages 49--68. Springer Heidelberg

Feature Unification in TAG Derivation Trees

Authors: Sylvain Schmitz, Joseph Le Roux

Abstract: The derivation trees of a tree adjoining grammar provide a first insight into the sentence semantics, and are thus prime targets for generation systems. We define a formalism, feature-based regular tree grammars, and a translation from feature based tree adjoining grammars into this new formalism. The translation preserves the derivation structures of the original grammar, and accounts for featu… ▽ More The derivation trees of a tree adjoining grammar provide a first insight into the sentence semantics, and are thus prime targets for generation systems. We define a formalism, feature-based regular tree grammars, and a translation from feature based tree adjoining grammars into this new formalism. The translation preserves the derivation structures of the original grammar, and accounts for feature unification. △ Less

Submitted 29 April, 2008; originally announced April 2008.

Comments: 12 pages, 4 figures In TAG+9, Ninth International Workshop on Tree Adjoining Grammars and Related Formalisms, 2008

ACM Class: F.4.2; I.2.7

Journal ref: In TAG+9, Ninth International Workshop on Tree Adjoining Grammars and Related Formalisms, 2008