Document

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail