2 Search Results for "Jezequel, Loig"

Document
DOI: 10.4230/LIPIcs.CONCUR.2016.17
Lazy Reachability Analysis in Distributed Systems

Authors: Loïg Jezequel and Didier Lime

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We address the problem of reachability in distributed systems, modelled as networks of finite automata and propose and prove a new algorithm to solve it efficiently in many cases. This algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. We have implemented this algorithm in an early prototype and provide some very encouraging experimental results.
Cite as

Loïg Jezequel and Didier Lime. Lazy Reachability Analysis in Distributed Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{jezequel_et_al:LIPIcs.CONCUR.2016.17,
  author =	{Jezequel, Lo\"{i}g and Lime, Didier},
  title =	{{Lazy Reachability Analysis in Distributed Systems}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.17},
  URN =		{urn:nbn:de:0030-drops-61545},
  doi =		{10.4230/LIPIcs.CONCUR.2016.17},
  annote =	{Keywords: Reachability analysis, Compositional verification, Automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.225
Computation of Summaries Using Net Unfoldings

Authors: Javier Esparza, Loig Jezequel, and Stefan Schwoon

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

Abstract
We study the following summarization problem: given a parallel composition A=A_1||...||A_n of labelled transition systems communicating with the environment through a distinguished component A_i, efficiently compute a summary S_i such that E||A and E||S_i are trace-equivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of MOLE, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.
Cite as

Javier Esparza, Loig Jezequel, and Stefan Schwoon. Computation of Summaries Using Net Unfoldings. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 225-236, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.FSTTCS.2013.225,
  author =	{Esparza, Javier and Jezequel, Loig and Schwoon, Stefan},
  title =	{{Computation of Summaries Using Net Unfoldings}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{225--236},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.225},
  URN =		{urn:nbn:de:0030-drops-43759},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.225},
  annote =	{Keywords: Net unfoldings, Concurrent systems, Petri nets}
}
  • Refine by Author
  • 1 Esparza, Javier
  • 1 Jezequel, Loig
  • 1 Jezequel, Loïg
  • 1 Lime, Didier
  • 1 Schwoon, Stefan

  • Refine by Classification

  • Refine by Keyword
  • 1 Automata
  • 1 Compositional verification
  • 1 Concurrent systems
  • 1 Net unfoldings
  • 1 Petri nets
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2013
  • 1 2016

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