9 Search Results for "�tefaň�k, Filip"

Document
DOI: 10.4230/DagRep.13.10.24
Accountable Software Systems (Dagstuhl Seminar 23411)

Authors: Bettina Könighofer, Joshua A. Kroll, Ruzica Piskac, Michael Veale, and Filip Cano Córdoba

Published in: Dagstuhl Reports, Volume 13, Issue 10 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23411 "Accountable Software Systems". The seminar brought together an interdisciplinary group of researchers from the fields of formal methods, machine learning, philosophy, political science, law, and policy studies to address the critical issue of accountability in the development and deployment of software systems. As these systems increasingly assume roles within safety-critical domains of society, including transportation, healthcare, recruitment, and the judiciary, the seminar aimed to explore the multifaceted concept of accountability, its significance, and its implementation challenges in this context. During the seminar, experts engaged deeply in discussions, presentations, and collaborative sessions, focusing on key themes such as the application of formal tools in socio-technical accountability, the impact of computing infrastructures on software accountability, and the innovation of formal languages and models to improve accountability measures. This interdisciplinary dialogue underscored the complexities involved in defining and operationalizing accountability, especially in light of technological advancements and their societal implications. The participants of the seminar reached a consensus on the pressing need for ongoing research and cross-disciplinary efforts to develop effective accountability mechanisms, highlighting the critical role of integrating socio-technical approaches and formal methodologies to enhance the accountability of autonomous systems and their contributions to society.
Cite as

Bettina Könighofer, Joshua A. Kroll, Ruzica Piskac, Michael Veale, and Filip Cano Córdoba. Accountable Software Systems (Dagstuhl Seminar 23411). In Dagstuhl Reports, Volume 13, Issue 10, pp. 24-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{konighofer_et_al:DagRep.13.10.24,
  author =	{K\"{o}nighofer, Bettina and Kroll, Joshua A. and Piskac, Ruzica and Veale, Michael and C\'{o}rdoba, Filip Cano},
  title =	{{Accountable Software Systems (Dagstuhl Seminar 23411)}},
  pages =	{24--49},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{10},
  editor =	{K\"{o}nighofer, Bettina and Kroll, Joshua A. and Piskac, Ruzica and Veale, Michael and C\'{o}rdoba, Filip Cano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.24},
  URN =		{urn:nbn:de:0030-drops-198328},
  doi =		{10.4230/DagRep.13.10.24},
  annote =	{Keywords: accountability, Responsible Decision Making, Societal Impact of AI}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2024.22
Evaluating Graph Queries Using Semantic Treewidth

Authors: Cristina Feier, Tomasz Gogacz, and Filip Murlak

Published in: LIPIcs, Volume 290, 27th International Conference on Database Theory (ICDT 2024)

Abstract
Unions of conjunctive two-way regular path queries (UC2RPQs) are a common abstraction of query languages for graph databases, much like unions of conjunctive queries (UCQs) in the relational case. As in the case of UCQs, their evaluation is NP-complete in combined complexity. Semantic tree-width, i.e. the minimal treewidth of equivalent queries, has been proposed as a candidate criterion to characterize fixed-parameter tractability of UC2RPQs. It was recently shown how to decide the semantic tree-width of a UC2RPQ, by constructing the best under-approximation of a given treewidth, in the form of a UC2RPQ of size doubly exponential in the size of the original query. This leads to an fpt algorithm for evaluating UC2RPQs of semantic TW k which runs in time doubly exponential in the size of the parameter, i.e. in the UC2RPQ. Here we describe a more efficient fpt algorithm for evaluating UC2RPQs of semantic treewidth k which runs in time singly exponential in the size of the parameter. We do this by a careful construction of a witness query which, while still being doubly exponential, can be represented as a Datalog program of bounded width and singly exponential size.
Cite as

Cristina Feier, Tomasz Gogacz, and Filip Murlak. Evaluating Graph Queries Using Semantic Treewidth. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{feier_et_al:LIPIcs.ICDT.2024.22,
  author =	{Feier, Cristina and Gogacz, Tomasz and Murlak, Filip},
  title =	{{Evaluating Graph Queries Using Semantic Treewidth}},
  booktitle =	{27th International Conference on Database Theory (ICDT 2024)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-312-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{290},
  editor =	{Cormode, Graham and Shekelyan, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.22},
  URN =		{urn:nbn:de:0030-drops-198048},
  doi =		{10.4230/LIPIcs.ICDT.2024.22},
  annote =	{Keywords: conjunctive two-way regular path queries, fixed-parameter tractable evaluation, semantic treewidth, Datalog encoding, optimization}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.131
Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality

Authors: Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Węgrzycki

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff’s bounding technique to show that if coverability holds then there is a run of length at most n^{2^𝒪(d log d)}, where d is the dimension and n is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in d-dimensional unary VASS that are only witnessed by runs of length at least n^{2^Ω(d)}. Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated log(d) factor, thus matching Lipton’s lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic n^{2^𝒪(d)}-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic n^{2^o(d)}-time algorithm, conditioned upon the Exponential Time Hypothesis. When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in 𝒪(n^{d+1})-time. We give evidence to this being near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that n^{2-o(1)}-time is required under the k-cycle hypothesis. In general fixed dimension d, we show that n^{d-2-o(1)}-time is required under the 3-uniform hyperclique hypothesis.
Cite as

Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Węgrzycki. Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 131:1-131:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kunnemann_et_al:LIPIcs.ICALP.2023.131,
  author =	{K\"{u}nnemann, Marvin and Mazowiecki, Filip and Sch\"{u}tze, Lia and Sinclair-Banks, Henry and W\k{e}grzycki, Karol},
  title =	{{Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{131:1--131:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.131},
  URN =		{urn:nbn:de:0030-drops-181834},
  doi =		{10.4230/LIPIcs.ICALP.2023.131},
  annote =	{Keywords: Vector Addition System, Coverability, Reachability, Fine-Grained Complexity, Exponential Time Hypothesis, k-Cycle Hypothesis, Hyperclique Hypothesis}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.24
On Rational Recursive Sequences

Authors: Lorenzo Clemente, Maria Donten-Bury, Filip Mazowiecki, and Michał Pilipczuk

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
We study the class of rational recursive sequences (ratrec) over the rational numbers. A ratrec sequence is defined via a system of sequences using mutually recursive equations of depth 1, where the next values are computed as rational functions of the previous values. An alternative class is that of simple ratrec sequences, where one uses a single recursive equation, however of depth k: the next value is defined as a rational function of k previous values. We conjecture that the classes ratrec and simple ratrec coincide. The main contribution of this paper is a proof of a variant of this conjecture where the initial conditions are treated symbolically, using a formal variable per sequence, while the sequences themselves consist of rational functions over those variables. While the initial conjecture does not follow from this variant, we hope that the introduced algebraic techniques may eventually be helpful in resolving the problem. The class ratrec strictly generalises a well-known class of polynomial recursive sequences (polyrec). These are defined like ratrec, but using polynomial functions instead of rational ones. One can observe that if our conjecture is true and effective, then we can improve the complexities of the zeroness and the equivalence problems for polyrec sequences. Currently, the only known upper bound is Ackermanian, which follows from results on polynomial automata. We complement this observation by proving a PSPACE lower bound for both problems for polyrec. Our lower bound construction also implies that the Skolem problem is PSPACE-hard for the polyrec class.
Cite as

Lorenzo Clemente, Maria Donten-Bury, Filip Mazowiecki, and Michał Pilipczuk. On Rational Recursive Sequences. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.STACS.2023.24,
  author =	{Clemente, Lorenzo and Donten-Bury, Maria and Mazowiecki, Filip and Pilipczuk, Micha{\l}},
  title =	{{On Rational Recursive Sequences}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{24:1--24:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.24},
  URN =		{urn:nbn:de:0030-drops-176763},
  doi =		{10.4230/LIPIcs.STACS.2023.24},
  annote =	{Keywords: recursive sequences, polynomial automata, zeroness problem, equivalence problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.16
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
DOI: 10.4230/LIPIcs.SAT.2022.15
Weighted Model Counting with Twin-Width

Authors: Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this paper, we investigate the use of twin-width for solving the propositional satisfiability problem (SAT) and propositional model counting. We particularly focus on Bounded-ones Weighted Model Counting (BWMC), which takes as input a CNF formula F along with a bound k and asks for the weighted sum of all models with at most k positive literals. BWMC generalizes not only SAT but also (weighted) model counting. We develop the notion of "signed" twin-width of CNF formulas and establish that BWMC is fixed-parameter tractable when parameterized by the certified signed twin-width of F plus k. We show that this result is tight: it is neither possible to drop the bound k nor use the vanilla twin-width instead if one wishes to retain fixed-parameter tractability, even for the easier problem SAT. Our theoretical results are complemented with an empirical evaluation and comparison of signed twin-width on various classes of CNF formulas.
Cite as

Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider. Weighted Model Counting with Twin-Width. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ganian_et_al:LIPIcs.SAT.2022.15,
  author =	{Ganian, Robert and Pokr\'{y}vka, Filip and Schidler, Andr\'{e} and Simonov, Kirill and Szeider, Stefan},
  title =	{{Weighted Model Counting with Twin-Width}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.15},
  URN =		{urn:nbn:de:0030-drops-166896},
  doi =		{10.4230/LIPIcs.SAT.2022.15},
  annote =	{Keywords: Weighted model counting, twin-width, parameterized complexity, SAT}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.FSTTCS.2018.1
Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper)

Authors: Rupak Majumdar

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Random testing has proven to be an effective way to catch bugs in concurrent and distributed systems. This is surprising, as the space of executions is enormous and conventional formal methods intuition would suggest that bad behaviors would only be found by extremely unlikely coincidences. Empirically, many bugs in distributed systems can be explained by interactions among only a small number of features. Thus, one can attempt to explain the effectiveness of random testing under various "small depth" hypotheses. In particular, it may be possible to test all interactions of k features for a small constant k by executing a family of tests that is exponentially or even doubly-exponentially smaller than the family of all tests. Moreover, under certain conditions, a randomly chosen small set of tests is sufficient to cover all k-wise interactions with high probability. I will describe two concrete scenarios. First, I will describe bugs in distributed systems caused by network partition faults. In many practical instances, these bugs occur due to two or three key nodes, such as leaders or replicas, not being able to communicate, or because the leading node finds itself in a block of the partition without quorum. In this case, I will show using the probabilistic method that a small set of randomly chosen tests will cover all "small partition" scenarios with high probability. Second, I will consider bugs that arise due to unexpected schedules (interleavings) of concurrent events. Again, many bugs depend only on the relative ordering of a small number of events (the "bug depth" of the bug). In this case, I will show a testing algorithm that prioritizes low depth interleavings and a randomized testing algorithm that bounds the probability of sampling any behavior of bug depth k for a fixed k. The testing algorithm is based on combinatorial insights from the theory of partial orders, such as the notion of dimension and its generalization to d-hitting families as well as results on online chain partitioning. Beyond the potential for designing or explaining random testing procedures, the technical arguments show the potential of combining "Theory A" and "Theory B" results to the important domain of software testing. This is joint work primarily with Filip Niksic [Filip Niksic, 2018], and with Dmitry Chistikov, Simin Oraee, Burcu Kulahcioglu Özkan, Mitra Tabaei Befrouei, and Georg Weissenbacher. This work was partially funded by an ERC Synergy Award (ImPACT).
Cite as

Rupak Majumdar. Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{majumdar:LIPIcs.FSTTCS.2018.1,
  author =	{Majumdar, Rupak},
  title =	{{Random Testing for Distributed Systems with Theoretical Guarantees}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.1},
  URN =		{urn:nbn:de:0030-drops-99000},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.1},
  annote =	{Keywords: Random testing, Hitting families}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2354
Space Effective Model Checking for Component-Interaction Automata

Authors: Nikola Beneš, Milan Křivánek, and Filip Štefaňák

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract
The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic. As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample set partial order reduction method within the component-interaction automata verification framework. Due to the state and action-based nature of both the modelling and specification formalisms, the implementation differs from traditional state-based approaches. After describing the implementation, we present some of the results obtained by employing the enhanced verification framework on a case study.
Cite as

Nikola Beneš, Milan Křivánek, and Filip Štefaňák. Space Effective Model Checking for Component-Interaction Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 80-87, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{benes_et_al:OASIcs:2009:DROPS.MEMICS.2009.2354,
  author =	{Bene\v{s}, Nikola and K\v{r}iv\'{a}nek, Milan and \v{S}tefa\v{n}\'{a}k, Filip},
  title =	{{Space Effective Model Checking for Component-Interaction Automata}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{80--87},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2354},
  URN =		{urn:nbn:de:0030-drops-23549},
  doi =		{10.4230/DROPS.MEMICS.2009.2354},
  annote =	{Keywords: Model checking, component-based systems, partial order reduction}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2312
The Wadge Hierarchy of Max-Regular Languages

Authors: Jérémie Cabessa, Jacques Duparc, Alessandro Facchini, and Filip Murlak

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

Abstract
Recently, Miko{\l}aj Boja{\'n}czyk introduced a class of max-regular languages, an extension of regular languages of infinite words preserving manyof its usual properties. This new class can be seen as a different way of generalising the notion of regularity from finite to infinite words. This paper compares regular and max-regular languages in terms of topological complexity.It is proved that up to Wadge equivalence the classes coincide. Moreover, when restricted to $\mathbf{\Delta}^0_2$-languages, the classes contain virtually the same languages. On the other hand, separating examples of arbitrary complexity exceeding $\mathbf{\Delta}^0_2$ are constructed.
Cite as

Jérémie Cabessa, Jacques Duparc, Alessandro Facchini, and Filip Murlak. The Wadge Hierarchy of Max-Regular Languages. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{cabessa_et_al:LIPIcs.FSTTCS.2009.2312,
  author =	{Cabessa, J\'{e}r\'{e}mie and Duparc, Jacques and Facchini, Alessandro and Murlak, Filip},
  title =	{{The Wadge Hierarchy of Max-Regular Languages}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{121--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2312},
  URN =		{urn:nbn:de:0030-drops-23122},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2312},
  annote =	{Keywords: Max-regular languages, Wadge hierarchy, Wagner hierarchy}
}
  • Refine by Author
  • 2 Mazowiecki, Filip
  • 2 Murlak, Filip
  • 1 Beneš, Nikola
  • 1 Cabessa, Jérémie
  • 1 Clemente, Lorenzo
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Law, social and behavioral sciences
  • 1 Information systems → Query languages
  • 1 Software and its engineering → Software testing and debugging
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Complexity theory and logic
  • Show More...

  • Refine by Keyword
  • 1 Coverability
  • 1 Datalog encoding
  • 1 Exponential Time Hypothesis
  • 1 Fine-Grained Complexity
  • 1 Hitting families
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2009
  • 2 2022
  • 2 2023
  • 2 2024
  • 1 2018

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