Searcharxiv⌕ Search

arXiv subjects

Michael Benedikt

Publications and source records attributed to Michael Benedikt.

53 records · Page 3Linked to original sources
arXiv2019

FCC-ee: Your Questions Answered

This document answers in simple terms many FAQs about FCC-ee, including comparisons with other colliders. It complements the FCC-ee CDR and the FCC Physics CDR by addressing many questions from non-experts and clarifying issues raised during the European Strategy symposium in Granada, with a view to informing discussions in the period between now and the final endorsement by the CERN Council in 2020 of the European Strategy Group recommendations. This document will be regularly updated as more questions appear or new information becomes available.

hep-ph↗
arXiv2019

Machine detector interface for the $e^+e^-$ future circular collider

The international Future Circular Collider (FCC) study aims at a design of $pp$, $e^+e^-$, $ep$ colliders to be built in a new 100 km tunnel in the Geneva region. The $e^+e^-$ collider (FCC-ee) has a centre of mass energy range between 90 (Z-pole) and 375 GeV (tt_bar). To reach such unprecedented energies and luminosities, the design of the interaction region is crucial. The crab-waist collision scheme has been chosen for the design and it will be compatible with all beam energies. In this paper we will describe the machine detector interface layout including the solenoid compensation scheme. We will describe how this layout fulfills all the requirements set by the parameters table and by the physical constraints. We will summarize the studies of the impact of the synchrotron radiation, the analysis of trapped modes and of the backgrounds induced by single beam and luminosity effects giving an estimate of the losses in the interaction region and in the detector.

physics.acc-ph↗
arXiv2018

Machine Parameters and Projected Luminosity Performance of Proposed Future Colliders at CERN

In response to a request from the CERN Scientific Policy Committee (SPC), the machine parameters and expected luminosity performance for several proposed post-LHC collider projects at CERN are compiled: three types of hadron colliders (HL-LHC upgrade, FCC-hh and HE-LHC), a circular lepton collider (FCC-ee), a linear lepton collider (CLIC), and three options for lepton-hadron colliders (LHeC, HE-LHeC, and FCC-eh). Particular emphasis is put on availability, physics run time, and efficiency. The information contained in this document was presented at the SPC Meeting of September 2018. It will serve as one of the inputs to the 2019/20 Update of the European Strategy for Particle Physics.

physics.acc-ph↗
arXiv2018

When Can We Answer Queries Using Result-Bounded Data Interfaces?

We consider answering queries where the underlying data is available only over limited interfaces which provide lookup access to the tuples matching a given binding, but possibly restricting the number of output tuples returned. Interfaces imposing such "result bounds" are common in accessing data via the web. Given a query over a set of relations as well as some integrity constraints that relate the queried relations to the data sources, we examine the problem of deciding if the query is answerable over the interfaces; that is, whether there exists a plan that returns all answers to the query, assuming the source data satisfies the integrity constraints. The first component of our analysis of answerability is a reduction to a query containment problem with constraints. The second component is a set of "schema simplification" theorems capturing limitations on how interfaces with result bounds can be useful to obtain complete answers to queries. These results also help to show decidability for the containment problem that captures answerability, for many classes of constraints. The final component in our analysis of answerability is a "linearization" method, showing that query containment with certain guarded dependencies -- including those that emerge from answerability problems -- can be reduced to query containment for a well-behaved class of linear dependencies. Putting these components together, we get a detailed picture of how to check answerability over result-bounded services.

cs.DB↗
arXiv2018

Inference From Visible Information And Background Knowledge

We provide a wide-ranging study of the scenario where a subset of the relations in a relational vocabulary are visible to a user --- that is, their complete contents are known --- while the remaining relations are invisible. We also have a background theory --- invariants given by logical sentences --- which may relate the visible relations to invisible ones, and also may constrain both the visible and invisible relations in isolation. We want to determine whether some other information, given as a positive existential formula, can be inferred using only the visible information and the background theory. This formula whose inference we are concered with is denoted as the \emph{query}. We consider whether positive information about the query can be inferred, and also whether negative information -- the sentence does not hold -- can be inferred. We further consider both the instance-level version of the problem, where both the query and the visible instance are given, and the schema-level version, where we want to know whether truth or falsity of the query can be inferred in some instance of the schema.

cs.LO↗
arXiv2018

Proton Colliders at the Energy Frontier

Since the CERN ISR, hadron colliders have defined the energy frontier. Noteworthy are the conversion of the Super Proton Synchrotron (SPS) into a proton-antiproton collider, the Tevatron collider, as well as the abandoned SSC in the United States. Hadron colliders are likely to determine the pace of particle-physics progress also during the next hundred years. Discoveries at past hadron colliders were essential for establishing the so-called Standard Model of particle physics. The world's present flagship collider, the LHC, including its high-luminosity upgrade HL-LHC, is set to operate through the second half of the 2030's. Further increases of the energy reach during the 21st century require another, still more powerful hadron collider. Three options for a next hadron collider are presently under investigation. The Future Circular Collider (FCC) study, hosted by CERN, is designing a 100 TeV collider, to be installed inside a new 100 km tunnel in the Lake Geneva basin. A similar 100 km collider, called SppC, is being pursued by CAS-IHEP in China. In either machine, for the first time in hadron storage rings, synchrotron radiation damping will be significant. In parallel, the synchrotron-radiation power emitted inside the cold magnets becomes an important design constraint. One important difference between FCC and SppC is the magnet technology. FCC uses 16 Tesla magnets based on Nb3Sn superconductor, while SppC magnets shall be realized with cables made from iron-based high-temperature superconductor. Initially the SppC magnets are assumed to provide a more moderate dipole field of 12 T, but they can later be pushed to a final ultimate field of 24 T. A third collider presently under study is the High-Energy LHC (HE-LHC), which is a higher energy collider in the existing LHC tunnel, exploiting the FCC magnet technology in order to double the LHC energy at significantly higher luminosity.

physics.acc-ph↗
arXiv2017

Goal-Driven Query Answering for Existential Rules with Equality

Inspired by the magic sets for Datalog, we present a novel goal-driven approach for answering queries over terminating existential rules with equality (aka TGDs and EGDs). Our technique improves the performance of query answering by pruning the consequences that are not relevant for the query. This is challenging in our setting because equalities can potentially affect all predicates in a dataset. We address this problem by combining the existing singularization technique with two new ingredients: an algorithm for identifying the rules relevant to a query and a new magic sets algorithm. We show empirically that our technique can significantly improve the performance of query answering, and that it can mean the difference between answering a query in a few seconds or not being able to process the query at all.

cs.AI↗
arXiv2016

Query Answering with Transitive and Linear-Ordered Data

We consider entailment problems involving powerful constraint languages such as guarded existential rules, in which additional semantic restrictions are put on a set of distinguished relations. We consider restricting a relation to be transitive, restricting a relation to be the transitive closure of another relation, and restricting a relation to be a linear order. We give some natural generalizations of guardedness that allow inference to be decidable in each case, and isolate the complexity of the corresponding decision problems. Finally we show that slight changes in our conditions lead to undecidability.

cs.DB↗
arXiv2015

Status and Challenges for FCC-ee

We report the design status and beam dynamics challenges for the electron-positron branch of the Future Circular Collider (FCC) study, as of August 2015. After recalling motivation and physics requirements for the FCC-ee, we briefly discuss configurations and parameters, collider layout, the superconducting RF system, possible staging scenarios, final-focus optics, interaction-region (IR) issues, machine detector interface and IR synchrotron radiation, dynamic aperture, beam-beam effects, top-up injection, mono-chromatization option, impedances, instabilities, energy calibration and polarization, and SuperKEKB as a key demonstrator, before presenting conclusions and outlook.

physics.acc-ph↗
arXiv2015

Finite Open-World Query Answering with Number Restrictions (Extended Version)

Open-world query answering is the problem of deciding, given a set of facts, conjunction of constraints, and query, whether the facts and constraints imply the query. This amounts to reasoning over all instances that include the facts and satisfy the constraints. We study finite open-world query answering (FQA), which assumes that the underlying world is finite and thus only considers the finite completions of the instance. The major known decidable cases of FQA derive from the following: the guarded fragment of first-order logic, which can express referential constraints (data in one place points to data in another) but cannot express number restrictions such as functional dependencies; and the guarded fragment with number restrictions but on a signature of arity only two. In this paper, we give the first decidability results for FQA that combine both referential constraints and number restrictions for arbitrary signatures: we show that, for unary inclusion dependencies and functional dependencies, the finiteness assumption of FQA can be lifted up to taking the finite implication closure of the dependencies. Our result relies on new techniques to construct finite universal models of such constraints, for any bound on the maximal query size.

cs.LO↗
arXiv2015

Combining Existential Rules and Description Logics (Extended Version)

Query answering under existential rules -- implications with existential quantifiers in the head -- is known to be decidable when imposing restrictions on the rule bodies such as frontier-guardedness [BLM10, BLMS11]. Query answering is also decidable for description logics [Baa03], which further allow disjunction and functionality constraints (assert that certain relations are functions), however, they are focused on ER-type schemas, where relations have arity two. This work investigates how to get the best of both worlds: having decidable existential rules on arbitrary arity relations, while allowing rich description logics, including functionality constraints, on arity-two relations. We first show negative results on combining such decidable languages. Second, we introduce an expressive set of existential rules (frontier-one rules with a certain restriction) which can be combined with powerful constraints on arity-two relations (e.g. GC 2, ALCQIb) while retaining decidable query answering. Further, we provide conditions to add functionality constraints on the higher-arity relations.

cs.DB↗
arXiv2013

Controlling the Depth, Size, and Number of Subtrees for Two-variable Logic on Trees

Verification of properties of first order logic with two variables FO2 has been investigated in a number of contexts. Over arbitrary structures it is known to be decidable with NEXPTIME complexity, with finitely satisfiable formulas having exponential-sized models. Over word structures, where FO2 is known to have the same expressiveness as unary temporal logic, the same properties hold. Over finite labelled ordered trees FO2 is also of interest: it is known to have the same expressiveness as navigational XPath, a common query language for XML documents. Prior work on XPath and FO2 gives a 2EXPTIME bound for satisfiability of FO2. In this work we give the first in-depth look at the complexity of FO2 on trees, and on the size and depth of models. We show that the doubly-exponential bound is not tight, and neither do the NEXPTIME-completeness results from the word case carry over: the exact complexity varies depending on the vocabulary used, the presence or absence of a schema, and the encoding used for labels. Our results depend on an analysis of subformula types in models of FO2 formulas, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to finite satisfiability for FO2 sentences over trees.

cs.LO↗
arXiv2013

Two Variable vs. Linear Temporal Logic in Model Checking and Games

Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In this paper we consider two such restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is more expressive but FO2 can be more succinct, and hence it is not clear which should be easier to verify. We take a comprehensive look at the issue, giving a comparison of verification problems for FO2, LTL, and various sublogics thereof across a wide range of models. In particular, we look at unary temporal logic (UTL), a subset of LTL that is expressively equivalent to FO2; we also consider the stutter-free fragment of FO2, obtained by omitting the successor relation, and the expressively equivalent fragment of UTL, obtained by omitting the next and previous connectives. We give three logic-to-automata translations which can be used to give upper bounds for FO2 and UTL and various sublogics. We apply these to get new bounds for both non-deterministic systems (hierarchical and recursive state machines, games) and for probabilistic systems (Markov chains, recursive Markov chains, and Markov decision processes). We couple these with matching lower-bound arguments. Next, we look at combining FO2 verification techniques with those for LTL. We present here a language that subsumes both FO2 and LTL, and inherits the model checking properties of both languages. Our results give both a unified approach to understanding the behaviour of FO2 and LTL, along with a nearly comprehensive picture of the complexity of verification for these logics and their sublogics.

cs.LO↗
arXiv2012

Bisimilarity of Pushdown Systems is Nonelementary

Given two pushdown systems, the bisimilarity problem asks whether they are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the previously best known lower bound for this problem. Our lower bound result holds for normed pushdown systems as well.

cs.FL↗
arXiv2012

Querying Schemas With Access Restrictions

We study verification of systems whose transitions consist of accesses to a Web-based data-source. An access is a lookup on a relation within a relational database, fixing values for a set of positions in the relation. For example, a transition can represent access to a Web form, where the user is restricted to filling in values for a particular set of fields. We look at verifying properties of a schema describing the possible accesses of such a system. We present a language where one can describe the properties of an access path, and also specify additional restrictions on accesses that are enforced by the schema. Our main property language, AccLTL, is based on a first-order extension of linear-time temporal logic, interpreting access paths as sequences of relational structures. We also present a lower-level automaton model, Aautomata, which AccLTL specifications can compile into. We show that AccLTL and A-automata can express static analysis problems related to "querying with limited access patterns" that have been studied in the database literature in the past, such as whether an access is relevant to answering a query, and whether two queries are equivalent in the accessible data they can return. We prove decidability and complexity results for several restrictions and variants of AccLTL, and explain which properties of paths can be expressed in each restriction.

cs.DB↗
arXiv2011

Determining Relevance of Accesses at Runtime (Extended Version)

Consider the situation where a query is to be answered using Web sources that restrict the accesses that can be made on backend relational data by requiring some attributes to be given as input of the service. The accesses provide lookups on the collection of attributes values that match the binding. They can differ in whether or not they require arguments to be generated from prior accesses. Prior work has focused on the question of whether a query can be answered using a set of data sources, and in developing static access plans (e.g., Datalog programs) that implement query answering. We are interested in dynamic aspects of the query answering problem: given partial information about the data, which accesses could provide relevant data for answering a given query? We consider immediate and long-term notions of "relevant accesses", and ascertain the complexity of query relevance, for both conjunctive queries and arbitrary positive queries. In the process, we relate dynamic relevance of an access to query containment under access limitations and characterize the complexity of this problem; we produce several complexity results about containment that are of interest by themselves.

cs.DB↗