2 Search Results for "Thomas, Bastien"

Document
DOI: 10.4230/LIPIcs.CONCUR.2021.15
Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms

Authors: Nathalie Bertrand, Bastien Thomas, and Josef Widder

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.
Cite as

Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2021.15,
  author =	{Bertrand, Nathalie and Thomas, Bastien and Widder, Josef},
  title =	{{Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.15},
  URN =		{urn:nbn:de:0030-drops-143926},
  doi =		{10.4230/LIPIcs.CONCUR.2021.15},
  annote =	{Keywords: Verification, Distributed algorithms, Domain theory}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2010.130
Column Generation Heuristic for a Rich Arc Routing Problem

Authors: Sébastien Lannez, Christian Artigues, Jean Damay, and Michel Gendreau

Published in: OASIcs, Volume 14, 10th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS'10) (2010)

Abstract
In this paper we address a real world optimisation problem, the Rail Track Inspection Scheduling Problem (RTISP). This problem consists of scheduling network inspection tasks. The objective is to minimise total deadhead distance. A mixed integer formulation of the problem is presented. A column generation based algorithm is proposed to solve this rich arc routing problem. Its performance is analysed by benchmarking a real world dataset from the French national railway company (SNCF). The efficiency of the algorithm is compared to an enhanced greedy algorithm. Its ability to schedule one year of inspection tasks on a sparse graph with thousand nodes, arcs and edges is assessed.
Cite as

Sébastien Lannez, Christian Artigues, Jean Damay, and Michel Gendreau. Column Generation Heuristic for a Rich Arc Routing Problem. In 10th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS'10). Open Access Series in Informatics (OASIcs), Volume 14, pp. 130-141, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{lannez_et_al:OASIcs.ATMOS.2010.130,
  author =	{Lannez, S\'{e}bastien and Artigues, Christian and Damay, Jean and Gendreau, Michel},
  title =	{{Column Generation Heuristic for a Rich Arc Routing Problem}},
  booktitle =	{10th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS'10)},
  pages =	{130--141},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-20-0},
  ISSN =	{2190-6807},
  year =	{2010},
  volume =	{14},
  editor =	{Erlebach, Thomas and L\"{u}bbecke, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2010.130},
  URN =		{urn:nbn:de:0030-drops-27559},
  doi =		{10.4230/OASIcs.ATMOS.2010.130},
  annote =	{Keywords: arc routing, column generation, heuristic, railtrack maintenance}
}
  • Refine by Author
  • 1 Artigues, Christian
  • 1 Bertrand, Nathalie
  • 1 Damay, Jean
  • 1 Gendreau, Michel
  • 1 Lannez, Sébastien
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Distributed algorithms
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 Distributed algorithms
  • 1 Domain theory
  • 1 Verification
  • 1 arc routing
  • 1 column generation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2010
  • 1 2021

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