9 Search Results for "Sutre, Grégoire"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.136
Improved Algorithm for Reachability in d-VASS

Authors: Yuxi Fu, Qizhe Yang, and Yangluo Zheng

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
An 𝖥_{d} upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where 𝖥_d is the d-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the 2-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the 𝖥_{d + 4} upper bound due to Leroux and Schmitz (LICS 2019).
Cite as

Yuxi Fu, Qizhe Yang, and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 136:1-136:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fu_et_al:LIPIcs.ICALP.2024.136,
  author =	{Fu, Yuxi and Yang, Qizhe and Zheng, Yangluo},
  title =	{{Improved Algorithm for Reachability in d-VASS}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{136:1--136:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.136},
  URN =		{urn:nbn:de:0030-drops-202799},
  doi =		{10.4230/LIPIcs.ICALP.2024.136},
  annote =	{Keywords: Petri net, vector addition system, reachability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.141
Flattability of Priority Vector Addition Systems

Authors: Roland Guttenberg

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS due to [Jérôme Leroux, 2013]. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.
Cite as

Roland Guttenberg. Flattability of Priority Vector Addition Systems. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 141:1-141:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guttenberg:LIPIcs.ICALP.2024.141,
  author =	{Guttenberg, Roland},
  title =	{{Flattability of Priority Vector Addition Systems}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{141:1--141:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.141},
  URN =		{urn:nbn:de:0030-drops-202848},
  doi =		{10.4230/LIPIcs.ICALP.2024.141},
  annote =	{Keywords: Priority Vector Addition Systems, Semilinear, Inductive Invariants, Geometry, Flattability, Almost Semilinear, Transformer Relation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.153
On the Length of Strongly Monotone Descending Chains over ℕ^d

Authors: Sylvain Schmitz and Lia Schütze

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Węgrzycki (ICALP 2023) bounds the running time for the coverability problem in d-dimensional vector addition systems under unary encoding to n^{2^{O(d)}}, improving on Rackoff’s n^{2^{O(dlg d)}} upper bound (Theor. Comput. Sci. 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazić and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput. 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over ℕ^d that arise from the dual backward coverability algorithm of Lazić and Schmitz on d-dimensional unary vector addition systems also enjoy this tight n^{2^{O(d)}} upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazić and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS 2017) for the coverability problem in invertible affine nets.
Cite as

Sylvain Schmitz and Lia Schütze. On the Length of Strongly Monotone Descending Chains over ℕ^d. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 153:1-153:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{schmitz_et_al:LIPIcs.ICALP.2024.153,
  author =	{Schmitz, Sylvain and Sch\"{u}tze, Lia},
  title =	{{On the Length of Strongly Monotone Descending Chains over \mathbb{N}^d}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{153:1--153:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.153},
  URN =		{urn:nbn:de:0030-drops-202964},
  doi =		{10.4230/LIPIcs.ICALP.2024.153},
  annote =	{Keywords: Vector addition system, coverability, well-quasi-order, order ideal, affine net}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.37
Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free

Authors: Jérôme Leroux and Grégoire Sutre

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.
Cite as

Jérôme Leroux and Grégoire Sutre. Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.CONCUR.2020.37,
  author =	{Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.37},
  URN =		{urn:nbn:de:0030-drops-128498},
  doi =		{10.4230/LIPIcs.CONCUR.2020.37},
  annote =	{Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Infinite-state system}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.31
Reachability for Two-Counter Machines with One Test and One Reset

Authors: Alain Finkel, Jérôme Leroux, and Grégoire Sutre

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.
Cite as

Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for Two-Counter Machines with One Test and One Reset. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2018.31,
  author =	{Finkel, Alain and Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Reachability for Two-Counter Machines with One Test and One Reset}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{31:1--31:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.31},
  URN =		{urn:nbn:de:0030-drops-99305},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.31},
  annote =	{Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Presburger arithmetic, Infinite-state system}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.44
On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems

Authors: Vincent Penelle, Sylvain Salvati, and Grégoire Sutre

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness. We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.
Cite as

Vincent Penelle, Sylvain Salvati, and Grégoire Sutre. On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{penelle_et_al:LIPIcs.FSTTCS.2018.44,
  author =	{Penelle, Vincent and Salvati, Sylvain and Sutre, Gr\'{e}goire},
  title =	{{On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{44:1--44:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.44},
  URN =		{urn:nbn:de:0030-drops-99432},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.44},
  annote =	{Keywords: Higher-order pushdown automata, Vector addition systems, Boundedness problem, Termination problem, Coverability problem}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.119
Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One

Authors: Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre

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

Abstract
Whether the reachability problem for branching vector addition systems, or equivalently the provability problem for multiplicative exponential linear logic, is decidable has been a long-standing open question. The one-dimensional case is a generalisation of the extensively studied one-counter nets, and it was recently established polynomial-time complete provided counter updates are given in unary. Our main contribution is to determine the complexity when the encoding is binary: polynomial-space complete.
Cite as

Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 119:1-119:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{figueira_et_al:LIPIcs.ICALP.2017.119,
  author =	{Figueira, Diego and Lazic, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip and Sutre, Gr\'{e}goire},
  title =	{{Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{119:1--119:14},
  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.119},
  URN =		{urn:nbn:de:0030-drops-74374},
  doi =		{10.4230/LIPIcs.ICALP.2017.119},
  annote =	{Keywords: branching vector addition systems, reachability problem}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.224
Safety Verification of Communicating One-Counter Machines

Authors: Alexander Heußner, Tristan Le Gall, and Grégoire Sutre

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

Abstract
In order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, FIFO channels. This model extends communicating finite-state machines (CFSM) by infinite-state local processes and an infinite message alphabet. The main result of the paper is a complete characterization of the communication topologies that have a solvable reachability question. As already CFSM exclude the possibility of automatic verification in presence of mutual communication, we also consider an under-approximative approach to the reachability problem, based on rendezvous synchronization.
Cite as

Alexander Heußner, Tristan Le Gall, and Grégoire Sutre. Safety Verification of Communicating One-Counter Machines. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 224-235, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{heuner_et_al:LIPIcs.FSTTCS.2012.224,
  author =	{Heu{\ss}ner, Alexander and Le Gall, Tristan and Sutre, Gr\'{e}goire},
  title =	{{Safety Verification of Communicating One-Counter Machines}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{224--235},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.224},
  URN =		{urn:nbn:de:0030-drops-38614},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.224},
  annote =	{Keywords: Counter Machines, FIFO Channels, Reachability Problem, Data Words}
}
Document
DOI: 10.4230/DagSemProc.06081.4
Flat counter automata almost everywhere!

Authors: Jérôme Leroux and Grégoire Sutre

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
This paper argues that flatness appears as a central notion in the verification of counter automata. A counter automaton is called flat when its control graph can be ``replaced'', equivalently w.r.t. reachability, by another one with no nested loops. From a practical view point, we show that flatness is a necessary and sufficient condition for termination of accelerated symbolic model checking, a generic semi-algorithmic technique implemented in successful tools like FAST, LASH or TReX. From a theoretical view point, we prove that many known semilinear subclasses of counter automata are flat: reversal bounded counter machines, lossy vector addition systems with states, reversible Petri nets, persistent and conflict-free Petri nets, etc. Hence, for these subclasses, the semilinear reachability set can be computed using a emph{uniform} accelerated symbolic procedure (whereas previous algorithms were specifically designed for each subclass).
Cite as

Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere!. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{leroux_et_al:DagSemProc.06081.4,
  author =	{Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Flat counter automata almost everywhere!}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.4},
  URN =		{urn:nbn:de:0030-drops-7297},
  doi =		{10.4230/DagSemProc.06081.4},
  annote =	{Keywords: Symbolic representation, Infinite state system, Acceleration, Meta-transition}
}
  • Refine by Author
  • 6 Sutre, Grégoire
  • 4 Leroux, Jérôme
  • 1 Figueira, Diego
  • 1 Finkel, Alain
  • 1 Fu, Yuxi
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Logic and verification
  • 2 Theory of computation → Models of computation
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Parameterized complexity and exact algorithms

  • Refine by Keyword
  • 3 Vector addition system
  • 2 Counter machine
  • 2 Formal verification
  • 2 Infinite-state system
  • 2 Reachability problem
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 3 2024
  • 2 2018
  • 1 2006
  • 1 2012
  • 1 2017
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact