Search Results

Documents authored by Jancar, Petr

Found 2 Possible Name Variants:

Jancar, Petr

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.36
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.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
DOI: 10.4230/LIPIcs.MFCS.2021.63
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.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
DOI: 10.4230/LIPIcs.MFCS.2016.52
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.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
DOI: 10.4230/LIPIcs.FSTTCS.2012.448
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.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}
}

Jančar, Petr

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.36
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.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
DOI: 10.4230/LIPIcs.MFCS.2021.63
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.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
DOI: 10.4230/LIPIcs.MFCS.2016.52
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.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
DOI: 10.4230/LIPIcs.FSTTCS.2012.448
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.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}
}
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