5 Search Results for "Mascle, Corto"

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.24
Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints

Authors: Corto Mascle, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.
Cite as

Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mascle_et_al:LIPIcs.CONCUR.2023.24,
  author =	{Mascle, Corto and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.24},
  URN =		{urn:nbn:de:0030-drops-190184},
  doi =		{10.4230/LIPIcs.CONCUR.2023.24},
  annote =	{Keywords: Parametric systems, Locks, Model-checking}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.125
Distributed Controller Synthesis for Deadlock Avoidance

Authors: Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes complete for the second level of the polynomial time hierarchy, and even in Ptime under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is Nexptime-complete. The drinking philosophers problem falls in this case.
Cite as

Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Distributed Controller Synthesis for Deadlock Avoidance. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 125:1-125:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gimbert_et_al:LIPIcs.ICALP.2022.125,
  author =	{Gimbert, Hugo and Mascle, Corto and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Distributed Controller Synthesis for Deadlock Avoidance}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{125:1--125:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.125},
  URN =		{urn:nbn:de:0030-drops-164668},
  doi =		{10.4230/LIPIcs.ICALP.2022.125},
  annote =	{Keywords: Distributed Synthesis, Concurrency, Lock Synchronisation, Deadlock Avoidance}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.49
Keyboards as a New Model of Computation

Authors: Yoan Géran, Bastien Laboureix, Corto Mascle, and Valentin D. Richard

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We introduce a new formalisation of language computation, called keyboards. We consider a set of atomic operations (writing a letter, erasing a letter, going to the right or to the left) and we define a keyboard as a set of finite sequences of such operations, called keys. The generated language is the set of words obtained by applying some non-empty sequence of those keys. Unlike classical models of computation, every key can be applied anytime. We define various classes of languages based on different sets of atomic operations, and compare their expressive powers. We also compare them to rational, context-free and context-sensitive languages. We obtain a strict hierarchy of classes, whose expressiveness is orthogonal to the one of the aforementioned classical models. We also study closure properties of those classes, as well as fundamental complexity problems on keyboards.
Cite as

Yoan Géran, Bastien Laboureix, Corto Mascle, and Valentin D. Richard. Keyboards as a New Model of Computation. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 49:1-49:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{geran_et_al:LIPIcs.MFCS.2021.49,
  author =	{G\'{e}ran, Yoan and Laboureix, Bastien and Mascle, Corto and Richard, Valentin D.},
  title =	{{Keyboards as a New Model of Computation}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{49:1--49:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.49},
  URN =		{urn:nbn:de:0030-drops-144896},
  doi =		{10.4230/LIPIcs.MFCS.2021.49},
  annote =	{Keywords: formal languages, models of computation, automata theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.29
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas

Authors: Corto Mascle and Martin Zimmermann

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border. First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.
Cite as

Corto Mascle and Martin Zimmermann. The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{mascle_et_al:LIPIcs.CSL.2020.29,
  author =	{Mascle, Corto and Zimmermann, Martin},
  title =	{{The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.29},
  URN =		{urn:nbn:de:0030-drops-116720},
  doi =		{10.4230/LIPIcs.CSL.2020.29},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2019.43
On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words

Authors: Stefan Kiefer and Corto Mascle

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
Let n be a natural number and M a set of n x n-matrices over the nonnegative integers such that M generates a finite multiplicative monoid. We show that if the zero matrix 0 is a product of matrices in M, then there are M_1, ..., M_{n^5} in M with M_1 *s M_{n^5} = 0. This result has applications in automata theory and the theory of codes. Specifically, if X subset Sigma^* is a finite incomplete code, then there exists a word w in Sigma^* of length polynomial in sum_{x in X} |x| such that w is not a factor of any word in X^*. This proves a weak version of Restivo’s conjecture.
Cite as

Stefan Kiefer and Corto Mascle. On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 43:1-43:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.STACS.2019.43,
  author =	{Kiefer, Stefan and Mascle, Corto},
  title =	{{On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{43:1--43:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.43},
  URN =		{urn:nbn:de:0030-drops-102823},
  doi =		{10.4230/LIPIcs.STACS.2019.43},
  annote =	{Keywords: matrix semigroups, unambiguous automata, codes, Restivo’s conjecture}
}
  • Refine by Author
  • 5 Mascle, Corto
  • 2 Muscholl, Anca
  • 2 Walukiewicz, Igor
  • 1 Gimbert, Hugo
  • 1 Géran, Yoan
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Distributed computing models
  • 1 Theory of computation
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Concurrency
  • 1 Deadlock Avoidance
  • 1 Distributed Synthesis
  • 1 Hyperproperties
  • 1 Linear Temporal Logic
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 1 2019
  • 1 2020
  • 1 2021
  • 1 2022
  • 1 2023

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