Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
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)
@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} }
Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
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)
@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} }
Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
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)
@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} }
Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)
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)
@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} }
Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
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)
@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} }
Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
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)
@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} }
Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
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)
@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} }
Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)
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)
@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} }