Search Results

Documents authored by Michaliszyn, Jakub

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.3
Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix

Authors: Jakub Michaliszyn, Jan Otop, and Piotr Wieczorek

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

Abstract
We study constraint automata, which are finite-state automata over infinite alphabets consisting of tuples of words. A constraint automaton can compare the words of the consecutive tuples using Boolean combinations of the relations prefix, suffix, infix and equality. First, we show that the reachability problem of such automata is PSpace-complete. Second, we study automata over infinite sequences with Büchi conditions. We show that the problem: given a constraint automaton, is there a bound B and a sequence of tuples of words of length bounded by B, which is accepted by the automaton, is also PSpace-complete. These results contribute towards solving the long-standing open problem of the decidability of the emptiness problem for constraint automata, in which the words can have arbitrary lengths.
Cite as

Jakub Michaliszyn, Jan Otop, and Piotr Wieczorek. Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.CONCUR.2023.3,
  author =	{Michaliszyn, Jakub and Otop, Jan and Wieczorek, Piotr},
  title =	{{Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{3:1--3:16},
  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.3},
  URN =		{urn:nbn:de:0030-drops-189971},
  doi =		{10.4230/LIPIcs.CONCUR.2023.3},
  annote =	{Keywords: constraint automata, emptiness problem}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.74
Learning Deterministic Visibly Pushdown Automata Under Accessible Stack

Authors: Jakub Michaliszyn and Jan Otop

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We study the problem of active learning deterministic visibly pushdown automata. We show that in the classical L^*-setting, efficient active learning algorithms are not possible. To overcome this difficulty, we propose the accessible stack setting, where the algorithm has the read and write access to the stack. In this setting, we show that active learning can be done in polynomial time in the size of the target automaton and the counterexamples provided by the teacher. As counterexamples of exponential size are inevitable, we consider an algorithm working with words in a compressed representation via (visibly) Straight-Line Programs. Employing compression allows us to obtain an algorithm where the teacher and the learner work in time polynomial in the size of the target automaton alone.
Cite as

Jakub Michaliszyn and Jan Otop. Learning Deterministic Visibly Pushdown Automata Under Accessible Stack. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 74:1-74:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.MFCS.2022.74,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Learning Deterministic Visibly Pushdown Automata Under Accessible Stack}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{74:1--74:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.74},
  URN =		{urn:nbn:de:0030-drops-168729},
  doi =		{10.4230/LIPIcs.MFCS.2022.74},
  annote =	{Keywords: visibly pushdown automata, automata inference, minimization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.17
Approximate Learning of Limit-Average Automata

Authors: Jakub Michaliszyn and Jan Otop

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Limit-average automata are weighted automata on infinite words that use average to aggregate the weights seen in infinite runs. We study approximate learning problems for limit-average automata in two settings: passive and active. In the passive learning case, we show that limit-average automata are not PAC-learnable as samples must be of exponential-size to provide (with good probability) enough details to learn an automaton. We also show that the problem of finding an automaton that fits a given sample is NP-complete. In the active learning case, we show that limit-average automata can be learned almost-exactly, i.e., we can learn in polynomial time an automaton that is consistent with the target automaton on almost all words. On the other hand, we show that the problem of learning an automaton that approximates the target automaton (with perhaps fewer states) is NP-complete. The abovementioned results are shown for the uniform distribution on words. We briefly discuss learning over different distributions.
Cite as

Jakub Michaliszyn and Jan Otop. Approximate Learning of Limit-Average Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.CONCUR.2019.17,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Approximate Learning of Limit-Average Automata}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.17},
  URN =		{urn:nbn:de:0030-drops-109198},
  doi =		{10.4230/LIPIcs.CONCUR.2019.17},
  annote =	{Keywords: weighted automata, learning, expected value}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.10
Non-deterministic Weighted Automata on Random Words

Authors: Jakub Michaliszyn and Jan Otop

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables. The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose an approximation algorithm for the probabilistic questions, which works in exponential time in the automaton and polynomial time in the Markov chain. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.
Cite as

Jakub Michaliszyn and Jan Otop. Non-deterministic Weighted Automata on Random Words. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.CONCUR.2018.10,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Non-deterministic Weighted Automata on Random Words}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.10},
  URN =		{urn:nbn:de:0030-drops-95481},
  doi =		{10.4230/LIPIcs.CONCUR.2018.10},
  annote =	{Keywords: quantitative verification, weighted automata, expected value}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.42
Average Stack Cost of Büchi Pushdown Automata

Authors: Jakub Michaliszyn and Jan Otop

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
We study the average stack cost of Buechi pushdown automata (Buechi PDA). We associate a non-negative price with each stack symbol and define the cost of a stack as the sum of costs of all its elements. We introduce and study the average stack cost problem (ASC), which asks whether there exists an accepting run of a given Buechi PDA such that the long-run average of stack costs is below some given threshold. The ASC problem generalises mean-payoff objective and can be use to express quantitative properties of pushdown systems. In particular, we can compute the average response time using the ASC problem. We show that the ASC problem can be solved in polynomial time.
Cite as

Jakub Michaliszyn and Jan Otop. Average Stack Cost of Büchi Pushdown Automata. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 42:1-42:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.FSTTCS.2017.42,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Average Stack Cost of B\"{u}chi Pushdown Automata}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{42:1--42:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.42},
  URN =		{urn:nbn:de:0030-drops-83971},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.42},
  annote =	{Keywords: pushdown automata, average stack cost, weighted pushdown systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.43
Querying Best Paths in Graph Databases

Authors: Jakub Michaliszyn, Jan Otop, and Piotr Wieczorek

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
Querying graph databases has recently received much attention. We propose a new approach to this problem, which balances competing goals of expressive power, language clarity and computational complexity. A distinctive feature of our approach is the ability to express properties of minimal (e.g. shortest) and maximal (e.g. most valuable) paths satisfying given criteria. To express complex properties in a modular way, we introduce labelling-generating ontologies. The resulting formalism is computationally attractive - queries can be answered in non-deterministic logarithmic space in the size of the database.
Cite as

Jakub Michaliszyn, Jan Otop, and Piotr Wieczorek. Querying Best Paths in Graph Databases. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 43:1-43:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.FSTTCS.2017.43,
  author =	{Michaliszyn, Jakub and Otop, Jan and Wieczorek, Piotr},
  title =	{{Querying Best Paths in Graph Databases}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{43:1--43:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.43},
  URN =		{urn:nbn:de:0030-drops-83989},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.43},
  annote =	{Keywords: graph databases, queries, aggregation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.563
Elementary Modal Logics over Transitive Structures

Authors: Jakub Michaliszyn and Jan Otop

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NExpTime.
Cite as

Jakub Michaliszyn and Jan Otop. Elementary Modal Logics over Transitive Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 563-577, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.CSL.2013.563,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Elementary Modal Logics over Transitive Structures}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{563--577},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.563},
  URN =		{urn:nbn:de:0030-drops-42195},
  doi =		{10.4230/LIPIcs.CSL.2013.563},
  annote =	{Keywords: Modal logic, Transitive frames, Elementary modal logics, Decidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.396
Two-Variable Universal Logic with Transitive Closure

Authors: Emanuel Kieronski and Jakub Michaliszyn

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We prove that the satisfiability problem for the two-variable, universal fragment of first-order logic with constants (or, alternatively phrased, for the Bernays-Schönfinkel class with two universally quantified variables) remains decidable after augmenting the fragment by the transitive closure of a single binary relation. We give a 2-NExpTime-upper bound and a 2-ExpTime-lower bound for the complexity of the problem. We also study the cases in which the number of constants is restricted. It appears that with two constants the considered fragment has the finite model property and NExpTime-complete satisfiability problem. Adding a third constant does not change the complexity but allows to construct infinity axioms. A fourth constant lifts the lower complexity bound to TwoExpTime. Finally, we observe that we are close to the border between decidability and undecidability: adding a third variable or the transitive closure of a second binary relation lead to undecidability.
Cite as

Emanuel Kieronski and Jakub Michaliszyn. Two-Variable Universal Logic with Transitive Closure. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 396-410, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kieronski_et_al:LIPIcs.CSL.2012.396,
  author =	{Kieronski, Emanuel and Michaliszyn, Jakub},
  title =	{{Two-Variable Universal Logic with Transitive Closure}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{396--410},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.396},
  URN =		{urn:nbn:de:0030-drops-36860},
  doi =		{10.4230/LIPIcs.CSL.2012.396},
  annote =	{Keywords: two-variable logic, transitive closure, decidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.264
Modal Logics Definable by Universal Three-Variable Formulas

Authors: Emanuel Kieronski, Jakub Michaliszyn, and Jan Otop

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

Abstract
We consider the satisfiability problem for modal logic over classes of structures definable by universal first-order formulas with three variables. We exhibit a simple formula for which the problem is undecidable. This improves an earlier result in which nine variables were used. We also show that for classes defined by three-variable, universal Horn formulas the problem is decidable. This subsumes decidability results for many natural modal logics, including T, B, K4, S4, S5.
Cite as

Emanuel Kieronski, Jakub Michaliszyn, and Jan Otop. Modal Logics Definable by Universal Three-Variable Formulas. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 264-275, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kieronski_et_al:LIPIcs.FSTTCS.2011.264,
  author =	{Kieronski, Emanuel and Michaliszyn, Jakub and Otop, Jan},
  title =	{{Modal Logics Definable by Universal Three-Variable Formulas}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{264--275},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.264},
  URN =		{urn:nbn:de:0030-drops-33495},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.264},
  annote =	{Keywords: modal logic, decidability}
}
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