Showing 1–23 of 23 results for author: Schnoebelen, P

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 piecewise complexity of words and periodic words

Authors: M. Praveen, Philippe Schnoebelen, Isa Vialard, Julien Veron

Abstract: The piecewise complexity $h(u)$ of a word is the minimal length of subwords needed to exactly characterise $u$. Its piecewise minimality index $ρ(u)$ is the smallest length $k$ such that $u$ is minimal among its order-$k$ class $[u]_k$ in Simon's congruence. We study these two measures and provide efficient algorithms for computing $h(u)$ and $ρ(u)$. We also provide efficient algorithms for the… ▽ More The piecewise complexity $h(u)$ of a word is the minimal length of subwords needed to exactly characterise $u$. Its piecewise minimality index $ρ(u)$ is the smallest length $k$ such that $u$ is minimal among its order-$k$ class $[u]_k$ in Simon's congruence. We study these two measures and provide efficient algorithms for computing $h(u)$ and $ρ(u)$. We also provide efficient algorithms for the case where $u$ is a periodic word, of the form $u=v^n$ △ Less

Submitted 26 November, 2023; originally announced November 2023.

On arch factorization and subword universality for words and compressed words

Authors: Philippe Schnoebelen, Julien Veron

Abstract: Using arch-jum** functions and properties of the arch factorization of words, we propose a new algorithm for computing the subword circular universality index of words. We also introduce the subword universality signature for words, that leads to simple algorithms for the universality indexes of SLP-compressed words. Using arch-jum** functions and properties of the arch factorization of words, we propose a new algorithm for computing the subword circular universality index of words. We also introduce the subword universality signature for words, that leads to simple algorithms for the universality indexes of SLP-compressed words. △ Less

Submitted 24 April, 2023; originally announced April 2023.

Comments: Accepted for publication in Proc. 14th Int. Conf. Combinatorics on Words (WORDS 2023)

On flat lossy channel machines

Authors: Philippe Schnoebelen

Abstract: We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds alr… ▽ More We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds already apply to acyclic or single-path machines. △ Less

Submitted 10 July, 2020; originally announced July 2020.

Comments: Submitted for publication

The Ideal Approach to Computing Closed Subsets in Well-Quasi-Ordering

Authors: Jean Goubault-Larrecq, Simon Halfon, Prateek Karandikar, K. Narayan Kumar, Philippe Schnoebelen

Abstract: Elegant and general algorithms for handling upwards-closed and downwards-closed subsets of WQOs can be developed using the filter-based and ideal-based representation for these sets. These algorithms can be built in a generic or parameterized way, in parallel with the way complex WQOs are obtained by combining or modifying simpler WQOs. Elegant and general algorithms for handling upwards-closed and downwards-closed subsets of WQOs can be developed using the filter-based and ideal-based representation for these sets. These algorithms can be built in a generic or parameterized way, in parallel with the way complex WQOs are obtained by combining or modifying simpler WQOs. △ Less

Submitted 24 April, 2019; originally announced April 2019.

On Functions Weakly Computable by Pushdown Petri Nets and Related Systems

Authors: J. Leroux, M. Praveen, Ph. Schnoebelen, G. Sutre

Abstract: We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions $F_α$ for $α<ω^ω$, hence they are computationally more powerful than standard vector addition systems. On the other hand they cannot weakly compute the inverses $F_α^{-1}$ or indeed any sublinear function. T… ▽ More We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions $F_α$ for $α<ω^ω$, hence they are computationally more powerful than standard vector addition systems. On the other hand they cannot weakly compute the inverses $F_α^{-1}$ or indeed any sublinear function. The proof relies on a pum** lemma for runs of GVASes that is of independent interest. △ Less

Submitted 17 December, 2019; v1 submitted 8 April, 2019; originally announced April 2019.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 4 (December 18, 2019) lmcs:5362

On shuffle products, acyclic automata and piecewise-testable languages

Authors: Simon Halfon, Philippe Schnoebelen

Abstract: We show that the shuffle $L \unicode{x29E2} F$ of a piecewise-testable language $L$ and a finite language $F$ is piecewise-testable. The proof relies on a classic but little-used automata-theoretic characterization of piecewise-testable languages. We also discuss some mild generalizations of the main result, and provide bounds on the piecewise complexity of $L \unicode{x29E2} F$. We show that the shuffle $L \unicode{x29E2} F$ of a piecewise-testable language $L$ and a finite language $F$ is piecewise-testable. The proof relies on a classic but little-used automata-theoretic characterization of piecewise-testable languages. We also discuss some mild generalizations of the main result, and provide bounds on the piecewise complexity of $L \unicode{x29E2} F$. △ Less

Submitted 1 February, 2019; v1 submitted 6 October, 2018; originally announced October 2018.

Journal ref: Information Processing Letters, 145:68-73, 2019

Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering

Authors: Simon Halfon, Philippe Schnoebelen, Georg Zetzsche

Abstract: We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over langua… ▽ More We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the $Σ_2$ fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable. △ Less

Submitted 24 September, 2021; v1 submitted 25 January, 2017; originally announced January 2017.

Comments: 26 pages, 1 table

The height of piecewise-testable languages and the complexity of the logic of subwords

Authors: Prateek Karandikar, Philippe Schnoebelen

Abstract: The height of a piecewise-testable language $L$ is the maximum length of the words needed to define $L$ by excluding and requiring given subwords. The height of $L$ is an important descriptive complexity measure that has not yet been investigated in a systematic way. This article develops a series of new techniques for bounding the height of finite languages and of languages obtained by taking clo… ▽ More The height of a piecewise-testable language $L$ is the maximum length of the words needed to define $L$ by excluding and requiring given subwords. The height of $L$ is an important descriptive complexity measure that has not yet been investigated in a systematic way. This article develops a series of new techniques for bounding the height of finite languages and of languages obtained by taking closures by subwords, superwords and related operations. As an application of these results, we show that $\mathsf{FO}^2(A^*,\sqsubseteq)$, the two-variable fragment of the first-order logic of sequences with the subword ordering, can only express piecewise-testable properties and has elementary complexity. △ Less

Submitted 28 April, 2019; v1 submitted 5 November, 2015; originally announced November 2015.

Comments: This article is a full version of "The height of piecewise-testable languages with applications in logical complexity", in Proc. CSL 2016, LIPiCS 62:37

ACM Class: F.4.1; F.4.3; F.3.1

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 2 (April 30, 2019) lmcs:4850

Decidability in the logic of subsequences and supersequences

Authors: Prateek Karandikar, Philippe Schnoebelen

Abstract: We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Σ_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO2 theory is decidable while the FO3 theory is undecidable. We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Σ_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO2 theory is decidable while the FO3 theory is undecidable. △ Less

Submitted 14 October, 2015; originally announced October 2015.

ACM Class: F.4.1; F.4.3

Journal ref: 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

On Reachability for Unidirectional Channel Systems Extended with Regular Tests

Authors: Jancar Petr, Prateek Karandikar, Philippe Schnoebelen

Abstract: "Unidirectional channel systems" (Chambart & Schnoebelen, CONCUR 2008) are finite-state systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equip** them with the possibility of testing regular properties on the contents of channels makes it undecidable. Decidability is… ▽ More "Unidirectional channel systems" (Chambart & Schnoebelen, CONCUR 2008) are finite-state systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equip** them with the possibility of testing regular properties on the contents of channels makes it undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on an elaborate reduction to a generalized version of Post's Embedding Problem. △ Less

Submitted 16 April, 2015; v1 submitted 16 May, 2014; originally announced June 2014.

Comments: An extended abstract of this work first appeared in IFIP-TCS 2012, LNCS 7604

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 2 (April 17, 2015) lmcs:876

On the state complexity of closures and interiors of regular languages with subwords and superwords

Authors: Prateek Karandikar, Matthias Niewerth, Philippe Schnoebelen

Abstract: The downward and upward closures of a regular language $L$ are obtained by collecting all the subwords and superwords of its elements, respectively. The downward and upward interiors of $L$ are obtained dually by collecting words having all their subwords and superwords in $L$, respectively. We provide lower and upper bounds on the size of the smallest automata recognizing these closures and inter… ▽ More The downward and upward closures of a regular language $L$ are obtained by collecting all the subwords and superwords of its elements, respectively. The downward and upward interiors of $L$ are obtained dually by collecting words having all their subwords and superwords in $L$, respectively. We provide lower and upper bounds on the size of the smallest automata recognizing these closures and interiors. We also consider the computational complexity of decision problems for closures of regular languages. △ Less

Submitted 1 December, 2015; v1 submitted 3 June, 2014; originally announced June 2014.

Journal ref: Theoretical Computer Science, 610:91-107, 2016

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

On the index of Simon's congruence for piecewise testability

Authors: Prateek Karandikar, Manfred Kufleitner, Philippe Schnoebelen

Abstract: Simon's congruence, denoted \sim_n, relates words having the same subwords of length up to n. We show that, over a k-letter alphabet, the number of words modulo \sim_n is in 2^{Θ(n^{k-1} log n)}. Simon's congruence, denoted \sim_n, relates words having the same subwords of length up to n. We show that, over a k-letter alphabet, the number of words modulo \sim_n is in 2^{Θ(n^{k-1} log n)}. △ Less

Submitted 22 September, 2014; v1 submitted 3 October, 2013; originally announced October 2013.

Journal ref: Information Processing Letters, 115(4):515-519, 2015

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

Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor

Authors: Nathalie Bertrand, Philippe Schnoebelen

Abstract: We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized Büchi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on… ▽ More We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized Büchi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on probabilistic lossy channel systems. △ Less

Submitted 11 June, 2013; v1 submitted 19 July, 2012; originally announced July 2012.

Comments: In Proceedings QAPL 2013, arXiv:1306.2413

ACM Class: D.2.4; G.3; C.2.2

Journal ref: EPTCS 117, 2013, pp. 116-131

Generalized Post Embedding Problems

Authors: Prateek Karandikar, Philippe Schnoebelen

Abstract: The Regular Post Embedding Problem extended with partial (co)directness is shown decidable. This extends to universal and/or counting versions. It is also shown that combining directness and codirectness in Post Embedding problems leads to undecidability. The Regular Post Embedding Problem extended with partial (co)directness is shown decidable. This extends to universal and/or counting versions. It is also shown that combining directness and codirectness in Post Embedding problems leads to undecidability. △ Less

Submitted 23 May, 2014; v1 submitted 8 September, 2011; originally announced September 2011.

Journal ref: Theory of Computing Systems, 56(4):697-716, 2015

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

Toward a Compositional Theory of Leftist Grammars and Transformations

Authors: Pierre Chambart, Philippe Schnoebelen

Abstract: Leftist grammars [Motwani et al., STOC 2000] are special semi-Thue systems where symbols can only insert or erase to their left. We develop a theory of leftist grammars seen as word transformers as a tool toward rigorous analyses of their computational power. Our main contributions in this first paper are (1) constructions proving that leftist transformations are closed under compositions and tr… ▽ More Leftist grammars [Motwani et al., STOC 2000] are special semi-Thue systems where symbols can only insert or erase to their left. We develop a theory of leftist grammars seen as word transformers as a tool toward rigorous analyses of their computational power. Our main contributions in this first paper are (1) constructions proving that leftist transformations are closed under compositions and transitive closures, and (2) a proof that bounded reachability is NP-complete even for leftist grammars with acyclic rules. △ Less

Submitted 27 January, 2010; originally announced January 2010.

Comments: Full version of the FOSSACS 2010 paper

Journal ref: Proc. FoSSaCS'10, LNCS 6014, pages 237-251. Springer, 2010

On Termination for Faulty Channel Machines

Authors: Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell

Abstract: A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Tem… ▽ More A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity. △ Less

Submitted 20 February, 2008; originally announced February 2008.

Journal ref: Dans Proceedings of the 25th Annual Symposium on the Theoretical Aspects of Computer Science - STACS 2008, Bordeaux : France (2008)

On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems

Authors: C. Baier, N. Bertrand, Ph. Schnoebelen

Abstract: We prove a general finite convergence theorem for "upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems. We prove a general finite convergence theorem for "upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems. △ Less

Submitted 21 June, 2006; originally announced June 2006.

Comments: 16 pages

Journal ref: Proc. LPAR 2006, LNCS 4246, pp. 347-361, Springer 2006

Verifying nondeterministic probabilistic channel systems against $ω$-regular linear-time properties

Authors: Christel Baier, Nathalie Bertrand, Philippe Schnoebelen

Abstract: Lossy channel systems (LCSs) are systems of finite state automata that communicate via unreliable unbounded fifo channels. In order to circumvent the undecidability of model checking for nondeterministic LCSs, probabilistic models have been introduced, where it can be decided whether a linear-time property holds almost surely. However, such fully probabilistic systems are not a faithful model o… ▽ More Lossy channel systems (LCSs) are systems of finite state automata that communicate via unreliable unbounded fifo channels. In order to circumvent the undecidability of model checking for nondeterministic LCSs, probabilistic models have been introduced, where it can be decided whether a linear-time property holds almost surely. However, such fully probabilistic systems are not a faithful model of nondeterministic protocols. We study a hybrid model for LCSs where losses of messages are seen as faults occurring with some given probability, and where the internal behavior of the system remains nondeterministic. Thus the semantics is in terms of infinite-state Markov decision processes. The purpose of this article is to discuss the decidability of linear-time properties formalized by formulas of linear temporal logic (LTL). Our focus is on the qualitative setting where one asks, e.g., whether a LTL-formula holds almost surely or with zero probability (in case the formula describes the bad behaviors). Surprisingly, it turns out that -- in contrast to finite-state Markov decision processes -- the satisfaction relation for LTL formulas depends on the chosen type of schedulers that resolve the nondeterminism. While all variants of the qualitative LTL model checking problem for the full class of history-dependent schedulers are undecidable, the same questions for finite-memory scheduler can be solved algorithmically. However, the restriction to reachability properties and special kinds of recurrent reachability properties yields decidable verification problems for the full class of schedulers, which -- for this restricted class of properties -- are as powerful as finite-memory schedulers, or even a subclass of them. △ Less

Submitted 11 April, 2006; v1 submitted 4 November, 2005; originally announced November 2005.

Comments: 39 pages

Journal ref: ACM Trans. Computational Logic 9(1), 2007