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

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.29
Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures

Authors: Stéphane Demri and Karin Quaas

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

Abstract
We introduce the class of tree constraint automata with data values in ℤ (equipped with the less than relation and equality predicates to constants), and we show that the nonemptiness problem is EXPTIME-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(ℤ) (CTL with constraints in ℤ) is EXPTIME-complete, and the satisfiability problem for CTL^*(ℤ) is 2ExpTime-complete (only decidability was known so far). By-product results with other concrete domains and other logics, are also briefly discussed.
Cite as

Stéphane Demri and Karin Quaas. Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 29:1-29:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{demri_et_al:LIPIcs.CONCUR.2023.29,
  author =	{Demri, St\'{e}phane and Quaas, Karin},
  title =	{{Constraint Automata on Infinite Data Trees: from CTL(\mathbb{Z})/CTL^*(\mathbb{Z}) to Decision Procedures}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.29},
  URN =		{urn:nbn:de:0030-drops-190238},
  doi =		{10.4230/LIPIcs.CONCUR.2023.29},
  annote =	{Keywords: Constraints, Constraint Automata, Temporal Logics, Infinite Data Trees}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  booktitle =	{LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems},
  pages =	{04:1--04:34},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.59
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.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
DOI: 10.4230/LIPIcs.ICALP.2022.101
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.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
DOI: 10.4230/LIPIcs.ICALP.2022.117
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.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
DOI: 10.4230/LITES.7.1.2
We know what you're doing! Application detection using thermal data

Authors: Philipp Miedl, Rehan Ahmed, and Lothar Thiele

Published in: LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security. Leibniz Transactions on Embedded Systems, Volume 7, Issue 1

Abstract
Modern mobile and embedded devices have high computing power which allows them to be used for multiple purposes. Therefore, applications with low security restrictions may execute on the same device as applications handling highly sensitive information. In such a setup, a security risk occurs if it is possible that an application uses system characteristics to gather information about another application on the same device.In this work, we present a method to leak sensitive runtime information by just using temperature sensor readings of a mobile device. We employ a Convolutional-Neural-Network, Long Short-Term Memory units and subsequent label sequence processing to identify the sequence of executed applications over time. To test our hypothesis we collect data from two state-of-the-art smartphones and real user usage patterns. We show an extensive evaluation using laboratory data, where we achieve labelling accuracies up to 90% and negligible timing error. Based on our analysis we state that the thermal information can be used to compromise sensitive user data and increase the vulnerability of mobile devices. A study based on data collected outside of the laboratory opens up various future directions for research.
Cite as

Philipp Miedl, Rehan Ahmed, and Lothar Thiele. We know what you're doing! Application detection using thermal data. In LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security. Leibniz Transactions on Embedded Systems, Volume 7, Issue 1, pp. 02:1-02:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{miedl_et_al:LITES.7.1.2,
  author =	{Miedl, Philipp and Ahmed, Rehan and Thiele, Lothar},
  title =	{{We know what you're doing! Application detection using thermal data}},
  booktitle =	{LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security},
  pages =	{02:1--02:28},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2021},
  volume =	{7},
  number =	{1},
  editor =	{Miedl, Philipp and Ahmed, Rehan and Thiele, Lothar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.7.1.2},
  doi =		{10.4230/LITES.7.1.2},
  annote =	{Keywords: Thermal Monitoring, Side Channel, Data Leak, Sequence Labelling}
}
Document
Extended Abstract
DOI: 10.4230/LIPIcs.ITCS.2021.76
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.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
DOI: 10.4230/LIPIcs.FSTTCS.2020.2
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.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
DOI: 10.4230/OASIcs.ATMOS.2019.6
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.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
DOI: 10.4230/LIPIcs.MFCS.2019.19
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.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
DOI: 10.4230/LITES-v004-i001-a005
Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains

Authors: Eric W. D. Rozier, Kristin Y. Rozier, and Ulya Bayram

Published in: LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1

Abstract
As data centers attempt to cope with the exponential growth of data, new techniques for intelligent, software-defined data centers (SDDC) are being developed to confront the scale and pace of changing resources and requirements.  For cost-constrained environments, like those increasingly present in scientific research labs, SDDCs also may provide better reliability and performability with no additional hardware through the use of dynamic syndrome allocation. To do so, the middleware layers of SDDCs must be able to calculate and account for complex dependence relationships to determine an optimal data layout.  This challenge is exacerbated by the growth of constraints on the dependence problem when available resources are both large (due to a higher number of syndromes that can be stored) and small (due to the lack of available space for syndrome allocation). We present a quantitative method for characterizing these challenges using an analysis of attack domains for high-dimension variants of the $n$-queens problem that enables performable solutions via the SMT solver Z3. We demonstrate correctness of our technique, and provide experimental evidence of its efficacy; our implementation is publicly available.
Cite as

Eric W. D. Rozier, Kristin Y. Rozier, and Ulya Bayram. Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 05:1-05:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{rozier_et_al:LITES-v004-i001-a005,
  author =	{Rozier, Eric W. D. and Rozier, Kristin Y. and Bayram, Ulya},
  title =	{{Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains}},
  booktitle =	{LITES, Volume 4, Issue 1 (2017)},
  pages =	{05:1--05:26},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  editor =	{Rozier, Eric W. D. and Rozier, Kristin Y. and Bayram, Ulya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a005},
  doi =		{10.4230/LITES-v004-i001-a005},
  annote =	{Keywords: SMT, Data dependence, n-queens}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.17
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.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
DOI: 10.4230/LIPIcs.APPROX-RANDOM.2016.23
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
DOI: 10.4230/LIPIcs.FSTTCS.2014.545
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.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
DOI: 10.4230/LITES-v001-i002-a001
Blocking Optimality in Distributed Real-Time Locking Protocols

Authors: Björn Bernhard Brandenburg

Published in: LITES, Volume 1, Issue 2 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 2

Abstract
Lower and upper bounds on the maximum priority inversion blocking (pi-blocking) that is generally unavoidable in distributed multiprocessor real-time locking protocols (where resources may be accessed only from specific synchronization processors) are established. Prior work on suspension-based shared-memory multiprocessor locking protocols (which require resources to be accessible from all processors) has established asymptotically tight bounds of Ω(m) and Ω(n) maximum pi-blocking under suspension-oblivious and suspension-aware analysis, respectively, where m denotes the total number of processors and n denotes the number of tasks. In this paper, it is shown that, in the case of distributed semaphore protocols, there exist two different task allocation scenarios that give rise to distinct lower bounds. In the case of co-hosted task allocation, where application tasks may also be assigned to synchronization processors (i.e., processors hosting critical sections), Ω(Φ · n) maximum pi-blocking is unavoidable for some tasks under any locking protocol under both suspension-aware and suspension-oblivious schedulability analysis, where Φ denotes the ratio of the maximum response time to the shortest period. In contrast, in the case of disjoint task allocation (i.e., if application tasks may not be assigned to synchronization processors), only Ω(m) and Ω(n) maximum pi-blocking is fundamentally unavoidable under suspension-oblivious and suspension-aware analysis, respectively, as in the shared-memory case. These bounds are shown to be asymptotically tight with the construction of two new distributed real-time locking protocols that ensure O(m) and O(n) maximum pi-blocking under suspension-oblivious and suspension-aware analysis, respectively.
Cite as

Björn Bernhard Brandenburg. Blocking Optimality in Distributed Real-Time Locking Protocols. In LITES, Volume 1, Issue 2 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 2, pp. 01:1-01:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{brandenburg:LITES-v001-i002-a001,
  author =	{Brandenburg, Bj\"{o}rn Bernhard},
  title =	{{Blocking Optimality in Distributed Real-Time Locking Protocols}},
  booktitle =	{LITES, Volume 1, Issue 2 (2014)},
  pages =	{01:1--01:22},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2014},
  volume =	{1},
  number =	{2},
  editor =	{Brandenburg, Bj\"{o}rn Bernhard},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v001-i002-a001},
  doi =		{10.4230/LITES-v001-i002-a001},
  annote =	{Keywords: Distributed multiprocessor real-time systems, Real-time locking, Priority inversion, Blocking optimality}
}
  • 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
  • 2 Theory of computation → Logic and verification
  • 1 Applied computing → Transportation
  • 1 Computer systems organization → Embedded and cyber-physical systems
  • 1 Computer systems organization → Real-time systems
  • Show More...

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

  • Refine by Type
  • 20 document

  • Refine by Publication Year
  • 4 2022
  • 2 2006
  • 2 2014
  • 2 2016
  • 2 2019
  • 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
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact