Prochain Exposé
Thursday December 9th, 4:15PM Paris/France. (Weblink)
Fabio Mogavero (Università degli Studi di Napoli Federico II, Italy)
Herbrand Property, Finite Quasi-Herbrand Models, and a Chandra-Merlin Theorem for Quantified Conjunctive Queries.
A structure enjoys the Herbrand property if, whenever it satisfies an equality between some terms, these terms are unifiable. On such structures the expressive power of equalities becomes trivial, as their semantic satisfiability is reduced to a purely syntactic check. In this work, we introduce the notion of Herbrand property and develop it in a finite model-theoretic perspective. We provide, indeed, a canonical realization of the new concept by what we call quasi-Herbrand models and observe that, in stark contrast with the naive implementation of the property via standard Herbrand models, their universe can be finite even in presence of functions in the vocabulary. We exploit this feature to decide and collapse the general and finite version of the satisfiability and entailment problems for previously unsettled fragments of first-order logic. We take advantage of the Herbrand property also to establish novel and tight complexity results for the aforementioned decision questions. In particular, we show that the finite containment problem for quantified conjunctive queries is NPTIME-complete, tightening along two dimensions the known 3EXPTIME upper bound for the general version of the problem (Chen, Madelaine, and Martin, LICS'08). We finally present an alternative view on this result by generalizing to such queries the classic characterization of conjunctive query containment via polynomial-time verifiable homomorphisms (Chandra and Merlin, STOC'77).
Exposés des semaines suivantes
Thursday December 16th, 3PM Paris/France. (Weblink)
Yvo Meeres (University of Leipzig, Germany)
Accepting Directed Acyclic Graphs with the Help of Finite State Automata.
Analogously to regular string and tree languages, regular directed graph (DAG) languages had been defined in literature. Although called regular, those DAG-languages are way more powerful and, consequently, standard problems have a higher complexity than in the string case. Top-down as well as bottom-up deterministic DAG languages are subclasses of the regular DAG languages. We refine this hierarchy by providing a weaker subclass of the deterministic DAG languages. Obviously, this weaker class exhibits beneficial algorithmic properties.For a DAG-automaton accepting a language in this new DAG language class, a classical finite state automaton (FSA) can be constructed which states enumerate the dangling edges throughout an appropriate run of the DAG-automaton. An edge is called dangling if not yet all of its vertices have been read in the run. This means that an FSA can be used for deciding membership of such DAGs.The motivation behind this joint work with Johannes Blum and Frank Drewes is the transfer of results about regular string languages to graphs. Furthermore, we provide a characterization of the class via the DAG-automaton’s rules.
Friday December 17th, 10AM, salle Markov.
Valeria Vignudelli (Ecole normale supérieure de Lyon, France)
Equational reasoning, metrics, and monads for nondeterministic and probabilistic systems
Programs combining nondeterministic and probabilistic features allow us to account for both the presence of concurrency, where scheduling choices may be unpredictable, and the presence of quantitative or uncertain information. In recent contributions, we have studied methods to reason about the equivalence of systems combining nondeterminism and probability. The quantitative information brought by probabilities moreover allows us to encompass program equivalence and to reason about the finer notion of program distance. This does not only tell us whether two systems are equivalent or not, but also how much they differ. As main reasoning tool, we use equational theories and their analogues for distances, in order to obtain axiomatizations of the systems and properties of interest. By modelling nondeterminism and probabilities via monads, we are able to show our results in the abstract setting of category theory and coalgebra. In this talk I will present our framework and show applications to proving equivalences and distances, e.g. bisimulation-based, of nondeterministic and probabilistic transition systems.
January 20th, 3PM.
Hugo Gimbert (CNRS, LaBRI, France)
Distributed Asynchronous Games With Causal Memory are Undecidable
The distributed version of the Ramadge and Wonham control problem asks for the existence of a correct controller of a plant modeled as an asynchronous transition system. The controllable plant is distributed on several finite-state processes which interact asynchronously using shared actions. The controller is distributed as well, and decomposes as one local controller on every process. Each local controller can choose to block some of the actions, called controllable actions, but it cannot block the uncontrollable actions from the environment. A controller is correct if it guarantees that every possible execution of the plant satisfies some specification. The controller synthesis problem is the decision problem which, given a plant as input, asks whether the system admits a correct controller. In case such a controller exists, the algorithm should compute one as well. The difficulty of the controller synthesis depends on several factors, including the architecture of the information flow between processes (pipeline, ring, ...), the information available to the controllers, and the specification. The choices of the local controllers can be based on several sources of information. A minima, a local controller monitors the sequence of states and actions of the local process. This information is called the *local view* of the controller. Pnueli and Rosner proved that the distributed controller synthesis problem is undecidable when local controllers are restricted to use their local view for taking decisions, even for very simple architectures. Gastin, Lerman and Zeitoun have proposed in 2004 a variant of the distributed controller synthesis problem where local controllers are allowed to base their decisions on their *causal past*. When a shared action is played by several processes then all the controllers of these processes are allowed to exchange as much information as they want, and in particular together they can compute their mutual view of the global execution: their causal past. In this setting, Gastin et al. established the decidability of the synthesis for series-parallel architectures, and left open the decidability in the general case. In this talk, we provide a negative answer to their open question: the distributed controller synthesis problem with causal memory is undecidable. We also review several architectures which where proved decidable or for which the decidability is still open.
Vos propositions sont les bienvenues !
