50 Search Results for "B�zivin, Jean"


Document
Extended Abstract
A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning (Extended Abstract)

Authors: Yakoub Salhi and Michael Sioutis

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)


Abstract
Dealing with inconsistency is a central problem in AI, due to the fact that inconsistency can arise for many reasons in real-world applications, such as context dependency, multi-source information, vagueness, noisy data, etc. Among the approaches that are involved in inconsistency handling, we can mention argumentation, non-monotonic reasoning, and paraconsistency, e.g., see [Philippe Besnard and Anthony Hunter, 2008; Gerhard Brewka et al., 1997; Koji Tanaka et al., 2013]. In the work of [Yakoub Salhi and Michael Sioutis, 2023], we are interested in dealing with inconsistency in the context of Qualitative Spatio-Temporal Reasoning (QSTR) [Ligozat, 2013]. QSTR is an AI framework that aims to mimic, natural, human-like representation and reasoning regarding space and time. This framework is applied to a variety of domains, such as qualitative case-based reasoning and learning [Thiago Pedro Donadon Homem et al., 2020] and visual sensemaking [Jakob Suchan et al., 2021]; the interested reader is referred to [Michael Sioutis and Diedrich Wolter, 2021] for a recent survey. Motivation. In [Yakoub Salhi and Michael Sioutis, 2023], we study the decomposition of an inconsistent constraint network into consistent subnetworks under, possible, mandatory constraints. To illustrate the interest of such a decomposition, we provide a simple example described in Figure 1. The QCN depicted in the top part of the figure corresponds to a description of an inconsistent plan. Further, we assume that the constraint Task A {before} Task B is mandatory. To handle inconsistency, this plan can be transformed into a decomposition of two consistent plans, depicted in the bottom part of the figure; this decomposition can be used, e.g., to capture the fact that Task C must be performed twice. More generally, network decomposition can be involved in inconsistency handling in several ways: it can be used to identify potential contexts that explain the presence of inconsistent information; it can also be used to restore consistency through a compromise between the components of a decomposition, e.g., by using belief merging [Jean-François Condotta et al., 2010]; in addition, QCN decomposition can be used as the basis for defining inconsistency measures. Contributions. We summarize the contributions of [Yakoub Salhi and Michael Sioutis, 2023] as follows. First, we propose a theoretical study of a problem that consists in decomposing an inconsistent QCN into a bounded number of consistent QCNs that may satisfy a specified part in the original QCN; intuitively, the required common part corresponds to the constraints that are considered necessary, if any. To this end, we provide upper bounds for the minimum number of components in a decomposition as well as computational complexity results. Secondly, we provide two methods for solving our decomposition problem. The first method corresponds to a greedy constraint-based algorithm, a variant of which involves the use of spanning trees; the basic idea of this variant is that any acyclic constraint graph in QSTR is consistent, and such a graph can be used as a starting point for building consistent components. The second method corresponds to a SAT-based encoding; every model of this encoding is used to construct a valid decomposition. Thirdly, we consider two optimization versions of the initial decomposition problem that focus on minimizing the number of components and maximizing the similarity between components, respectively. The similarity between two QCNs is quantified by the number of common non-universal constraints; the interest in maximizing the similarity lies mainly in the fact that it reduces the number of constraints that allow each component to be distinguished from the rest. Of course, our previous methods are adapted to tackle these optimization versions, too. Additionally, we introduce two inconsistency measures based on QCN decomposition, which can be seen as counterparts of measures for propositional KBs introduced in [Matthias Thimm, 2016; Meriem Ammoura et al., 2017], and show that they satisfy several desired properties in the literature. Finally, we provide implementations of our methods for computing decompositions and experimentally evaluate them using different metrics.

Cite as

Yakoub Salhi and Michael Sioutis. A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{salhi_et_al:LIPIcs.TIME.2023.16,
  author =	{Salhi, Yakoub and Sioutis, Michael},
  title =	{{A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{16:1--16:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.16},
  URN =		{urn:nbn:de:0030-drops-191062},
  doi =		{10.4230/LIPIcs.TIME.2023.16},
  annote =	{Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Inconsistency Handling, Decomposition, Inconsistency Measures}
}
Document
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-dev.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
Deciding What Is Good-For-MDPs

Authors: Sven Schewe, Qiyi Tang, and Tansholpan Zhanabekova

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


Abstract
Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof.

Cite as

Sven Schewe, Qiyi Tang, and Tansholpan Zhanabekova. Deciding What Is Good-For-MDPs. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{schewe_et_al:LIPIcs.CONCUR.2023.35,
  author =	{Schewe, Sven and Tang, Qiyi and Zhanabekova, Tansholpan},
  title =	{{Deciding What Is Good-For-MDPs}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{35:1--35: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.35},
  URN =		{urn:nbn:de:0030-drops-190290},
  doi =		{10.4230/LIPIcs.CONCUR.2023.35},
  annote =	{Keywords: B\"{u}chi automata, Markov Decision Processes, Omega-regular objectives, Reinforcement learning}
}
Document
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata

Authors: Yong Li, Sven Schewe, and Moshe Y. Vardi

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


Abstract
We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak automata (AVAs) - automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)ⁿ vs. (0.76n)ⁿ), while the input of our construction can be exponentially more succinct.

Cite as

Yong Li, Sven Schewe, and Moshe Y. Vardi. Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CONCUR.2023.37,
  author =	{Li, Yong and Schewe, Sven and Vardi, Moshe Y.},
  title =	{{Singly Exponential Translation of Alternating Weak B\"{u}chi Automata to Unambiguous B\"{u}chi Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{37:1--37: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.37},
  URN =		{urn:nbn:de:0030-drops-190313},
  doi =		{10.4230/LIPIcs.CONCUR.2023.37},
  annote =	{Keywords: B\"{u}chi automata, unambiguous automata, alternation, weak, disambiguation}
}
Document
On Extended Boundary Sequences of Morphic and Sturmian Words

Authors: Michel Rigo, Manon Stipulanti, and Markus A. Whiteland

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


Abstract
Generalizing the notion of the boundary sequence introduced by Chen and Wen, the nth term of the 𝓁-boundary sequence of an infinite word is the finite set of pairs (u,v) of prefixes and suffixes of length 𝓁 appearing in factors uyv of length n+𝓁 (n ≥ 𝓁 ≥ 1). Otherwise stated, for increasing values of n, one looks for all pairs of factors of length 𝓁 separated by n-𝓁 symbols. For the large class of addable numeration systems U, we show that if an infinite word is U-automatic, then the same holds for its 𝓁-boundary sequence. In particular, they are both morphic (or generated by an HD0L system). We also provide examples of numeration systems and U-automatic words with a boundary sequence that is not U-automatic. In the second part of the paper, we study the 𝓁-boundary sequence of a Sturmian word. We show that it is obtained through a sliding block code from the characteristic Sturmian word of the same slope. We also show that it is the image under a morphism of some other characteristic Sturmian word.

Cite as

Michel Rigo, Manon Stipulanti, and Markus A. Whiteland. On Extended Boundary Sequences of Morphic and Sturmian Words. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 79:1-79:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{rigo_et_al:LIPIcs.MFCS.2022.79,
  author =	{Rigo, Michel and Stipulanti, Manon and Whiteland, Markus A.},
  title =	{{On Extended Boundary Sequences of Morphic and Sturmian Words}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{79:1--79: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.79},
  URN =		{urn:nbn:de:0030-drops-168776},
  doi =		{10.4230/LIPIcs.MFCS.2022.79},
  annote =	{Keywords: Boundary sequences, Sturmian words, Numeration systems, Automata, Graph of addition}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Strategy Synthesis for Global Window PCTL

Authors: Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
Given a Markov decision process (MDP) M and a formula Φ, the strategy synthesis problem asks if there exists a strategy σ s.t. the resulting Markov chain M[σ] satisfies Φ. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.

Cite as

Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin. Strategy Synthesis for Global Window PCTL. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.ICALP.2022.115,
  author =	{Bordais, Benjamin and Busatto-Gaston, Damien and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Strategy Synthesis for Global Window PCTL}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.115},
  URN =		{urn:nbn:de:0030-drops-164562},
  doi =		{10.4230/LIPIcs.ICALP.2022.115},
  annote =	{Keywords: Markov decision processes, synthesis, PCTL}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
The Complexity of SPEs in Mean-Payoff Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
We establish that the subgame perfect equilibrium (SPE) threshold problem for mean-payoff games is NP-complete. While the SPE threshold problem was recently shown to be decidable (in doubly exponential time) and NP-hard, its exact worst case complexity was left open.

Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. The Complexity of SPEs in Mean-Payoff Games. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 116:1-116:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.ICALP.2022.116,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{The Complexity of SPEs in Mean-Payoff Games}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{116:1--116:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.116},
  URN =		{urn:nbn:de:0030-drops-164574},
  doi =		{10.4230/LIPIcs.ICALP.2022.116},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, mean-payoff objectives}
}
Document
Subquadratic Algorithms for Some 3Sum-Hard Geometric Problems in the Algebraic Decision Tree Model

Authors: Boris Aronov, Mark de Berg, Jean Cardinal, Esther Ezra, John Iacono, and Micha Sharir

Published in: LIPIcs, Volume 212, 32nd International Symposium on Algorithms and Computation (ISAAC 2021)


Abstract
We present subquadratic algorithms in the algebraic decision-tree model for several 3Sum-hard geometric problems, all of which can be reduced to the following question: Given two sets A, B, each consisting of n pairwise disjoint segments in the plane, and a set C of n triangles in the plane, we want to count, for each triangle Δ ∈ C, the number of intersection points between the segments of A and those of B that lie in Δ. The problems considered in this paper have been studied by Chan (2020), who gave algorithms that solve them, in the standard real-RAM model, in O((n²/log²n) log^O(1) log n) time. We present solutions in the algebraic decision-tree model whose cost is O(n^{60/31+ε}), for any ε > 0. Our approach is based on a primal-dual range searching mechanism, which exploits the multi-level polynomial partitioning machinery recently developed by Agarwal, Aronov, Ezra, and Zahl (2020). A key step in the procedure is a variant of point location in arrangements, say of lines in the plane, which is based solely on the order type of the lines, a "handicap" that turns out to be beneficial for speeding up our algorithm.

Cite as

Boris Aronov, Mark de Berg, Jean Cardinal, Esther Ezra, John Iacono, and Micha Sharir. Subquadratic Algorithms for Some 3Sum-Hard Geometric Problems in the Algebraic Decision Tree Model. In 32nd International Symposium on Algorithms and Computation (ISAAC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 212, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{aronov_et_al:LIPIcs.ISAAC.2021.3,
  author =	{Aronov, Boris and de Berg, Mark and Cardinal, Jean and Ezra, Esther and Iacono, John and Sharir, Micha},
  title =	{{Subquadratic Algorithms for Some 3Sum-Hard Geometric Problems in the Algebraic Decision Tree Model}},
  booktitle =	{32nd International Symposium on Algorithms and Computation (ISAAC 2021)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-214-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{212},
  editor =	{Ahn, Hee-Kap and Sadakane, Kunihiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2021.3},
  URN =		{urn:nbn:de:0030-drops-154363},
  doi =		{10.4230/LIPIcs.ISAAC.2021.3},
  annote =	{Keywords: Computational geometry, Algebraic decision-tree model, Polynomial partitioning, Primal-dual range searching, Order types, Point location, Hierarchical partitions}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Dynamic Membership for Regular Languages

Authors: Antoine Amarilli, Louis Jachiet, and Charles Paperman

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
We study the dynamic membership problem for regular languages: fix a language L, read a word w, build in time O(|w|) a data structure indicating if w is in L, and maintain this structure efficiently under letter substitutions on w. We consider this problem on the unit cost RAM model with logarithmic word length, where the problem always has a solution in O(log|w| / log log|w|) per operation. We show that the problem is in O(log log|w|) for languages in an algebraically-defined, decidable class QSG, and that it is in O(1) for another such class QLZG. We show that languages not in QSG admit a reduction from the prefix problem for a cyclic group, so that they require Ω(log|w| /log log|w|) operations in the worst case; and that QSG languages not in QLZG admit a reduction from the prefix problem for the multiplicative monoid U₁ = {0, 1}, which we conjecture cannot be maintained in O(1). This yields a conditional trichotomy. We also investigate intermediate cases between O(1) and O(log log|w|). Our results are shown via the dynamic word problem for monoids and semigroups, for which we also give a classification. We thus solve open problems of the paper of Skovbjerg Frandsen, Miltersen, and Skyum [Skovbjerg Frandsen et al., 1997] on the dynamic word problem, and additionally cover regular languages.

Cite as

Antoine Amarilli, Louis Jachiet, and Charles Paperman. Dynamic Membership for Regular Languages. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 116:1-116:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.ICALP.2021.116,
  author =	{Amarilli, Antoine and Jachiet, Louis and Paperman, Charles},
  title =	{{Dynamic Membership for Regular Languages}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{116:1--116:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.116},
  URN =		{urn:nbn:de:0030-drops-141850},
  doi =		{10.4230/LIPIcs.ICALP.2021.116},
  annote =	{Keywords: regular language, membership, RAM model, updates, dynamic}
}
Document
Invited Talk
μ-Calculi with Atoms (Invited Talk)

Authors: Bartek Klin

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
Modal μ-calculus is a well-known formalism for describing properties of state-based transition systems. It can define properties such as "[in the current state] p holds, and there is a path where is holds again at some point in the future", where p comes from some fixed vocabulary of basic predicates. A formula of the classical μ-calculus refers only to finitely many basic predicates, which may sometimes seem restrictive. Real systems routinely operate on data coming from potentially infinite domains, such as numbers or character strings. Basic properties of such systems may reasonably include ones like "the number n was input", for every number n. It is then not clear how to say that "there exists a transition path where the currently input number is input again some time in the future" as a formula. Various modal formalisms have been proposed to model temporal properties of systems that refer to data coming from infinite domains. Here I focus on the modal μ-calculus with atoms, which is an extension of the classical calculus with features of nominal sets. There, basic predicates, formulas and models rely on atoms that come from some fixed infinite domain and can be tested for equality (or, in an extended variant, for some fixed order). I present a few variants of the modal μ-calculus with atoms, and describe their properties. As an example application, I show how to formulate the security property of the cryptographic Needham-Schroeder protocol, which relies on generating atomic nonces and comparing them for equality, and which famously fails due to a man-in-the-middle attack. Much of the material presented in this talk is drawn from [C. Eberhart and B. Klin, 2019; B. Klin and M. Łełyk, 2019; B. Klin and M. Łełyk, 2017].

Cite as

Bartek Klin. μ-Calculi with Atoms (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{klin:LIPIcs.CSL.2021.1,
  author =	{Klin, Bartek},
  title =	{{\mu-Calculi with Atoms}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.1},
  URN =		{urn:nbn:de:0030-drops-134358},
  doi =		{10.4230/LIPIcs.CSL.2021.1},
  annote =	{Keywords: modal \mu-calculus, sets with atoms}
}
Document
A Deep Quantitative Type System

Authors: Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the "collection calculus", as a Curry-Howard interpretation of the type system, that embodies these computational properties.

Cite as

Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus. A Deep Quantitative Type System. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.24,
  author =	{Guerrieri, Giulio and Heijltjes, Willem B. and Paulus, Joseph W.N.},
  title =	{{A Deep Quantitative Type System}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.24},
  URN =		{urn:nbn:de:0030-drops-134586},
  doi =		{10.4230/LIPIcs.CSL.2021.24},
  annote =	{Keywords: Lambda-calculus, Deep inference, Intersection types, Resource calculus}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
The Adversarial Stackelberg Value in Quantitative Games

Authors: Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
In this paper, we study the notion of adversarial Stackelberg value for two-player non-zero sum games played on bi-weighted graphs with the mean-payoff and the discounted sum functions. The adversarial Stackelberg value of Player 0 is the largest value that Player 0 can obtain when announcing her strategy to Player 1 which in turn responds with any of his best response. For the mean-payoff function, we show that the adversarial Stackelberg value is not always achievable but ε-optimal strategies exist. We show how to compute this value and prove that the associated threshold problem is in NP. For the discounted sum payoff function, we draw a link with the target discounted sum problem which explains why the problem is difficult to solve for this payoff function. We also provide solutions to related gap problems.

Cite as

Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Adversarial Stackelberg Value in Quantitative Games. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 127:1-127:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2020.127,
  author =	{Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Fran\c{c}ois},
  title =	{{The Adversarial Stackelberg Value in Quantitative Games}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{127:1--127:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.127},
  URN =		{urn:nbn:de:0030-drops-125348},
  doi =		{10.4230/LIPIcs.ICALP.2020.127},
  annote =	{Keywords: Non-zero sum games, reactive synthesis, adversarial Stackelberg}
}
Document
Testing Polynomials for Vanishing on Cartesian Products of Planar Point Sets

Authors: Boris Aronov, Esther Ezra, and Micha Sharir

Published in: LIPIcs, Volume 164, 36th International Symposium on Computational Geometry (SoCG 2020)


Abstract
We present subquadratic algorithms, in the algebraic decision-tree model of computation, for detecting whether there exists a triple of points, belonging to three respective sets A, B, and C of points in the plane, that satisfy a certain polynomial equation or two equations. The best known instance of such a problem is testing for the existence of a collinear triple of points in A×B×C, a classical 3SUM-hard problem that has so far defied any attempt to obtain a subquadratic solution, whether in the (uniform) real RAM model, or in the algebraic decision-tree model. While we are still unable to solve this problem, in full generality, in subquadratic time, we obtain such a solution, in the algebraic decision-tree model, that uses only roughly O(n^(28/15)) constant-degree polynomial sign tests, for the special case where two of the sets lie on one-dimensional curves and the third is placed arbitrarily in the plane. Our technique is fairly general, and applies to any other problem where we seek a triple that satisfies a single polynomial equation, e.g., determining whether A× B× C contains a triple spanning a unit-area triangle. This result extends recent work by Barba et al. [Luis Barba et al., 2019] and by Chan [Timothy M. Chan, 2020], where all three sets A, B, and C are assumed to be one-dimensional. While there are common features in the high-level approaches, here and in [Luis Barba et al., 2019], the actual analysis in this work becomes more involved and requires new methods and techniques, involving polynomial partitions and other related tools. As a second application of our technique, we again have three n-point sets A, B, and C in the plane, and we want to determine whether there exists a triple (a,b,c) ∈ A×B×C that simultaneously satisfies two real polynomial equations. For example, this is the setup when testing for the existence of pairs of similar triangles spanned by the input points, in various contexts discussed later in the paper. We show that problems of this kind can be solved with roughly O(n^(24/13)) constant-degree polynomial sign tests. These problems can be extended to higher dimensions in various ways, and we present subquadratic solutions to some of these extensions, in the algebraic decision-tree model.

Cite as

Boris Aronov, Esther Ezra, and Micha Sharir. Testing Polynomials for Vanishing on Cartesian Products of Planar Point Sets. In 36th International Symposium on Computational Geometry (SoCG 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 164, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{aronov_et_al:LIPIcs.SoCG.2020.8,
  author =	{Aronov, Boris and Ezra, Esther and Sharir, Micha},
  title =	{{Testing Polynomials for Vanishing on Cartesian Products of Planar Point Sets}},
  booktitle =	{36th International Symposium on Computational Geometry (SoCG 2020)},
  pages =	{8:1--8:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-143-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{164},
  editor =	{Cabello, Sergio and Chen, Danny Z.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2020.8},
  URN =		{urn:nbn:de:0030-drops-121666},
  doi =		{10.4230/LIPIcs.SoCG.2020.8},
  annote =	{Keywords: Algebraic decision tree, Polynomial partition, Collinearity testing, 3SUM-hard problems, Polynomials vanishing on Cartesian products}
}
Document
Invited Talk
What Makes a Variant of Query Determinacy (Un)Decidable? (Invited Talk)

Authors: Jerzy Marcinkowski

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)


Abstract
This paper was written as the companion paper of the ICDT 2020 invited tutorial. Query determinacy is a broad topic, with literally hundreds of papers published since late 1980s. This paper is not going to be a "survey" but rather a personal perspective of a person somehow involved in the recent developments in the area. First I explain how, in the last 30+ years, the question of determinacy was formalized. There are many parameters here: obviously one needs to choose the query language of the available views and the query language of the query itself. But - surprisingly - there is also some choice regarding what the word "to compute" actually means in this context. Then I concentrate on certain variants of the decision problem of determinacy (for each choice of parameters there is one such problem) and explain how I understand the mechanisms rendering such variants of determinacy decidable or undecidable. This is on a rather informal level. No really new theorems are presented, but I show some improvements of existing theorems and also simplified proofs of some of the earlier results.

Cite as

Jerzy Marcinkowski. What Makes a Variant of Query Determinacy (Un)Decidable? (Invited Talk). In 23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{marcinkowski:LIPIcs.ICDT.2020.2,
  author =	{Marcinkowski, Jerzy},
  title =	{{What Makes a Variant of Query Determinacy (Un)Decidable?}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.2},
  URN =		{urn:nbn:de:0030-drops-119265},
  doi =		{10.4230/LIPIcs.ICDT.2020.2},
  annote =	{Keywords: database theory, query, view, determinacy}
}
Document
Optimal Joins Using Compact Data Structures

Authors: Gonzalo Navarro, Juan L. Reutter, and Javiel Rojas-Ledesma

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)


Abstract
Worst-case optimal join algorithms have gained a lot of attention in the database literature. We now count with several algorithms that are optimal in the worst case, and many of them have been implemented and validated in practice. However, the implementation of these algorithms often requires an enhanced indexing structure: to achieve optimality we either need to build completely new indexes, or we must populate the database with several instantiations of indexes such as B+-trees. Either way, this means spending an extra amount of storage space that may be non-negligible. We show that optimal algorithms can be obtained directly from a representation that regards the relations as point sets in variable-dimensional grids, without the need of extra storage. Our representation is a compact quadtree for the static indexes, and a dynamic quadtree sharing subtrees (which we dub a qdag) for intermediate results. We develop a compositional algorithm to process full join queries under this representation, and show that the running time of this algorithm is worst-case optimal in data complexity. Remarkably, we can extend our framework to evaluate more expressive queries from relational algebra by introducing a lazy version of qdags (lqdags). Once again, we can show that the running time of our algorithms is worst-case optimal.

Cite as

Gonzalo Navarro, Juan L. Reutter, and Javiel Rojas-Ledesma. Optimal Joins Using Compact Data Structures. In 23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{navarro_et_al:LIPIcs.ICDT.2020.21,
  author =	{Navarro, Gonzalo and Reutter, Juan L. and Rojas-Ledesma, Javiel},
  title =	{{Optimal Joins Using Compact Data Structures}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.21},
  URN =		{urn:nbn:de:0030-drops-119453},
  doi =		{10.4230/LIPIcs.ICDT.2020.21},
  annote =	{Keywords: Join algorithms, Compact data structures, Quadtrees, AGM bound}
}
  • Refine by Author
  • 5 Bézivin, Jean
  • 3 Mertzios, George B.
  • 3 Raskin, Jean-François
  • 3 Rumpe, Bernhard
  • 3 Schewe, Sven
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Computational geometry
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Regular languages
  • Show More...

  • Refine by Keyword
  • 2 Büchi automata
  • 2 Coalgebra Modalities
  • 2 Conceptual modeling
  • 2 Dagstuhl Seminar 04101
  • 2 graph
  • Show More...

  • Refine by Type
  • 50 document

  • Refine by Publication Year
  • 9 2017
  • 6 2008
  • 6 2020
  • 4 2010
  • 4 2021
  • 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