Search Results

Documents authored by Semukhin, Pavel

Document
DOI: 10.4230/LIPIcs.MFCS.2021.15
Decision Questions for Probabilistic Automata on Small Alphabets

Authors: Paul C. Bell and Pavel Semukhin

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

Abstract
We study the emptiness and λ-reachability problems for unary and binary Probabilistic Finite Automata (PFA) and characterise the complexity of these problems in terms of the degree of ambiguity of the automaton and the size of its alphabet. Our main result is that emptiness and λ-reachability are solvable in EXPTIME for polynomially ambiguous unary PFA and if, in addition, the transition matrix is over {0, 1}, we show they are in NP. In contrast to the Skolem-hardness of the λ-reachability and emptiness problems for exponentially ambiguous unary PFA, we show that these problems are NP-hard even for finitely ambiguous unary PFA. For binary polynomially ambiguous PFA with commuting transition matrices, we prove NP-hardness of the λ-reachability (dimension 9), nonstrict emptiness (dimension 37) and strict emptiness (dimension 40) problems.
Cite as

Paul C. Bell and Pavel Semukhin. Decision Questions for Probabilistic Automata on Small Alphabets. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bell_et_al:LIPIcs.MFCS.2021.15,
  author =	{Bell, Paul C. and Semukhin, Pavel},
  title =	{{Decision Questions for Probabilistic Automata on Small Alphabets}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{15:1--15:17},
  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.15},
  URN =		{urn:nbn:de:0030-drops-144559},
  doi =		{10.4230/LIPIcs.MFCS.2021.15},
  annote =	{Keywords: Probabilistic finite automata, unary alphabet, emptiness problem, bounded ambiguity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.6
Linear-Time Model Checking Branching Processes

Authors: Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
(Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing both transition systems and Markov chains (but not generally Markov decision processes). We study the complexity of model checking branching processes against linear-time omega-regular specifications: is it the case almost surely that every branch of a tree randomly generated by the branching process satisfies the omega-regular specification? The main result is that for LTL specifications this problem is in PSPACE, subsuming classical results for transition systems and Markov chains, respectively. The underlying general model-checking algorithm is based on the automata-theoretic approach, using unambiguous Büchi automata.
Cite as

Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven. Linear-Time Model Checking Branching Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2021.6,
  author =	{Kiefer, Stefan and Semukhin, Pavel and Widdershoven, Cas},
  title =	{{Linear-Time Model Checking Branching Processes}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.6},
  URN =		{urn:nbn:de:0030-drops-143834},
  doi =		{10.4230/LIPIcs.CONCUR.2021.6},
  annote =	{Keywords: model checking, Markov chains, branching processes, automata, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.22
Decidability of Cutpoint Isolation for Probabilistic Finite Automata on Letter-Bounded Inputs

Authors: Paul C. Bell and Pavel Semukhin

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

Abstract
We show the surprising result that the cutpoint isolation problem is decidable for probabilistic finite automata where input words are taken from a letter-bounded context-free language. A context-free language ℒ is letter-bounded when ℒ ⊆ a₁^* a₂^* ⋯ a_𝓁^* for some finite 𝓁 > 0 where each letter is distinct. A cutpoint is isolated when it cannot be approached arbitrarily closely. The decidability of this problem is in marked contrast to the situation for the (strict) emptiness problem for PFA which is undecidable under the even more severe restrictions of PFA with polynomial ambiguity, commutative matrices and input over a letter-bounded language as well as to the injectivity problem which is undecidable for PFA over letter-bounded languages. We provide a constructive nondeterministic algorithm to solve the cutpoint isolation problem, which holds even when the PFA is exponentially ambiguous. We also show that the problem is at least NP-hard and use our decision procedure to solve several related problems.
Cite as

Paul C. Bell and Pavel Semukhin. Decidability of Cutpoint Isolation for Probabilistic Finite Automata on Letter-Bounded Inputs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bell_et_al:LIPIcs.CONCUR.2020.22,
  author =	{Bell, Paul C. and Semukhin, Pavel},
  title =	{{Decidability of Cutpoint Isolation for Probabilistic Finite Automata on Letter-Bounded Inputs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{22:1--22:16},
  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.22},
  URN =		{urn:nbn:de:0030-drops-128344},
  doi =		{10.4230/LIPIcs.CONCUR.2020.22},
  annote =	{Keywords: Probabilistic finite automata, cutpoint isolation problem, letter-bounded context-free languages}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.83
On the Mortality Problem: From Multiplicative Matrix Equations to Linear Recurrence Sequences and Beyond

Authors: Paul C. Bell, Igor Potapov, and Pavel Semukhin

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We consider the following variant of the Mortality Problem: given k x k matrices A_1, A_2, ...,A_{t}, does there exist nonnegative integers m_1, m_2, ...,m_t such that the product A_1^{m_1} A_2^{m_2} * ... * A_{t}^{m_{t}} is equal to the zero matrix? It is known that this problem is decidable when t <= 2 for matrices over algebraic numbers but becomes undecidable for sufficiently large t and k even for integral matrices. In this paper, we prove the first decidability results for t>2. We show as one of our central results that for t=3 this problem in any dimension is Turing equivalent to the well-known Skolem problem for linear recurrence sequences. Our proof relies on the Primary Decomposition Theorem for matrices that was not used to show decidability results in matrix semigroups before. As a corollary we obtain that the above problem is decidable for t=3 and k <= 3 for matrices over algebraic numbers and for t=3 and k=4 for matrices over real algebraic numbers. Another consequence is that the set of triples (m_1,m_2,m_3) for which the equation A_1^{m_1} A_2^{m_2} A_3^{m_3} equals the zero matrix is equal to a finite union of direct products of semilinear sets. For t=4 we show that the solution set can be non-semilinear, and thus it seems unlikely that there is a direct connection to the Skolem problem. However we prove that the problem is still decidable for upper-triangular 2 x 2 rational matrices by employing powerful tools from transcendence theory such as Baker’s theorem and S-unit equations.
Cite as

Paul C. Bell, Igor Potapov, and Pavel Semukhin. On the Mortality Problem: From Multiplicative Matrix Equations to Linear Recurrence Sequences and Beyond. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 83:1-83:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bell_et_al:LIPIcs.MFCS.2019.83,
  author =	{Bell, Paul C. and Potapov, Igor and Semukhin, Pavel},
  title =	{{On the Mortality Problem: From Multiplicative Matrix Equations to Linear Recurrence Sequences and Beyond}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{83:1--83:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.83},
  URN =		{urn:nbn:de:0030-drops-110279},
  doi =		{10.4230/LIPIcs.MFCS.2019.83},
  annote =	{Keywords: Linear recurrence sequences, Skolem’s problem, mortality problem, matrix equations, primary decomposition theorem, Baker’s theorem}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.44
On Reachability Problems for Low-Dimensional Matrix Semigroups

Authors: Thomas Colcombet, Joël Ouaknine, Pavel Semukhin, and James Worrell

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We consider the Membership and the Half-Space Reachability problems for matrices in dimensions two and three. Our first main result is that the Membership Problem is decidable for finitely generated sub-semigroups of the Heisenberg group over rational numbers. Furthermore, we prove two decidability results for the Half-Space Reachability Problem. Namely, we show that this problem is decidable for sub-semigroups of GL(2,Z) and of the Heisenberg group over rational numbers.
Cite as

Thomas Colcombet, Joël Ouaknine, Pavel Semukhin, and James Worrell. On Reachability Problems for Low-Dimensional Matrix Semigroups. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 44:1-44:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2019.44,
  author =	{Colcombet, Thomas and Ouaknine, Jo\"{e}l and Semukhin, Pavel and Worrell, James},
  title =	{{On Reachability Problems for Low-Dimensional Matrix Semigroups}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{44:1--44:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.44},
  URN =		{urn:nbn:de:0030-drops-106209},
  doi =		{10.4230/LIPIcs.ICALP.2019.44},
  annote =	{Keywords: membership problem, half-space reachability problem, matrix semigroups, Heisenberg group, general linear group}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.44
Membership Problem in GL(2, Z) Extended by Singular Matrices

Authors: Igor Potapov and Pavel Semukhin

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We consider the membership problem for matrix semigroups, which is the problem to decide whether a matrix belongs to a given finitely generated matrix semigroup. In general, the decidability and complexity of this problem for two-dimensional matrix semigroups remains open. Recently there was a significant progress with this open problem by showing that the membership is decidable for 2x2 nonsingular integer matrices. In this paper we focus on the membership for singular integer matrices and prove that this problem is decidable for 2x2 integer matrices whose determinants are equal to 0, 1, -1 (i.e. for matrices from GL(2,Z) and any singular matrices). Our algorithm relies on a translation of numerical problems on matrices into combinatorial problems on words and conversion of the membership problem into decision problem on regular languages.
Cite as

Igor Potapov and Pavel Semukhin. Membership Problem in GL(2, Z) Extended by Singular Matrices. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 44:1-44:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{potapov_et_al:LIPIcs.MFCS.2017.44,
  author =	{Potapov, Igor and Semukhin, Pavel},
  title =	{{Membership Problem in GL(2, Z) Extended by Singular Matrices}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{44:1--44:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.44},
  URN =		{urn:nbn:de:0030-drops-80737},
  doi =		{10.4230/LIPIcs.MFCS.2017.44},
  annote =	{Keywords: Matrix Semigroups, Membership Problem, General Linear Group, Singular Matrices, Automata and Formal Languages}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.84
Vector Reachability Problem in SL(2, Z)

Authors: Igor Potapov and Pavel Semukhin

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

Abstract
The decision problems on matrices were intensively studied for many decades as matrix products play an essential role in the representation of various computational processes. However, many computational problems for matrix semigroups are inherently difficult to solve even for problems in low dimensions and most matrix semigroup problems become undecidable in general starting from dimension three or four. This paper solves two open problems about the decidability of the vector reachability problem over a finitely generated semigroup of matrices from SL(2, Z) and the point to point reachability (over rational numbers) for fractional linear transformations, where associated matrices are from SL(2, Z). The approach to solving reachability problems is based on the characterization of reachability paths between points which is followed by the translation of numerical problems on matrices into computational and combinatorial problems on words and formal languages. We also give a geometric interpretation of reachability paths and extend the decidability results to matrix products represented by arbitrary labelled directed graphs. Finally, we will use this technique to prove that a special case of the scalar reachability problem is decidable.
Cite as

Igor Potapov and Pavel Semukhin. Vector Reachability Problem in SL(2, Z). In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 84:1-84:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{potapov_et_al:LIPIcs.MFCS.2016.84,
  author =	{Potapov, Igor and Semukhin, Pavel},
  title =	{{Vector Reachability Problem in SL(2, Z)}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{84:1--84:14},
  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.84},
  URN =		{urn:nbn:de:0030-drops-64925},
  doi =		{10.4230/LIPIcs.MFCS.2016.84},
  annote =	{Keywords: matrix semigroup, vector reachability problem, special linear group, linear fractional transformation, automata and formal languages}
}
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 About DROPS Imprint Privacy Contact