Главная

Thomas A. Henzinger

  1. Expressiveness and Closure Properties for Quantitative Languages.

    Пнд, 07/26/2010 - 15:01 — SomNambul
    Authors: Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger
    Subjects: Logic in Computer Science
    Abstract

    Weighted automata are nondeterministic automata with numerical weights on
    transitions. They can define quantitative languages~$L$ that assign to each
    word~$w$ a real number~$L(w)$. In the case of infinite words, the value of a
    run is naturally computed as the maximum, limsup, liminf, limit-average, or
    discounted-sum of the transition weights. The value of a word $w$ is the
    supremum of the values of the runs over $w$. We study expressiveness and
    closure questions about these quantitative languages.

  2. GIST: A Solver for Probabilistic Games.

    Чт, 04/15/2010 - 15:01 — SomNambul
    Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna
    Subjects: Logic in Computer Science
    Abstract

    Gist is a tool that (a) solves the qualitative analysis problem of turn-based
    probabilistic games with {\omega}-regular objectives; and (b) synthesizes
    reasonable environment assumptions for synthesis of unrealizable
    specifications. Our tool provides the first and efficient implementations of
    several reduction-based techniques to solve turn-based probabilistic games, and
    uses the analysis of turn-based probabilistic games for synthesizing
    environment assumptions for unrealizable specifications.

  3. Measuring and Synthesizing Systems in Probabilistic Environments.

    Ср, 04/07/2010 - 15:02 — SomNambul
    Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh
    Subjects: Logic in Computer Science
    Abstract

    Often one has a preference order among the different systems that satisfy a
    given specification. Under a probabilistic assumption about the possible
    inputs, such a preference order is naturally expressed by a weighted automaton,
    which assigns to each word a value, such that a system is preferred if it
    generates a higher expected value.

  4. Synthesis of AMBA AHB from Formal Specification.

    Ср, 02/03/2010 - 16:01 — SomNambul
    Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Yashdeep Godhal
    Subjects: Logic in Computer Science
    Abstract

    The standard procedure for hardware design consists of describing circuit in
    a hardware description language at logic level followed by extensive
    verification and logic-synthesis. However, this process consumes significant
    time and needs a lot of effort. An alternative is to use formal specification
    language as a high-level hardware description language and synthesize hardware
    from formal specification. Bloem et.al. gave formal specifications and
    synthesize the AMBA AHB Arbiter.

  5. Qualitative Analysis of Partially-observable Markov Decision Processes.

    Чт, 09/10/2009 - 10:12 — SomNambul
    Authors: Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger
    Subjects: Computer Science and Game Theory
    Abstract

    We study observation-based strategies for partially-observable Markov
    decision processes (POMDPs) with omega-regular objectives. An observation-based
    strategy relies on partial information about the history of a play, namely, on
    the past sequence of observations. We consider the qualitative analysis
    problem: given a POMDP with an omega-regular objective, whether there is an
    observation-based strategy to achieve the objective with probability~1
    (almost-sure winning), or with positive probability (positive winning). Our
    main results are twofold.

  6. Probabilistic Weighted Automata.

    Чт, 09/10/2009 - 10:12 — SomNambul
    Authors: Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger
    Subjects: Logic in Computer Science
    Abstract

    Nondeterministic weighted automata are finite automata with numerical weights
    on transitions. They define quantitative languages L that assign to each word w
    a real number L(w). The value of an infinite word w is computed as the maximal
    value of all runs over w, and the value of a run as the maximum, limsup,
    liminf, limit average, or discounted sum of the transition weights. We
    introduce probabilistic weighted automata, in which the transitions are chosen
    in a randomized (rather than nondeterministic) fashion. Under almost-sure
    semantics (resp.

Math-arch

RSS-материал