15 Search Results for "Müller, P."


Document
Automating OBDD proofs is NP-hard

Authors: Dmitry Itsykson and Artur Riazanov

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


Abstract
We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al., 2020] to establish the hardness of automatability result for Cutting Planes.

Cite as

Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.MFCS.2022.59,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Automating OBDD proofs is NP-hard}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{59:1--59:15},
  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.59},
  URN =		{urn:nbn:de:0030-drops-168575},
  doi =		{10.4230/LIPIcs.MFCS.2022.59},
  annote =	{Keywords: proof complexity, OBDD, automatability, lifting, dag-like communication}
}
Document
Track A: Algorithms, Complexity and Games
Learning Algorithms Versus Automatability of Frege Systems

Authors: Ján Pich and Rahul Santhanam

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


Abstract
We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system P, we prove that the following statements are equivalent, - Provable learning. P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries. - Provable automatability. P proves efficiently that P is automatable by non-uniform circuits on propositional formulas expressing p-size circuit lower bounds. Here, P is sufficiently strong and well-behaved if I.-III. holds: I. P p-simulates Jeřábek’s system WF (which strengthens the Extended Frege system EF by a surjective weak pigeonhole principle); II. P satisfies some basic properties of standard proof systems which p-simulate WF; III. P proves efficiently for some Boolean function h that h is hard on average for circuits of subexponential size. For example, if III. holds for P = WF, then Items 1 and 2 are equivalent for P = WF. The notion of automatability in Item 2 is slightly modified so that the automating algorithm outputs a proof of a given formula (expressing a p-size circuit lower bound) in p-time in the length of the shortest proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound). If there is a function h ∈ NE∩ coNE which is hard on average for circuits of size 2^{n/4}, for each sufficiently big n, then there is an explicit propositional proof system P satisfying properties I.-III., i.e. the equivalence of Items 1 and 2 holds for P.

Cite as

Ján Pich and Rahul Santhanam. Learning Algorithms Versus Automatability of Frege Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 101:1-101:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{pich_et_al:LIPIcs.ICALP.2022.101,
  author =	{Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{Learning Algorithms Versus Automatability of Frege Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{101:1--101: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.101},
  URN =		{urn:nbn:de:0030-drops-164427},
  doi =		{10.4230/LIPIcs.ICALP.2022.101},
  annote =	{Keywords: learning algorithms, automatability, proof complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games

Authors: Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen

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


Abstract
In this paper, we look at good-for-games Rabin automata that recognise a Muller language (a language that is entirely characterised by the set of letters that appear infinitely often in each word). We establish that minimal such automata are exactly of the same size as the minimal memory required for winning Muller games that have this language as their winning condition. We show how to effectively construct such minimal automata. Finally, we establish that these automata can be exponentially more succinct than equivalent deterministic ones, thus proving as a consequence that chromatic memory for winning a Muller game can be exponentially larger than unconstrained memory.

Cite as

Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen. On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 117:1-117:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2022.117,
  author =	{Casares, Antonio and Colcombet, Thomas and Lehtinen, Karoliina},
  title =	{{On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{117:1--117: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.117},
  URN =		{urn:nbn:de:0030-drops-164580},
  doi =		{10.4230/LIPIcs.ICALP.2022.117},
  annote =	{Keywords: Infinite duration games, Muller games, Rabin conditions, omega-regular languages, memory in games, good-for-games automata}
}
Document
Extended Abstract
High-Entropy Dual Functions and Locally Decodable Codes (Extended Abstract)

Authors: Jop Briët and Farrokh Labib

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)


Abstract
Locally decodable codes (LDCs) allow any single encoded message symbol to be retrieved from a codeword with good probability by reading only a tiny number of codeword symbols, even if the codeword is partially corrupted. LDCs have surprisingly many applications in computer science and mathematics (we refer to [Yekhanin, 2012; Lovett, 2007] for extensive surveys). But despite their ubiquity, they are poorly understood. Of particular interest is the tradeoff between the codeword length N as a function of message length k when the query complexity - the number of probed codeword symbols - and alphabet size are constant. The Hadamard code is a 2-query LDC of length N = 2^O(k) and this length is optimal in the 2-query regime [Lovett, 2007]. For q ≥ 3, near-exponential gaps persist between the best-known upper and lower bounds. The family of Reed-Muller codes, which generalize the Hadamard code, were for a long time the best-known examples, giving q-query LDCs of length exp(O(k^{1/(q-1)})), until breakthrough constructions of matching vector LDCs of Yekhanin and Efremenko [Yekhanin, 2008; Efremenko, 2012]. In contrast with other combinatorial objects such as expander graphs, the probabilistic method has so far not been successfully used to beat the best explicit LDC constructions. In [Lovett, 2007], a probabilistic framework was given that could in principle yield best-possible LDCs, albeit non-constructively. A special instance of this framework connects LDCs with a probabilistic version of Szemerédi’s theorem. The setup for this is as follows: For a finite abelian group G of size N = |G|, let D ⊆ G be a random subset where each element is present with probability ρ independently of all others. For k ≥ 3 and ε ∈ (0,1), let E be the event that every subset A ⊆ G of size |A| ≥ ε |G| contains a proper k-term arithmetic progression with common difference in D. For fixed ε > 0 and sufficiently large N, it is an open problem to determine the smallest value of ρ - denoted ρ_k - such that Pr[E] ≥ 1/2. In [Lovett, 2007] it is shown that there exist k-query LDCs of message length Ω(ρ_k N) and codeword length O(N). As such, Szemerédi’s theorem with random differences, in particular lower bounds on ρ_k, can be used to show the existence of LDCs. Conversely, this connection indirectly implies the best-known upper bounds on ρ_k for all k ≥ 3 [Lovett, 2007; Lovett, 2007]. However, a conjecture from [Lovett, 2007] states that over ℤ_N we have ρ_k ≤ O_k(N^{-1}log N) for all k, which would be best-possible. Truth of this conjecture would imply that over this group, Szemerédi’s theorem with random differences cannot give LDCs better than the Hadamard code. For finite fields, Altman [Lovett, 2007] showed that this is false. In particular, over 𝔽_pⁿ for p odd, he proved that ρ₃ ≥ Ω(p^{-n} n²); generally, ρ_k ≥ Ω(p^{-n} n^{k-1}) holds when p ≥ k+1 [Lovett, 2007]. In turn, these bounds are conjectured to be optimal for the finite-field setting, which would imply that over finite fields, Szemerédi’s theorem with random differences cannot give LDCs better than Reed-Muller codes. The finite-field conjecture is motivated mainly by the possibility that so-called dual functions can be approximated well by polynomial phases, functions of the form e^{2π i P(x)/p} where P is a multivariate polynomial over 𝔽_p. We show that this is false. Using Yekhanin’s matching-vector-code construction, we give dual functions of order k over 𝔽_pⁿ that cannot be approximated in L_∞-distance by polynomial phases of degree k-1. This answers in the negative a natural finite-field analog of a problem of Frantzikinakis over ℕ [Lovett, 2007].

Cite as

Jop Briët and Farrokh Labib. High-Entropy Dual Functions and Locally Decodable Codes (Extended Abstract). In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 76:1-76:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{briet_et_al:LIPIcs.ITCS.2021.76,
  author =	{Bri\"{e}t, Jop and Labib, Farrokh},
  title =	{{High-Entropy Dual Functions and Locally Decodable Codes}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{76:1--76:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.76},
  URN =		{urn:nbn:de:0030-drops-136157},
  doi =		{10.4230/LIPIcs.ITCS.2021.76},
  annote =	{Keywords: Higher-order Fourier analysis, dual functions, finite fields, additive combinatorics, coding theory}
}
Document
Invited Talk
Proofs of Soundness and Proof Search (Invited Talk)

Authors: Albert Atserias

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)


Abstract
Let P be a sound proof system for propositional logic. For each CNF formula F, let SAT(F) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with those of F (e.g., F itself). For each integer s, let REF(F,s) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with the P-refutations of F of length s. Since P is sound, it is obvious that the conjunction formula SAT(F) & REF(F,s) is unsatisfiable for any choice of F and s. It has been long known that, for many natural proof systems P and for the most natural formalizations of the formulas SAT and REF, the unsatisfiability of SAT(F) & REF(F,s) can be established by a short refutation. In addition, for many P, these short refutations live in the proof system P itself. This is the case for all Frege proof systems. In contrast it was known since the early 2000’s that Resolution proofs of Resolution’s soundness statements must have superpolynomial length. In this talk I will explain how the soundness formulas for a proof system P relate to the computational complexity of the proof search problem for P. In particular, I will explain how such formulas are used in the recent proof that the problem of approximating the minimum proof-length for Resolution is NP-hard (Atserias-Müller 2019). Besides playing a key role in this hardness of approximation result, the renewed interest in the soundness formulas led to a complete answer to the question whether Resolution has subexponential-length proofs of its own soundness statements (Garlík 2019).

Cite as

Albert Atserias. Proofs of Soundness and Proof Search (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{atserias:LIPIcs.FSTTCS.2020.2,
  author =	{Atserias, Albert},
  title =	{{Proofs of Soundness and Proof Search}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.2},
  URN =		{urn:nbn:de:0030-drops-132439},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.2},
  annote =	{Keywords: Proof complexity, automatability, Resolution, proof search, consistency statements, lower bounds, reflection principle, satisfiability}
}
Document
The Trickle-In Effect: Modeling Passenger Behavior in Delay Management

Authors: Anita Schöbel, Julius Pätzold, and Jörg P. Müller

Published in: OASIcs, Volume 75, 19th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2019)


Abstract
Delay management is concerned with making decisions if a train should wait for passengers from delayed trains or if it should depart on time. Models for delay management exist and can be adapted to capacities of stations, capacities of tracks, or respect vehicle and driver schedules, passengers' routes and further constraints. Nevertheless, what has been neglected so far, is that a train cannot depart as planned if passengers from another train trickle in one after another such that the doors of the departing train cannot close. This effect is often observed in real-world, but has not yet been taken into account in delay management. We show the impact of this "trickle-in" effect to departure delays of trains under different conditions. We then modify existing delay management models to take the trickle-in effect into account. This can be done by forbidding certain intervals for departure. We present an integer programming formulation with these additional constraints resulting in a generalization of classic delay management models. We analyze the resulting model and identify parameters with which it can be best approximated by the classical delay management problem. Experimentally, we show that the trickle-in effect has a high impact on the overall delay of public transport systems. We discuss the impact of the trickle-in effect on the objective function value and on the computation time of the delay management problem. We also analyze the trickle-in effect for timetables which have been derived without taking this particular behavioral pattern of passengers into account.

Cite as

Anita Schöbel, Julius Pätzold, and Jörg P. Müller. The Trickle-In Effect: Modeling Passenger Behavior in Delay Management. In 19th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2019). Open Access Series in Informatics (OASIcs), Volume 75, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{schobel_et_al:OASIcs.ATMOS.2019.6,
  author =	{Sch\"{o}bel, Anita and P\"{a}tzold, Julius and M\"{u}ller, J\"{o}rg P.},
  title =	{{The Trickle-In Effect: Modeling Passenger Behavior in Delay Management}},
  booktitle =	{19th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2019)},
  pages =	{6:1--6:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-128-3},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{75},
  editor =	{Cacchiani, Valentina and Marchetti-Spaccamela, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2019.6},
  URN =		{urn:nbn:de:0030-drops-114187},
  doi =		{10.4230/OASIcs.ATMOS.2019.6},
  annote =	{Keywords: Public Transport Planning, Delay Management, Integer Programming}
}
Document
Counting of Teams in First-Order Team Logics

Authors: Anselm Haak, Juha Kontinen, Fabian Müller, Heribert Vollmer, and Fan Yang

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


Abstract
We study descriptive complexity of counting complexity classes in the range from #P to #*NP. A corollary of Fagin’s characterization of NP by existential second-order logic is that #P can be logically described as the class of functions counting satisfying assignments to free relation variables in first-order formulae. In this paper we extend this study to classes beyond #P and extensions of first-order logic with team semantics. These team-based logics are closely related to existential second-order logic and its fragments, hence our results also shed light on the complexity of counting for extensions of first-order logic in Tarski’s semantics. Our results show that the class #*NP can be logically characterized by independence logic and existential second-order logic, whereas dependence logic and inclusion logic give rise to subclasses of #*NP and #P, respectively. We also study the function class generated by inclusion logic and relate it to the complexity class TotP, which is a subclass of #P. Our main technical result shows that the problem of counting satisfying assignments for monotone Boolean Sigma_1-formulae is #*NP-complete with respect to Turing reductions as well as complete for the function class generated by dependence logic with respect to first-order reductions.

Cite as

Anselm Haak, Juha Kontinen, Fabian Müller, Heribert Vollmer, and Fan Yang. Counting of Teams in First-Order Team Logics. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 19:1-19:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{haak_et_al:LIPIcs.MFCS.2019.19,
  author =	{Haak, Anselm and Kontinen, Juha and M\"{u}ller, Fabian and Vollmer, Heribert and Yang, Fan},
  title =	{{Counting of Teams in First-Order Team Logics}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{19:1--19:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.19},
  URN =		{urn:nbn:de:0030-drops-109634},
  doi =		{10.4230/LIPIcs.MFCS.2019.19},
  annote =	{Keywords: team-based logics, counting classes, finite model theory, descriptive complexity}
}
Document
Robust Multiplication-Based Tests for Reed-Muller Codes

Authors: Prahladh Harsha and Srikanth Srinivasan

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
We consider the following multiplication-based tests to check if a given function f: F^n_q -> F_q is the evaluation of a degree-d polynomial over F_q for q prime. Test_{e,k}: Pick P_1,...,P_k independent random degree-e polynomials and accept iff the function f P_1 ... P_k is the evaluation of a degree-(d + ek) polynomial. We prove the robust soundness of the above tests for large values of e, answering a question of Dinur and Guruswami (FOCS 2013). Previous soundness analyses of these tests were known only for the case when either e = 1 or k = 1. Even for the case k = 1 and e > 1, earlier soundness analyses were not robust. We also analyze a derandomized version of this test, where (for example) the polynomials P_1 ,... , P_k can be the same random polynomial P. This generalizes a result of Guruswami et al. (STOC 2014). One of the key ingredients that go into the proof of this robust soundness is an extension of the standard Schwartz-Zippel lemma over general finite fields F_q, which may be of independent interest.

Cite as

Prahladh Harsha and Srikanth Srinivasan. Robust Multiplication-Based Tests for Reed-Muller Codes. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{harsha_et_al:LIPIcs.FSTTCS.2016.17,
  author =	{Harsha, Prahladh and Srinivasan, Srikanth},
  title =	{{Robust Multiplication-Based Tests for Reed-Muller Codes}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.17},
  URN =		{urn:nbn:de:0030-drops-68524},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.17},
  annote =	{Keywords: Polynomials over finite fields, Schwartz-Zippel lemma, Low degree testing, Low degree long code}
}
Document
On Higher-Order Fourier Analysis over Non-Prime Fields

Authors: Arnab Bhattacharyya, Abhishek Bhowmick, and Chetan Gupta

Published in: LIPIcs, Volume 60, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2016)


Abstract
The celebrated Weil bound for character sums says that for any low-degree polynomial P and any additive character chi, either chi(P) is a constant function or it is distributed close to uniform. The goal of higher-order Fourier analysis is to understand the connection between the algebraic and analytic properties of polynomials (and functions, generally) at a more detailed level. For instance, what is the tradeoff between the equidistribution of chi(P) and its "structure"? Previously, most of the work in this area was over fields of prime order. We extend the tools of higher-order Fourier analysis to analyze functions over general finite fields. Let K be a field extension of a prime finite field F_p. Our technical results are: 1. If P: K^n -> K is a polynomial of degree <= d, and E[chi(P(x))] > |K|^{-s} for some s > 0 and non-trivial additive character chi, then P is a function of O_{d, s}(1) many non-classical polynomials of weight degree < d. The definition of non-classical polynomials over non-prime fields is one of the contributions of this work. 2. Suppose K and F are of bounded order, and let H be an affine subspace of K^n. Then, if P: K^n -> K is a polynomial of degree d that is sufficiently regular, then (P(x): x in H) is distributed almost as uniformly as possible subject to constraints imposed by the degree of P. Such a theorem was previously known for H an affine subspace over a prime field. The tools of higher-order Fourier analysis have found use in different areas of computer science, including list decoding, algorithmic decomposition and testing. Using our new results, we revisit some of these areas. (i) For any fixed finite field K, we show that the list decoding radius of the generalized Reed Muller code over K equals the minimum distance of the code. (ii) For any fixed finite field K, we give a polynomial time algorithm to decide whether a given polynomial P: K^n -> K can be decomposed as a particular composition of lesser degree polynomials. (iii) For any fixed finite field K, we prove that all locally characterized affine-invariant properties of functions f: K^n -> K are testable with one-sided error.

Cite as

Arnab Bhattacharyya, Abhishek Bhowmick, and Chetan Gupta. On Higher-Order Fourier Analysis over Non-Prime Fields. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 60, pp. 23:1-23:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bhattacharyya_et_al:LIPIcs.APPROX-RANDOM.2016.23,
  author =	{Bhattacharyya, Arnab and Bhowmick, Abhishek and Gupta, Chetan},
  title =	{{On Higher-Order Fourier Analysis over Non-Prime Fields}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2016)},
  pages =	{23:1--23:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-018-7},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{60},
  editor =	{Jansen, Klaus and Mathieu, Claire and Rolim, Jos\'{e} D. P. and Umans, Chris},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2016.23},
  URN =		{urn:nbn:de:0030-drops-66463},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2016.23},
  annote =	{Keywords: finite fields, higher order fourier analysis, coding theory, property testing}
}
Document
Summary-Based Inter-Procedural Analysis via Modular Trace Refinement

Authors: Franck Cassez, Christian Müller, and Karla Burnett

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)


Abstract
We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results.

Cite as

Franck Cassez, Christian Müller, and Karla Burnett. Summary-Based Inter-Procedural Analysis via Modular Trace Refinement. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 545-556, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{cassez_et_al:LIPIcs.FSTTCS.2014.545,
  author =	{Cassez, Franck and M\"{u}ller, Christian and Burnett, Karla},
  title =	{{Summary-Based Inter-Procedural Analysis via Modular Trace Refinement}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{545--556},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.545},
  URN =		{urn:nbn:de:0030-drops-48708},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.545},
  annote =	{Keywords: Program verification, Hoare Logic, Refinement, Automata}
}
Document
Software Engineering for Self-Adaptive Systems: A second Research Roadmap

Authors: Rogerio de Lemos, Holger Giese, Hausi Müller, Mary Shaw, Jesper Andersson, Luciano Baresi, Basil Becker, Nelly Bencomo, Yuriy Brun, Bojan Cikic, Ron Desmarais, Schahram Dustdar, Gregor Engels, Kurt Geihs, Karl M. Goeschka, Alessandra Gorla, Vincenzo Grassi, Poala Inverardi, Gabor Karsai, Jeff Kramer, Marin Litoiu, Antonia Lopes, Jeff Magee, Sam Malek, Serge Mankovskii, Raffaela Mirandola, John Mylopoulos, Oscar Nierstrasz, Mauro Pezzè, Christian Prehofer, Wilhelm Schäfer, Wilhelm Schlichting, Bradley Schmerl, Dennis B. Smith, Joao P. Sousa, Gabriel Tamura, Ladan Tahvildari, Norha M. Villegas, Thomas Vogel, Danny Weyns, Kenny Wong, and Jochen Wuttke

Published in: Dagstuhl Seminar Proceedings, Volume 10431, Software Engineering for Self-Adaptive Systems (2011)


Abstract
The goal of this roadmap paper is to summarize the state of-the-art and identify research challenges when developing, deploying and managing self-adaptive software systems. Instead of dealing with a wide range of topics associated with the field, we focus on four essential topics of self-adaptation: design space for adaptive solutions, processes, from centralized to decentralized control, and practical run-time verification and validation. For each topic, we present an overview, suggest future directions, and focus on selected challenges. This paper complements and extends a previous roadmap on software engineering for self-adaptive systems published in 2009 covering a different set of topics, and reflecting in part on the previous paper. This roadmap is one of the many results of the Dagstuhl Seminar 10431 on Software Engineering for Self-Adaptive Systems, which took place in October 2010.

Cite as

Rogerio de Lemos, Holger Giese, Hausi Müller, Mary Shaw, Jesper Andersson, Luciano Baresi, Basil Becker, Nelly Bencomo, Yuriy Brun, Bojan Cikic, Ron Desmarais, Schahram Dustdar, Gregor Engels, Kurt Geihs, Karl M. Goeschka, Alessandra Gorla, Vincenzo Grassi, Poala Inverardi, Gabor Karsai, Jeff Kramer, Marin Litoiu, Antonia Lopes, Jeff Magee, Sam Malek, Serge Mankovskii, Raffaela Mirandola, John Mylopoulos, Oscar Nierstrasz, Mauro Pezzè, Christian Prehofer, Wilhelm Schäfer, Wilhelm Schlichting, Bradley Schmerl, Dennis B. Smith, Joao P. Sousa, Gabriel Tamura, Ladan Tahvildari, Norha M. Villegas, Thomas Vogel, Danny Weyns, Kenny Wong, and Jochen Wuttke. Software Engineering for Self-Adaptive Systems: A second Research Roadmap. In Software Engineering for Self-Adaptive Systems. Dagstuhl Seminar Proceedings, Volume 10431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{delemos_et_al:DagSemProc.10431.3,
  author =	{de Lemos, Rogerio and Giese, Holger and M\"{u}ller, Hausi and Shaw, Mary and Andersson, Jesper and Baresi, Luciano and Becker, Basil and Bencomo, Nelly and Brun, Yuriy and Cikic, Bojan and Desmarais, Ron and Dustdar, Schahram and Engels, Gregor and Geihs, Kurt and Goeschka, Karl M. and Gorla, Alessandra and Grassi, Vincenzo and Inverardi, Poala and Karsai, Gabor and Kramer, Jeff and Litoiu, Marin and Lopes, Antonia and Magee, Jeff and Malek, Sam and Mankovskii, Serge and Mirandola, Raffaela and Mylopoulos, John and Nierstrasz, Oscar and Pezz\`{e}, Mauro and Prehofer, Christian and Sch\"{a}fer, Wilhelm and Schlichting, Wilhelm and Schmerl, Bradley and Smith, Dennis B. and Sousa, Joao P. and Tamura, Gabriel and Tahvildari, Ladan and Villegas, Norha M. and Vogel, Thomas and Weyns, Danny and Wong, Kenny and Wuttke, Jochen},
  title =	{{Software Engineering for Self-Adaptive Systems:  A second Research Roadmap}},
  booktitle =	{Software Engineering for Self-Adaptive Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10431},
  editor =	{Rogerio de Lemos and Holger Giese and Hausi M\"{u}ller and Mary Shaw},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10431.3},
  URN =		{urn:nbn:de:0030-drops-31561},
  doi =		{10.4230/DagSemProc.10431.3},
  annote =	{Keywords: }
}
Document
A Unified Framework for Verification Techniques for Object Invariants

Authors: Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)


Abstract
Object invariants define the consistency of objects. They have subtle semantics, mainly because of call-backs, multi-object invariants, and subclassing. Several verification techniques for object invariants have been proposed. It is difficult to compare these techniques, and to ascertain their soundness, because of their differences in restrictions on programs and invariants, in the use of advanced type systems (e.g., ownership types), in the meaning of invariants, and in proof obligations. We develop a unified framework for such techniques. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters which guarantee soundness. We instantiate our framework with three verification techniques from the literature, and use it to assess soundness and compare expressiveness.

Cite as

Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers. A Unified Framework for Verification Techniques for Object Invariants. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{drossopoulou_et_al:DagSemProc.08061.3,
  author =	{Drossopoulou, Sophia and Francalanza, Adrian and M\"{u}ller, P. and Summers, Alexander J.},
  title =	{{A Unified Framework for  Verification Techniques for Object Invariants}},
  booktitle =	{Types, Logics and Semantics for State},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8061},
  editor =	{Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.3},
  URN =		{urn:nbn:de:0030-drops-14278},
  doi =		{10.4230/DagSemProc.08061.3},
  annote =	{Keywords: Object invariants, visible states semantics, verification, sound}
}
Document
Inefficiency of equilibria in query auctions with continuous valuations

Authors: Elena Grigorieva, P. Jean-Jacques Herings, Rudolf Müller, and Dries Vermeulen

Published in: Dagstuhl Seminar Proceedings, Volume 7271, Computational Social Systems and the Internet (2007)


Abstract
We show that, when bidders have continuous valuations, any ex post equilibrium in an ex post individually rational query auction can only be ex post efficient when the running time of the auction is infinite for almost all realizations of valuations of the bidders. In contrast we show that, when we allow for inefficient allocations with arbitrarily small probability, there is a query auction (to be more specific, a bisection auction) that attains this level of approximate efficiency in equilibrium, while additionally the running time of the auction in equilibrium is finite for all realizations of valuations.

Cite as

Elena Grigorieva, P. Jean-Jacques Herings, Rudolf Müller, and Dries Vermeulen. Inefficiency of equilibria in query auctions with continuous valuations. In Computational Social Systems and the Internet. Dagstuhl Seminar Proceedings, Volume 7271, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{grigorieva_et_al:DagSemProc.07271.7,
  author =	{Grigorieva, Elena and Herings, P. Jean-Jacques and M\"{u}ller, Rudolf and Vermeulen, Dries},
  title =	{{Inefficiency of equilibria in query auctions with continuous valuations}},
  booktitle =	{Computational Social Systems and the Internet},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7271},
  editor =	{Peter Cramton and Rudolf M\"{u}ller and Eva Tardos and Moshe Tennenholtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07271.7},
  URN =		{urn:nbn:de:0030-drops-11616},
  doi =		{10.4230/DagSemProc.07271.7},
  annote =	{Keywords: Query auctions, ex post equilibrium, efficiency}
}
Document
06031 Abstracts Collection – Organic Computing – Controlled Emergence

Authors: Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)


Abstract
Organic Computing has emerged recently as a challenging vision for future information processing systems, based on the insight that we will soon be surrounded by large collections of autonomous systems equipped with sensors and actuators to be aware of their environment, to communicate freely, and to organize themselves in order to perform the actions and services required. Organic Computing Systems will adapt dynamically to the current conditions of its environment, they will be self-organizing, self-configuring, self-healing, self-protecting, self-explaining, and context-aware. From 15.01.06 to 20.01.06, the Dagstuhl Seminar 06031 ``Organic Computing – Controlled Emergence'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. The seminar was characterized by the very constructive search for common ground between engineering and natural sciences, between informatics on the one hand and biology, neuroscience, and chemistry on the other. The common denominator was the objective to build practically usable self-organizing and emergent systems or their components. An indicator for the practical orientation of the seminar was the large number of OC application systems, envisioned or already under implementation, such as the Internet, robotics, wireless sensor networks, traffic control, computer vision, organic systems on chip, an adaptive and self-organizing room with intelligent sensors or reconfigurable guiding systems for smart office buildings. The application orientation was also apparent by the large number of methods and tools presented during the seminar, which might be used as building blocks for OC systems, such as an evolutionary design methodology, OC architectures, especially several implementations of observer/controller structures, measures and measurement tools for emergence and complexity, assertion-based methods to control self-organization, wrappings, a software methodology to build reflective systems, and components for OC middleware. Organic Computing is clearly oriented towards applications but is augmented at the same time by more theoretical bio-inspired and nature-inspired work, such as chemical computing, theory of complex systems and non-linear dynamics, control mechanisms in insect swarms, homeostatic mechanisms in the brain, a quantitative approach to robustness, abstraction and instantiation as a central metaphor for understanding complex systems. Compared to its beginnings, Organic Computing is coming of age. The OC vision is increasingly padded with meaningful applications and usable tools, but the path towards full OC systems is still complex. There is progress in a more scientific understanding of emergent processes. In the future, we must understand more clearly how to open the configuration space of technical systems for on-line modification. Finally, we must make sure that the human user remains in full control while allowing the systems to optimize.

Cite as

Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz. 06031 Abstracts Collection – Organic Computing – Controlled Emergence. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{bellman_et_al:DagSemProc.06031.1,
  author =	{Bellman, Kirstie and Hofmann, Peter and M\"{u}ller-Schloer, Christian and Schmeck, Hartmut and W\"{u}rtz, Rolf P.},
  title =	{{06031 Abstracts Collection – Organic Computing – Controlled Emergence}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.1},
  URN =		{urn:nbn:de:0030-drops-5777},
  doi =		{10.4230/DagSemProc.06031.1},
  annote =	{Keywords: Emergence, self-organization, self-configuration, self-healing, self-protection, self-explaining, context-awareness}
}
Document
06031 Executive Summary – Organic Computing – Controlled Emergence

Authors: Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz

Published in: Dagstuhl Seminar Proceedings, Volume 6031, Organic Computing - Controlled Emergence (2006)


Abstract
Organic Computing has emerged recently as a challenging vision for future information processing systems, based on the insight that we will soon be surrounded by systems with massive numbers of processing elements, sensors and actuators, many of which will be autonomous. Because of the size of these systems it is infeasible for us to monitor and control them entirely from external observations; instead they will need to help us monitor, control and adapt themselves. To do so, these components will need to be aware of their environment, to communicate freely, and to organize themselves in order to perform the actions and services that are required. The presence of networks of intelligent systems in our environment opens up fascinating application areas but, at the same time, bears the problem of their controllability. Hence, we have to construct these systems which we increasingly depend on as robust, safe, flexible, and trustworthy as possible. In particular, a strong orientation towards human needs as opposed to a pure implementation of the technologically possible seems absolutely central. In order to achieve these goals, our technical systems will have to act more independently, flexibly, and autonomously, i.e., they will have to exhibit lifelike properties. We call those systems ''organic''. Hence, an ''Organic Computing System'' is a technical system which adapts dynamically to the current conditions of its environment. It will be selforganizing, selfconfiguring, selfhealing, selfprotecting, selfexplaining, and context-aware.

Cite as

Kirstie Bellman, Peter Hofmann, Christian Müller-Schloer, Hartmut Schmeck, and Rolf P. Würtz. 06031 Executive Summary – Organic Computing – Controlled Emergence. In Organic Computing - Controlled Emergence. Dagstuhl Seminar Proceedings, Volume 6031, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{bellman_et_al:DagSemProc.06031.2,
  author =	{Bellman, Kirstie and Hofmann, Peter and M\"{u}ller-Schloer, Christian and Schmeck, Hartmut and W\"{u}rtz, Rolf P.},
  title =	{{06031 Executive Summary – Organic Computing – Controlled Emergence}},
  booktitle =	{Organic Computing - Controlled Emergence},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6031},
  editor =	{Kirstie Bellman and Peter Hofmann and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06031.2},
  URN =		{urn:nbn:de:0030-drops-5788},
  doi =		{10.4230/DagSemProc.06031.2},
  annote =	{Keywords: Emergence, self-organization, self-configuration, self-healing, self-protection, self-explaining, context-awareness}
}
  • Refine by Author
  • 2 Bellman, Kirstie
  • 2 Hofmann, Peter
  • 2 Müller-Schloer, Christian
  • 2 Schmeck, Hartmut
  • 2 Würtz, Rolf P.
  • Show More...

  • Refine by Classification
  • 2 Theory of computation
  • 1 Applied computing → Transportation
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Complexity classes
  • Show More...

  • Refine by Keyword
  • 3 automatability
  • 2 Emergence
  • 2 coding theory
  • 2 context-awareness
  • 2 finite fields
  • Show More...

  • Refine by Type
  • 15 document

  • Refine by Publication Year
  • 3 2022
  • 2 2006
  • 2 2016
  • 2 2019
  • 1 2007
  • 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