Search Results

Documents authored by Schnoebelen, Philippe

Document
DOI: 10.4230/LIPIcs.CSL.2021.37
On Flat Lossy Channel Machines

Authors: Philippe Schnoebelen

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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 already apply to acyclic or single-path machines.
Cite as

Philippe Schnoebelen. On Flat Lossy Channel Machines. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 37:1-37:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{schnoebelen:LIPIcs.CSL.2021.37,
  author =	{Schnoebelen, Philippe},
  title =	{{On Flat Lossy Channel Machines}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{37:1--37:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.37},
  URN =		{urn:nbn:de:0030-drops-134712},
  doi =		{10.4230/LIPIcs.CSL.2021.37},
  annote =	{Keywords: Infinite state systems, Automated verification, Flat systems, Lossy channels}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2017.85
Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk)

Authors: Philippe Schnoebelen

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We explain how the downward-closed subsets of a well-quasi-ordering (X,\leq) can be represented via the ideals of X and how this leads to simple and efficient algorithms for the verification of well-structured systems.
Cite as

Philippe Schnoebelen. Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk). In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 85:1-85:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{schnoebelen:LIPIcs.MFCS.2017.85,
  author =	{Schnoebelen, Philippe},
  title =	{{Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{85:1--85:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.85},
  URN =		{urn:nbn:de:0030-drops-81393},
  doi =		{10.4230/LIPIcs.MFCS.2017.85},
  annote =	{Keywords: Well-structured systems and verification, Order theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.37
The Height of Piecewise-Testable Languages with Applications in Logical Complexity

Authors: Prateek Karandikar and Philippe Schnoebelen

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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 paper 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 FO^2(A^*, subword), 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.
Cite as

Prateek Karandikar and Philippe Schnoebelen. The Height of Piecewise-Testable Languages with Applications in Logical Complexity. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 37:1-37:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{karandikar_et_al:LIPIcs.CSL.2016.37,
  author =	{Karandikar, Prateek and Schnoebelen, Philippe},
  title =	{{The Height of Piecewise-Testable Languages with Applications in Logical Complexity}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{37:1--37:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.37},
  URN =		{urn:nbn:de:0030-drops-65776},
  doi =		{10.4230/LIPIcs.CSL.2016.37},
  annote =	{Keywords: Descriptive complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.84
Decidability in the Logic of Subsequences and Supersequences

Authors: Prateek Karandikar and Philippe Schnoebelen

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Sigma_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO^2 theory is decidable while the FO^3 theory is undecidable.
Cite as

Prateek Karandikar and Philippe Schnoebelen. Decidability in the Logic of Subsequences and Supersequences. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 84-97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{karandikar_et_al:LIPIcs.FSTTCS.2015.84,
  author =	{Karandikar, Prateek and Schnoebelen, Philippe},
  title =	{{Decidability in the Logic of Subsequences and Supersequences}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{84--97},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.84},
  URN =		{urn:nbn:de:0030-drops-56428},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.84},
  annote =	{Keywords: subsequence, subword, logic, first-order logic, decidability, piecewise- testability, Simon’s congruence}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1339
On Termination for Faulty Channel Machines

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

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

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 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.
Cite as

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination for Faulty Channel Machines. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.STACS.2008.1339,
  author =	{Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo\"{e}l and Schnoebelen, Philippe and Worrell, James},
  title =	{{On Termination for Faulty Channel Machines}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{121--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1339},
  URN =		{urn:nbn:de:0030-drops-13390},
  doi =		{10.4230/LIPIcs.STACS.2008.1339},
  annote =	{Keywords: Automated Verification, Computational Complexity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact