6 Search Results for "Jančar, Petr"


Document
The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets

Authors: Petr Jančar and Jérôme Leroux

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
A set of configurations H is a home-space for a set of configurations X of a Petri net if every configuration reachable from (any configuration in) X can reach (some configuration in) H. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations X, H, if H is a home-space for X. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when X is a singleton and H is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any linear set of configurations L we can effectively compute a semilinear set C of configurations, called a non-reachability core for L, such that for every set X the set L is not a home-space for X if, and only if, C is reachable from X. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.

Cite as

Petr Jančar and Jérôme Leroux. The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{jancar_et_al:LIPIcs.CONCUR.2023.36,
  author =	{Jan\v{c}ar, Petr and Leroux, J\'{e}r\^{o}me},
  title =	{{The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.36},
  URN =		{urn:nbn:de:0030-drops-190300},
  doi =		{10.4230/LIPIcs.CONCUR.2023.36},
  annote =	{Keywords: Petri nets, home-space property, semilinear sets, Ackermannian complexity}
}
Document
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable

Authors: Wojciech Czerwiński and Piotr Hofman

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.

Cite as

Wojciech Czerwiński and Piotr Hofman. Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2022.16,
  author =	{Czerwi\'{n}ski, Wojciech and Hofman, Piotr},
  title =	{{Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{16:1--16:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.16},
  URN =		{urn:nbn:de:0030-drops-170796},
  doi =		{10.4230/LIPIcs.CONCUR.2022.16},
  annote =	{Keywords: vector addition systems, language inclusion, language equivalence, determinism, unambiguity, bounded ambiguity, Petri nets, well-structured transition systems}
}
Document
The Simplest Non-Regular Deterministic Context-Free Language

Authors: Petr Jančar and Jiří Šíma

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)


Abstract
We introduce a new notion of 𝒞-simple problems for a class 𝒞 of decision problems (i.e. languages), w.r.t. a particular reduction. A problem is 𝒞-simple if it can be reduced to each problem in 𝒞. This can be viewed as a conceptual counterpart to 𝒞-hard problems to which all problems in 𝒞 reduce. Our concrete example is the class of non-regular deterministic context-free languages (DCFL'), with a truth-table reduction by Mealy machines. The main technical result is a proof that the DCFL' language L_# = {0^n1^n ∣ n ≥ 1} is DCFL'-simple, and can be thus viewed as one of the simplest languages in the class DCFL', in a precise sense. The notion of DCFL'-simple languages is nontrivial: e.g., the language L_R = {wcw^R∣ w ∈ {a,b}^*} is not DCFL'-simple. By describing an application in the area of neural networks (elaborated in another paper), we demonstrate that 𝒞-simple problems under suitable reductions can provide a tool for expanding the lower-bound results known for single problems to the whole classes of problems.

Cite as

Petr Jančar and Jiří Šíma. The Simplest Non-Regular Deterministic Context-Free Language. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 63:1-63:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{jancar_et_al:LIPIcs.MFCS.2021.63,
  author =	{Jan\v{c}ar, Petr and \v{S}{\'\i}ma, Ji\v{r}{\'\i}},
  title =	{{The Simplest Non-Regular Deterministic Context-Free Language}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{63:1--63:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.63},
  URN =		{urn:nbn:de:0030-drops-145037},
  doi =		{10.4230/LIPIcs.MFCS.2021.63},
  annote =	{Keywords: deterministic context-free language, truth-table reduction, Mealy automaton, pushdown automaton}
}
Document
Two Lower Bounds for BPA

Authors: Mingzhang Huang and Qiang Yin

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)


Abstract
Branching bisimilarity of normed Basic Process Algebra (nBPA) was claimed to be EXPTIME-hard in previous papers without any explicit proof. Recently it has been pointed out by Petr Jancar that the claim lacked proper justification. In this paper, we develop a new complete proof for the EXPTIME-hardness of branching bisimilarity of nBPA. We also prove that the associated regularity problem of nBPA is PSPACE-hard. This improves previous P-hard result.

Cite as

Mingzhang Huang and Qiang Yin. Two Lower Bounds for BPA. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{huang_et_al:LIPIcs.CONCUR.2017.20,
  author =	{Huang, Mingzhang and Yin, Qiang},
  title =	{{Two Lower Bounds for BPA}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{20:1--20:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.20},
  URN =		{urn:nbn:de:0030-drops-77772},
  doi =		{10.4230/LIPIcs.CONCUR.2017.20},
  annote =	{Keywords: BPA, branching bisimulation, regularity}
}
Document
Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence

Authors: Petr Jancar

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)


Abstract
The problem if a given configuration of a pushdown automaton (PDA) is bisimilar with some (unspecified) finite-state process is shown to be decidable. The decidability is proven in the framework of first-order grammars, which are given by finite sets of labelled rules that rewrite roots of first-order terms. The framework is equivalent to PDA where also deterministic popping epsilon-steps are allowed, i.e. to the model for which Senizergues showed an involved procedure deciding bisimilarity (FOCS 1998). Such a procedure is here used as a black-box part of the algorithm. For deterministic PDA the regularity problem was shown decidable by Valiant (JACM 1975) but the decidability question for nondeterministic PDA, answered positively here, had been open (as indicated, e.g., by Broadbent and Goeller, FSTTCS 2012).

Cite as

Petr Jancar. Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 52:1-52:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{jancar:LIPIcs.MFCS.2016.52,
  author =	{Jancar, Petr},
  title =	{{Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{52:1--52:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.52},
  URN =		{urn:nbn:de:0030-drops-64649},
  doi =		{10.4230/LIPIcs.MFCS.2016.52},
  annote =	{Keywords: pushdown processes, first-order grammars, bisimulation, regularity}
}
Document
Bisimilarity of Probabilistic Pushdown Automata

Authors: Vojtech Forejt, Petr Jancar, Stefan Kiefer, and James Worrell

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


Abstract
We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata (without epsilon-transitions). Our first contribution is a general construction that reduces checking bisimilarity of probabilistic transition systems to checking bisimilarity of non-deterministic transition systems. This construction directly yields decidability of bisimilarity for pPDA, as well as an elementary upper bound for the bisimilarity problem on the subclass of probabilistic basic process algebras, i.e., single-state pPDA. We further show that, with careful analysis, the general reduction can be used to prove an EXPTIME upper bound for bisimilarity of probabilistic visibly pushdown automata. Here we also provide a matching lower bound, establishing EXPTIME-completeness. Finally we prove that deciding bisimilarity of probabilistic one-counter automata, another subclass of pPDA, is PSPACE-complete. Here we use a more specialised argument to obtain optimal complexity bounds.

Cite as

Vojtech Forejt, Petr Jancar, Stefan Kiefer, and James Worrell. Bisimilarity of Probabilistic Pushdown Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 448-460, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{forejt_et_al:LIPIcs.FSTTCS.2012.448,
  author =	{Forejt, Vojtech and Jancar, Petr and Kiefer, Stefan and Worrell, James},
  title =	{{Bisimilarity of Probabilistic Pushdown Automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{448--460},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.448},
  URN =		{urn:nbn:de:0030-drops-38800},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.448},
  annote =	{Keywords: bisimilarity, probabilistic systems, pushdown automata}
}
  • Refine by Author
  • 2 Jancar, Petr
  • 2 Jančar, Petr
  • 1 Czerwiński, Wojciech
  • 1 Forejt, Vojtech
  • 1 Hofman, Piotr
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Grammars and context-free languages
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Parallel computing models
  • 1 Theory of computation → Problems, reductions and completeness
  • 1 Theory of computation → Transducers

  • Refine by Keyword
  • 2 Petri nets
  • 2 regularity
  • 1 Ackermannian complexity
  • 1 BPA
  • 1 Mealy automaton
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 1 2012
  • 1 2016
  • 1 2017
  • 1 2021
  • 1 2022
  • Show More...

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