7 Search Results for "Fournier, Paulin"

Document
DOI: 10.4230/LIPIcs.CSL.2026.31
Parametric Disjunctive Timed Networks

Authors: Étienne André, Swen Jacobs, and Engel Lefaucheux

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e., unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters - a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants.
Cite as

Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric Disjunctive Timed Networks. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 31:1-31:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.CSL.2026.31,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Lefaucheux, Engel},
  title =	{{Parametric Disjunctive Timed Networks}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{31:1--31:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.31},
  URN =		{urn:nbn:de:0030-drops-254562},
  doi =		{10.4230/LIPIcs.CSL.2026.31},
  annote =	{Keywords: parametrised verification, parametric timed automata, verification of infinite-state systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.8
Parameterized Verification of Timed Networks with Clock Invariants

Authors: Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur

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

Abstract
We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with k-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al. (2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable.
Cite as

Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur. Parameterized Verification of Timed Networks with Clock Invariants. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.FSTTCS.2025.8,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Karra, Shyam Lal and Sankur, Ocan},
  title =	{{Parameterized Verification of Timed Networks with Clock Invariants}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.8},
  URN =		{urn:nbn:de:0030-drops-250878},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.8},
  annote =	{Keywords: Networks of Timed Automata, Parameterized Verification, Timed Petri Nets}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.68
Slightly Non-Linear Higher-Order Tree Transducers

Authors: Lê Thành Dũng (Tito) Nguyễn and Gabriele Vanoni

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We investigate the tree-to-tree functions computed by "affine λ-transducers": tree automata whose memory consists of an affine λ-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati’s Linear High-Order Deterministic Tree Transducers. When the memory is almost purely affine (à la Kanazawa), we show that these machines can be translated to tree-walking transducers (and with a purely affine memory, we get a reversible tree-walking transducer). This leads to a proof of an inexpressivity conjecture of Nguyễn and Pradic on "implicit automata" in an affine λ-calculus. We also prove that a more powerful variant, extended with preprocessing by an MSO relabeling and allowing a limited amount of non-linearity, is equivalent in expressive power to Engelfriet, Hoogeboom and Samwel’s invisible pebble tree transducers. The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of Girard’s geometry of interaction, a semantics of linear logic. We work with ad-hoc specializations to λ-terms of low exponential depth of a tree-generating version of the IAM.
Cite as

Lê Thành Dũng (Tito) Nguyễn and Gabriele Vanoni. Slightly Non-Linear Higher-Order Tree Transducers. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 68:1-68:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.STACS.2025.68,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Vanoni, Gabriele},
  title =	{{Slightly Non-Linear Higher-Order Tree Transducers}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{68:1--68:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.68},
  URN =		{urn:nbn:de:0030-drops-228934},
  doi =		{10.4230/LIPIcs.STACS.2025.68},
  annote =	{Keywords: Almost affine lambda-calculus, geometry of interaction, reversibility, tree transducers, tree-walking automata}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.13
Alternating Nonzero Automata

Authors: Paulin Fournier and Hugo Gimbert

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We introduce a new class of automata on infinite trees called alternating nonzero automata, which extends the class of non-deterministic nonzero automata. The emptiness problem for this class is still open, however we identify a subclass, namely limited choice, for which we reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain, as corollaries, algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.
Cite as

Paulin Fournier and Hugo Gimbert. Alternating Nonzero Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fournier_et_al:LIPIcs.CONCUR.2018.13,
  author =	{Fournier, Paulin and Gimbert, Hugo},
  title =	{{Alternating Nonzero Automata}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.13},
  URN =		{urn:nbn:de:0030-drops-95517},
  doi =		{10.4230/LIPIcs.CONCUR.2018.13},
  annote =	{Keywords: zero-automata, probabilities, temporal logics}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.113
On Reversible Transducers

Authors: Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition. However, the best known algorithms for composing two-way transducers cause a double exponential blow-up in the size of the inputs. In this paper, we introduce a class of transducers for which the composition has polynomial complexity. It is the class of reversible transducers, for which the computation steps can be reversed deterministically. While in the one-way setting this class is not very expressive, we prove that any two-way transducer can be made reversible through a single exponential blow-up. As a consequence, we prove that the composition of two-way transducers can be done with a single exponential blow-up in the number of states. A uniformization of a relation is a function with the same domain and which is included in the original relation. Our main result actually states that we can uniformize any non-deterministic two-way transducer by a reversible transducer with a single exponential blow-up, improving the known result by de Souza which has a quadruple exponential complexity. As a side result, our construction also gives a quadratic transformation from copyless streaming string transducers to two-way transducers, improving the exponential previous bound.
Cite as

Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote. On Reversible Transducers. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 113:1-113:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dartois_et_al:LIPIcs.ICALP.2017.113,
  author =	{Dartois, Luc and Fournier, Paulin and Jecker, Isma\"{e}l and Lhote, Nathan},
  title =	{{On Reversible Transducers}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{113:1--113:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.113},
  URN =		{urn:nbn:de:0030-drops-74491},
  doi =		{10.4230/LIPIcs.ICALP.2017.113},
  annote =	{Keywords: Transducers, reversibility, two-way, uniformization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.44
Distributed Local Strategies in Broadcast Networks

Authors: Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We study the problems of reaching a specific control state, or converging to a set of target states, in networks with a parameterized number of identical processes communicating via broadcast. To reflect the distributed aspect of such networks, we restrict our attention to executions in which all the processes must follow the same local strategy that, given their past performed actions and received messages, provides the next action to be performed. We show that the reachability and target problems under such local strategies are NP-complete, assuming that the set of receivers is chosen non-deterministically at each step. On the other hand, these problems become undecidable when the communication topology is a clique. However, decidability can be regained for reachability under the additional assumption that all processes are bound to receive the broadcast messages.
Cite as

Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed Local Strategies in Broadcast Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 44-57, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2015.44,
  author =	{Bertrand, Nathalie and Fournier, Paulin and Sangnier, Arnaud},
  title =	{{Distributed Local Strategies in Broadcast Networks}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{44--57},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.44},
  URN =		{urn:nbn:de:0030-drops-53796},
  doi =		{10.4230/LIPIcs.CONCUR.2015.44},
  annote =	{Keywords: Broadcast networks, parameterized verification, local strategies}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.501
Parameterized Verification of Many Identical Probabilistic Timed Processes

Authors: Nathalie Bertrand and Paulin Fournier

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
Parameterized verification aims at validating a system's model irrespective of the value of a parameter. We introduce a model for networks of identical probabilistic timed processes, where the number of processes is a parameter. Each process is a probabilistic single-clock timed automaton and communicates with the others by broadcasting. The number of processes either is constant (static case), or evolves over time through random disappearances and creations (dynamic case). An example of relevant parameterized verification problem for these systems is whether, independently of the number of processes, a configuration where one process is in a target state is reached almost-surely under all scheduling policies. On the one hand, most parameterized verification problems turn out to be undecidable in the static case (even for untimed processes). On the other hand, we prove their decidability in the dynamic case.
Cite as

Nathalie Bertrand and Paulin Fournier. Parameterized Verification of Many Identical Probabilistic Timed Processes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 501-513, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2013.501,
  author =	{Bertrand, Nathalie and Fournier, Paulin},
  title =	{{Parameterized Verification of Many Identical Probabilistic Timed Processes}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{501--513},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.501},
  URN =		{urn:nbn:de:0030-drops-43964},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.501},
  annote =	{Keywords: model checking, Markov decision processes, parameterized verification}
}
  • Refine by Type
  • 7 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 1 2018
  • 1 2017
  • 1 2015
  • Show More...

  • Refine by Author
  • 4 Fournier, Paulin
  • 2 André, Étienne
  • 2 Bertrand, Nathalie
  • 2 Jacobs, Swen
  • 1 Dartois, Luc
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 1 Software and its engineering → Model checking
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Transducers

  • Refine by Keyword
  • 2 parameterized verification
  • 2 reversibility
  • 1 Almost affine lambda-calculus
  • 1 Broadcast networks
  • 1 Markov decision processes
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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