2 Search Results for "Long, Huan"

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.2020.141

Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete

Authors: Wenbo Zhang, Qiang Yin, Huan Long, and Xian Xu

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract

Deciding bisimulation equivalence of two pushdown automata is one of the most fundamental problems in formal verification. Though Sénizergues established decidability of this problem in 1998, it has taken a long time to understand its complexity: the problem was proven to be non-elementary in 2013, and only recently, Jančar and Schmitz showed that it has an Ackermann upper bound. We improve the lower bound to Ackermann-hard, and thus close the complexity gap.

Cite as

Wenbo Zhang, Qiang Yin, Huan Long, and Xian Xu. Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 141:1-141:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICALP.2020.141,
  author =	{Zhang, Wenbo and Yin, Qiang and Long, Huan and Xu, Xian},
  title =	{{Bisimulation Equivalence of Pushdown Automata Is Ackermann-Complete}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{141:1--141:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.141},
  URN =		{urn:nbn:de:0030-drops-125482},
  doi =		{10.4230/LIPIcs.ICALP.2020.141},
  annote =	{Keywords: PDA, Bisimulation, Equivalence checking}
}

Refine by Author
1 Fu, Yuxi
1 Long, Huan
1 Xu, Xian
1 Yang, Qizhe
1 Yin, Qiang
Show More...

Refine by Classification
2 Theory of computation → Logic and verification
1 Theory of computation → Formal languages and automata theory
1 Theory of computation → Models of computation

Refine by Keyword
1 Bisimulation
1 Equivalence checking
1 PDA
1 Petri net
1 reachability
Show More...

Refine by Type
2 document

Refine by Publication Year
1 2020
1 2024