---
_id: '4399'
abstract:
- lang: eng
  text: 'A temporal interface for a software component is a finite automaton that
    specifies the legal sequences of calls to functions that are provided by the component.
    We compare and evaluate three different algorithms for automatically extracting
    temporal interfaces from program code: (1) a game algorithm that computes the
    interface as a representation of the most general environment strategy to avoid
    a safety violation; (2) a learning algorithm that repeatedly queries the program
    to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively
    refines an abstract interface hypothesis by adding relevant program variables.
    For comparison purposes, we present and implement the three algorithms in a unifying
    formal setting. While the three algorithms compute the same output and have similar
    worst-case complexities, their actual running times may differ considerably for
    a given input program. On the theoretical side, we provide for each of the three
    algorithms a family of input programs on which that algorithm outperforms the
    two alternatives. On the practical side, we evaluate the three algorithms experimentally
    on a variety of Java libraries. '
acknowledgement: This research was supported in part by the grant SFU/PRG 06-3, and
  by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Vasu
  full_name: Vasu Singh
  id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
  last_name: Singh
citation:
  ama: 'Beyer D, Henzinger TA, Singh V. Algorithms for interface synthesis. In: Vol
    4590. Springer; 2007:4-19. doi:<a href="https://doi.org/10.1007/978-3-540-73368-3_4">10.1007/978-3-540-73368-3_4</a>'
  apa: 'Beyer, D., Henzinger, T. A., &#38; Singh, V. (2007). Algorithms for interface
    synthesis (Vol. 4590, pp. 4–19). Presented at the CAV: Computer Aided Verification,
    Springer. <a href="https://doi.org/10.1007/978-3-540-73368-3_4">https://doi.org/10.1007/978-3-540-73368-3_4</a>'
  chicago: Beyer, Dirk, Thomas A Henzinger, and Vasu Singh. “Algorithms for Interface
    Synthesis,” 4590:4–19. Springer, 2007. <a href="https://doi.org/10.1007/978-3-540-73368-3_4">https://doi.org/10.1007/978-3-540-73368-3_4</a>.
  ieee: 'D. Beyer, T. A. Henzinger, and V. Singh, “Algorithms for interface synthesis,”
    presented at the CAV: Computer Aided Verification, 2007, vol. 4590, pp. 4–19.'
  ista: 'Beyer D, Henzinger TA, Singh V. 2007. Algorithms for interface synthesis.
    CAV: Computer Aided Verification, LNCS, vol. 4590, 4–19.'
  mla: Beyer, Dirk, et al. <i>Algorithms for Interface Synthesis</i>. Vol. 4590, Springer,
    2007, pp. 4–19, doi:<a href="https://doi.org/10.1007/978-3-540-73368-3_4">10.1007/978-3-540-73368-3_4</a>.
  short: D. Beyer, T.A. Henzinger, V. Singh, in:, Springer, 2007, pp. 4–19.
conference:
  name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:39Z
date_published: 2007-07-02T00:00:00Z
date_updated: 2021-01-12T07:56:41Z
day: '02'
doi: 10.1007/978-3-540-73368-3_4
extern: 1
intvolume: '      4590'
month: '07'
page: 4 - 19
publication_status: published
publisher: Springer
publist_id: '1059'
quality_controlled: 0
status: public
title: Algorithms for interface synthesis
type: conference
volume: 4590
year: '2007'
...
---
_id: '4402'
alternative_title:
- LNCS
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Pavol
  full_name: Pavol Cerny
  id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  last_name: Cerny
- first_name: Swarat
  full_name: Chaudhuri,Swarat
  last_name: Chaudhuri
citation:
  ama: 'Alur R, Cerny P, Chaudhuri S. Model Checking on Trees with Path Equivalences.
    In: Springer; 2007:664-678. doi:<a href="https://doi.org/1544">1544</a>'
  apa: 'Alur, R., Cerny, P., &#38; Chaudhuri, S. (2007). Model Checking on Trees with
    Path Equivalences (pp. 664–678). Presented at the TACAS: Tools and Algorithms
    for the Construction and Analysis of Systems, Springer. <a href="https://doi.org/1544">https://doi.org/1544</a>'
  chicago: Alur, Rajeev, Pavol Cerny, and Swarat Chaudhuri. “Model Checking on Trees
    with Path Equivalences,” 664–78. Springer, 2007. <a href="https://doi.org/1544">https://doi.org/1544</a>.
  ieee: 'R. Alur, P. Cerny, and S. Chaudhuri, “Model Checking on Trees with Path Equivalences,”
    presented at the TACAS: Tools and Algorithms for the Construction and Analysis
    of Systems, 2007, pp. 664–678.'
  ista: 'Alur R, Cerny P, Chaudhuri S. 2007. Model Checking on Trees with Path Equivalences.
    TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
    , 664–678.'
  mla: Alur, Rajeev, et al. <i>Model Checking on Trees with Path Equivalences</i>.
    Springer, 2007, pp. 664–78, doi:<a href="https://doi.org/1544">1544</a>.
  short: R. Alur, P. Cerny, S. Chaudhuri, in:, Springer, 2007, pp. 664–678.
conference:
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:08:40Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:43Z
day: '01'
doi: '1544'
extern: 1
month: '01'
page: 664 - 678
publication_status: published
publisher: Springer
publist_id: '1055'
quality_controlled: 0
status: public
title: Model Checking on Trees with Path Equivalences
type: conference
year: '2007'
...
---
_id: '4405'
abstract:
- lang: eng
  text: |-
    Background
    A central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce Qualitative networks, an extension of Boolean networks. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico.

    Results
    We consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 1086 states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis.

    Conclusion
    We introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.
author:
- first_name: Marc
  full_name: Schaub, Marc A
  last_name: Schaub
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jasmin
  full_name: Fisher, Jasmin
  last_name: Fisher
citation:
  ama: 'Schaub M, Henzinger TA, Fisher J. Qualitative networks: A symbolic approach
    to analyze biological signaling networks. <i>BMC Systems Biology</i>. 2007;1(4).
    doi:<a href="https://doi.org/10.1186/1752-0509-1-4">10.1186/1752-0509-1-4</a>'
  apa: 'Schaub, M., Henzinger, T. A., &#38; Fisher, J. (2007). Qualitative networks:
    A symbolic approach to analyze biological signaling networks. <i>BMC Systems Biology</i>.
    BioMed Central. <a href="https://doi.org/10.1186/1752-0509-1-4">https://doi.org/10.1186/1752-0509-1-4</a>'
  chicago: 'Schaub, Marc, Thomas A Henzinger, and Jasmin Fisher. “Qualitative Networks:
    A Symbolic Approach to Analyze Biological Signaling Networks.” <i>BMC Systems
    Biology</i>. BioMed Central, 2007. <a href="https://doi.org/10.1186/1752-0509-1-4">https://doi.org/10.1186/1752-0509-1-4</a>.'
  ieee: 'M. Schaub, T. A. Henzinger, and J. Fisher, “Qualitative networks: A symbolic
    approach to analyze biological signaling networks,” <i>BMC Systems Biology</i>,
    vol. 1, no. 4. BioMed Central, 2007.'
  ista: 'Schaub M, Henzinger TA, Fisher J. 2007. Qualitative networks: A symbolic
    approach to analyze biological signaling networks. BMC Systems Biology. 1(4).'
  mla: 'Schaub, Marc, et al. “Qualitative Networks: A Symbolic Approach to Analyze
    Biological Signaling Networks.” <i>BMC Systems Biology</i>, vol. 1, no. 4, BioMed
    Central, 2007, doi:<a href="https://doi.org/10.1186/1752-0509-1-4">10.1186/1752-0509-1-4</a>.'
  short: M. Schaub, T.A. Henzinger, J. Fisher, BMC Systems Biology 1 (2007).
date_created: 2018-12-11T12:08:41Z
date_published: 2007-01-08T00:00:00Z
date_updated: 2021-01-12T07:56:44Z
day: '08'
doi: 10.1186/1752-0509-1-4
extern: 1
intvolume: '         1'
issue: '4'
main_file_link:
- open_access: '0'
  url: http://www.biomedcentral.com/1752-0509/1/4
month: '01'
publication: BMC Systems Biology
publication_status: published
publisher: BioMed Central
publist_id: '325'
quality_controlled: 0
status: public
title: 'Qualitative networks: A symbolic approach to analyze biological signaling
  networks'
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
volume: 1
year: '2007'
...
---
_id: '4417'
abstract:
- lang: eng
  text: Counterexample-guided abstraction refinement (CEGAR) is a powerful technique
    to scale automatic program analysis techniques to large programs. However, so
    far it has been used primarily for model checking in the context of predicate
    abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract
    counterexample needs to be removed through abstraction refinement, there are often
    several choices, such as which program location(s) to refine, which abstract domain(s)
    to use at different locations, and which abstract values to compute. We define
    several plausible preference orderings on abstraction refinements, such as refining
    as “late” as possible and as “coarse” as possible. We present generic algorithms
    for finding refinements that are optimal with respect to the different preference
    orderings. We also compare the different orderings with respect to desirable properties,
    including the property if locally optimal refinements compose to a global optimum.
    Finally, we point out some difficulties with CEGAR for non-powerset domains.
acknowledgement: This research is partially supported by the Clore Fellowship Programme.
  Supported in part by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Roman
  full_name: Manevich, Roman
  last_name: Manevich
- first_name: John
  full_name: Field, John
  last_name: Field
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ganesan
  full_name: Ramalingam, Ganesan
  last_name: Ramalingam
- first_name: Mooly
  full_name: Sagiv, Mooly
  last_name: Sagiv
citation:
  ama: 'Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. Abstract counterexample-based
    refinement for powerset domains. In: <i>Program Analysis and Compilation, Theory
    and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th
    Birthday</i>. Vol 4444. Springer; 2007:273-292. doi:<a href="https://doi.org/10.1007/978-3-540-71322-7_13">10.1007/978-3-540-71322-7_13</a>'
  apa: 'Manevich, R., Field, J., Henzinger, T. A., Ramalingam, G., &#38; Sagiv, M.
    (2007). Abstract counterexample-based refinement for powerset domains. In <i>Program
    Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm
    on the Occasion of His 60th Birthday</i> (Vol. 4444, pp. 273–292). Springer. <a
    href="https://doi.org/10.1007/978-3-540-71322-7_13">https://doi.org/10.1007/978-3-540-71322-7_13</a>'
  chicago: 'Manevich, Roman, John Field, Thomas A Henzinger, Ganesan Ramalingam, and
    Mooly Sagiv. “Abstract Counterexample-Based Refinement for Powerset Domains.”
    In <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated
    to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, 4444:273–92. Springer,
    2007. <a href="https://doi.org/10.1007/978-3-540-71322-7_13">https://doi.org/10.1007/978-3-540-71322-7_13</a>.'
  ieee: 'R. Manevich, J. Field, T. A. Henzinger, G. Ramalingam, and M. Sagiv, “Abstract
    counterexample-based refinement for powerset domains,” in <i>Program Analysis
    and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on
    the Occasion of His 60th Birthday</i>, vol. 4444, Springer, 2007, pp. 273–292.'
  ista: 'Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. 2007.Abstract counterexample-based
    refinement for powerset domains. In: Program Analysis and Compilation, Theory
    and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th
    Birthday. LNCS, vol. 4444, 273–292.'
  mla: 'Manevich, Roman, et al. “Abstract Counterexample-Based Refinement for Powerset
    Domains.” <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated
    to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, vol. 4444, Springer,
    2007, pp. 273–92, doi:<a href="https://doi.org/10.1007/978-3-540-71322-7_13">10.1007/978-3-540-71322-7_13</a>.'
  short: 'R. Manevich, J. Field, T.A. Henzinger, G. Ramalingam, M. Sagiv, in:, Program
    Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm
    on the Occasion of His 60th Birthday, Springer, 2007, pp. 273–292.'
date_created: 2018-12-11T12:08:45Z
date_published: 2007-03-30T00:00:00Z
date_updated: 2021-01-12T07:56:49Z
day: '30'
doi: 10.1007/978-3-540-71322-7_13
extern: 1
intvolume: '      4444'
month: '03'
page: 273 - 292
publication: 'Program Analysis and Compilation, Theory and Practice: Essays Dedicated
  to Reinhard Wilhelm on the Occasion of His 60th Birthday'
publication_status: published
publisher: Springer
publist_id: '314'
quality_controlled: 0
status: public
title: Abstract counterexample-based refinement for powerset domains
type: book_chapter
volume: 4444
year: '2007'
...
---
_id: '4446'
abstract:
- lang: eng
  text: The Embedded Machine is a virtual machine that mediates in real time the interaction
    between software processes and physical processes. It separates the compilation
    of embedded programs into two phases. The first phase, the platform-independent
    compiler phase, generates E code (code executed by the Embedded Machine), which
    supervises the timing, not the scheduling of, application tasks relative to external
    events such as clock ticks and sensor interrupts. E code is portable and, given
    an input behavior, exhibits predictable (i.e., deterministic) timing and output
    behavior. The second phase, the platform-dependent compiler phase, checks the
    time safety of the E code, that is, whether platform performance (determined by
    the hardware) and platform utilization (determined by the scheduler of the operating
    system) enable its timely execution. We have used the Embedded Machine to compile
    and execute high-performance control applications written in Giotto, such as the
    flight control system of an autonomous model helicopter.
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Christoph
  full_name: Kirsch, Christoph M
  last_name: Kirsch
citation:
  ama: 'Henzinger TA, Kirsch C. The embedded machine: Predictable, portable real-time
    code. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. 2007;29(393).
    doi:<a href="https://doi.org/10.1145/1286821.1286824">10.1145/1286821.1286824</a>'
  apa: 'Henzinger, T. A., &#38; Kirsch, C. (2007). The embedded machine: Predictable,
    portable real-time code. <i>ACM Transactions on Programming Languages and Systems
    (TOPLAS)</i>. ACM. <a href="https://doi.org/10.1145/1286821.1286824">https://doi.org/10.1145/1286821.1286824</a>'
  chicago: 'Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable,
    Portable Real-Time Code.” <i>ACM Transactions on Programming Languages and Systems
    (TOPLAS)</i>. ACM, 2007. <a href="https://doi.org/10.1145/1286821.1286824">https://doi.org/10.1145/1286821.1286824</a>.'
  ieee: 'T. A. Henzinger and C. Kirsch, “The embedded machine: Predictable, portable
    real-time code,” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>,
    vol. 29, no. 393. ACM, 2007.'
  ista: 'Henzinger TA, Kirsch C. 2007. The embedded machine: Predictable, portable
    real-time code. ACM Transactions on Programming Languages and Systems (TOPLAS).
    29(393).'
  mla: 'Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable,
    Portable Real-Time Code.” <i>ACM Transactions on Programming Languages and Systems
    (TOPLAS)</i>, vol. 29, no. 393, ACM, 2007, doi:<a href="https://doi.org/10.1145/1286821.1286824">10.1145/1286821.1286824</a>.'
  short: T.A. Henzinger, C. Kirsch, ACM Transactions on Programming Languages and
    Systems (TOPLAS) 29 (2007).
date_created: 2018-12-11T12:08:53Z
date_published: 2007-10-01T00:00:00Z
date_updated: 2021-01-12T07:57:01Z
day: '01'
doi: 10.1145/1286821.1286824
extern: 1
intvolume: '        29'
issue: 393
month: '10'
publication: ACM Transactions on Programming Languages and Systems (TOPLAS)
publication_status: published
publisher: ACM
publist_id: '286'
quality_controlled: 0
status: public
title: 'The embedded machine: Predictable, portable real-time code'
type: journal_article
volume: 29
year: '2007'
...
---
_id: '4511'
abstract:
- lang: eng
  text: 'In the traditional view, a language is a set of words, i.e., a function from
    words to boolean values. We call this view “qualitative,” because each word either
    belongs to or does not belong to a language. Let Σ be an alphabet, and let us
    consider infinite words over Σ. Formally, a qualitative language over Σ is a function
    A: B . There are many applications of qualitative languages. For example, qualitative
    languages are used to specify the legal behaviors of systems, and zero-sum objectives
    of games played on graphs. In the former case, each behavior of a system is either
    legal or illegal; in the latter case, each outcome of a game is either winning
    or losing. For defining languages, it is convenient to use finite acceptors (or
    generators). In particular, qualitative languages are often defined using finite-state
    machines (so-called ω-automata) whose transitions are labeled by letters from
    Σ. For example, the states of an ω-automaton may represent states of a system,
    and the transition labels may represent atomic observables of a behavior. There
    is a rich and well-studied theory of finite-state acceptors of qualitative languages,
    namely, the theory of theω-regular languages.'
acknowledgement: This research was supported in part by the Swiss National Science
  Foundation and by the NSF grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Henzinger TA. Quantitative generalizations of languages. In: Vol 4588. Springer;
    2007:20-22. doi:<a href="https://doi.org/10.1007/978-3-540-73208-2_2">10.1007/978-3-540-73208-2_2</a>'
  apa: 'Henzinger, T. A. (2007). Quantitative generalizations of languages (Vol. 4588,
    pp. 20–22). Presented at the DLT: Developments in Language Theory, Springer. <a
    href="https://doi.org/10.1007/978-3-540-73208-2_2">https://doi.org/10.1007/978-3-540-73208-2_2</a>'
  chicago: Henzinger, Thomas A. “Quantitative Generalizations of Languages,” 4588:20–22.
    Springer, 2007. <a href="https://doi.org/10.1007/978-3-540-73208-2_2">https://doi.org/10.1007/978-3-540-73208-2_2</a>.
  ieee: 'T. A. Henzinger, “Quantitative generalizations of languages,” presented at
    the DLT: Developments in Language Theory, 2007, vol. 4588, pp. 20–22.'
  ista: 'Henzinger TA. 2007. Quantitative generalizations of languages. DLT: Developments
    in Language Theory, LNCS, vol. 4588, 20–22.'
  mla: Henzinger, Thomas A. <i>Quantitative Generalizations of Languages</i>. Vol.
    4588, Springer, 2007, pp. 20–22, doi:<a href="https://doi.org/10.1007/978-3-540-73208-2_2">10.1007/978-3-540-73208-2_2</a>.
  short: T.A. Henzinger, in:, Springer, 2007, pp. 20–22.
conference:
  name: 'DLT: Developments in Language Theory'
date_created: 2018-12-11T12:09:14Z
date_published: 2007-06-21T00:00:00Z
date_updated: 2021-01-12T07:59:21Z
day: '21'
doi: 10.1007/978-3-540-73208-2_2
extern: 1
intvolume: '      4588'
month: '06'
page: 20 - 22
publication_status: published
publisher: Springer
publist_id: '218'
quality_controlled: 0
status: public
title: Quantitative generalizations of languages
type: conference
volume: 4588
year: '2007'
...
---
_id: '4514'
abstract:
- lang: eng
  text: 'Digital technology is increasingly deployed in safety-critical situations.
    This calls for systematic design and verification methodologies that can cope
    with three major sources of system complexity: concurrency, real time, and uncertainty.
    We advocate a two-step process: formal modeling followed by algorithmic analysis
    (or, “model building” followed by “model checking”). We model the concurrent components
    of a reactive system as potential collaborators or adversaries in a multi-player
    game with temporal objectives, such as system safety. The real-time aspect of
    embedded systems requires models that combine discrete state transitions and continuous
    state evolutions. Uncertainty in the environment is naturally modeled by probabilistic
    state changes. As a result, we obtain three orthogonal extensions of the basic
    state-transition graph model for reactive systems —game graphs, timed graphs,
    and stochastic graphs— as well as combinations thereof. In this short text, we
    provide a uniform exposition of the underlying definitions. For verification algorithms,
    we refer the reader to the literature.'
acknowledgement: This research was supported in part by the Swiss National Science
  Foundation, and by the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Henzinger TA. Games, time, and probability: Graph models for system design
    and analysis. In: Vol 4362. Springer; 2007:103-110. doi:<a href="https://doi.org/10.1007/978-3-540-69507-3_7">10.1007/978-3-540-69507-3_7</a>'
  apa: 'Henzinger, T. A. (2007). Games, time, and probability: Graph models for system
    design and analysis (Vol. 4362, pp. 103–110). Presented at the SOFSEM: Current
    Trends in Theory and Practice of Computer Science, Springer. <a href="https://doi.org/10.1007/978-3-540-69507-3_7">https://doi.org/10.1007/978-3-540-69507-3_7</a>'
  chicago: 'Henzinger, Thomas A. “Games, Time, and Probability: Graph Models for System
    Design and Analysis,” 4362:103–10. Springer, 2007. <a href="https://doi.org/10.1007/978-3-540-69507-3_7">https://doi.org/10.1007/978-3-540-69507-3_7</a>.'
  ieee: 'T. A. Henzinger, “Games, time, and probability: Graph models for system design
    and analysis,” presented at the SOFSEM: Current Trends in Theory and Practice
    of Computer Science, 2007, vol. 4362, pp. 103–110.'
  ista: 'Henzinger TA. 2007. Games, time, and probability: Graph models for system
    design and analysis. SOFSEM: Current Trends in Theory and Practice of Computer
    Science, LNCS, vol. 4362, 103–110.'
  mla: 'Henzinger, Thomas A. <i>Games, Time, and Probability: Graph Models for System
    Design and Analysis</i>. Vol. 4362, Springer, 2007, pp. 103–10, doi:<a href="https://doi.org/10.1007/978-3-540-69507-3_7">10.1007/978-3-540-69507-3_7</a>.'
  short: T.A. Henzinger, in:, Springer, 2007, pp. 103–110.
conference:
  name: 'SOFSEM: Current Trends in Theory and Practice of Computer Science'
date_created: 2018-12-11T12:09:15Z
date_published: 2007-01-04T00:00:00Z
date_updated: 2021-01-12T07:59:22Z
day: '04'
doi: 10.1007/978-3-540-69507-3_7
extern: 1
intvolume: '      4362'
month: '01'
page: 103 - 110
publication_status: published
publisher: Springer
publist_id: '217'
quality_controlled: 0
status: public
title: 'Games, time, and probability: Graph models for system design and analysis'
type: conference
volume: 4362
year: '2007'
...
---
_id: '4529'
abstract:
- lang: eng
  text: Computational modeling of biological systems is becoming increasingly important
    in efforts to better understand complex biological behaviors. In this review,
    we distinguish between two types of biological models—mathematical and computational—which
    differ in their representations of biological phenomena. We call the approach
    of constructing computational models of biological systems 'executable biology',
    as it focuses on the design of executable computer algorithms that mimic biological
    phenomena. We survey the main modeling efforts in this direction, emphasize the
    applicability and benefits of executable models in biological research and highlight
    some of the challenges that executable biology poses for biology and computer
    science. We claim that for executable biology to reach its full potential as a
    mainstream biological technique, formal and algorithmic approaches must be integrated
    into biological research. This will drive biology toward a more precise engineering
    discipline.
author:
- first_name: Jasmin
  full_name: Fisher, Jasmin
  last_name: Fisher
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Fisher J, Henzinger TA. Executable cell biology. <i>Nature Biotechnology</i>.
    2007;25:1239-1249. doi:<a href="https://doi.org/10.1038/nbt1356">10.1038/nbt1356</a>
  apa: Fisher, J., &#38; Henzinger, T. A. (2007). Executable cell biology. <i>Nature
    Biotechnology</i>. Nature Publishing Group. <a href="https://doi.org/10.1038/nbt1356">https://doi.org/10.1038/nbt1356</a>
  chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Cell Biology.” <i>Nature
    Biotechnology</i>. Nature Publishing Group, 2007. <a href="https://doi.org/10.1038/nbt1356">https://doi.org/10.1038/nbt1356</a>.
  ieee: J. Fisher and T. A. Henzinger, “Executable cell biology,” <i>Nature Biotechnology</i>,
    vol. 25. Nature Publishing Group, pp. 1239–1249, 2007.
  ista: Fisher J, Henzinger TA. 2007. Executable cell biology. Nature Biotechnology.
    25, 1239–1249.
  mla: Fisher, Jasmin, and Thomas A. Henzinger. “Executable Cell Biology.” <i>Nature
    Biotechnology</i>, vol. 25, Nature Publishing Group, 2007, pp. 1239–49, doi:<a
    href="https://doi.org/10.1038/nbt1356">10.1038/nbt1356</a>.
  short: J. Fisher, T.A. Henzinger, Nature Biotechnology 25 (2007) 1239–1249.
date_created: 2018-12-11T12:09:19Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:28Z
day: '01'
doi: 10.1038/nbt1356
extern: 1
intvolume: '        25'
month: '01'
page: 1239 - 1249
publication: Nature Biotechnology
publication_status: published
publisher: Nature Publishing Group
publist_id: '198'
quality_controlled: 0
status: public
title: Executable cell biology
type: journal_article
volume: 25
year: '2007'
...
---
_id: '4530'
abstract:
- lang: eng
  text: This book constitutes the refereed proceedings of the 21st International Workshop
    on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the
    EACSL in Lausanne, Switzerland. The 36 revised full papers presented together
    with the abstracts of six invited lectures are organized in topical sections on
    logic and games, expressiveness, games and trees, logic and deduction, lambda
    calculus, finite model theory, linear logic, proof theory, and game semantics.
alternative_title:
- LNCS
author:
- first_name: Jacques
  full_name: Duparc, Jacques
  last_name: Duparc
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Duparc J, Henzinger TA. <i>CSL: Computer Science Logic </i>. Vol 4646. Springer;
    2007. doi:<a href="https://doi.org/10.1007/978-3-540-74915-8">10.1007/978-3-540-74915-8</a>'
  apa: 'Duparc, J., &#38; Henzinger, T. A. (2007). <i>CSL: Computer Science Logic
    </i>. <i>CSL: Computer Science Logic</i> (Vol. 4646). Springer. <a href="https://doi.org/10.1007/978-3-540-74915-8">https://doi.org/10.1007/978-3-540-74915-8</a>'
  chicago: 'Duparc, Jacques, and Thomas A Henzinger. <i>CSL: Computer Science Logic
    </i>. <i>CSL: Computer Science Logic</i>. Vol. 4646. Springer, 2007. <a href="https://doi.org/10.1007/978-3-540-74915-8">https://doi.org/10.1007/978-3-540-74915-8</a>.'
  ieee: 'J. Duparc and T. A. Henzinger, <i>CSL: Computer Science Logic </i>, vol.
    4646. Springer, 2007.'
  ista: 'Duparc J, Henzinger TA. 2007. CSL: Computer Science Logic , Springer,p.'
  mla: 'Duparc, Jacques, and Thomas A. Henzinger. “CSL: Computer Science Logic .”
    <i>CSL: Computer Science Logic</i>, vol. 4646, Springer, 2007, doi:<a href="https://doi.org/10.1007/978-3-540-74915-8">10.1007/978-3-540-74915-8</a>.'
  short: 'J. Duparc, T.A. Henzinger, CSL: Computer Science Logic , Springer, 2007.'
date_created: 2018-12-11T12:09:20Z
date_published: 2007-09-01T00:00:00Z
date_updated: 2019-08-02T12:38:32Z
day: '01'
doi: 10.1007/978-3-540-74915-8
extern: 1
intvolume: '      4646'
month: '09'
publication: 'CSL: Computer Science Logic'
publication_status: published
publisher: Springer
publist_id: '194'
quality_controlled: 0
status: public
title: 'CSL: Computer Science Logic '
type: conference_editor
volume: 4646
year: '2007'
...
---
_id: '4531'
abstract:
- lang: eng
  text: Caenorhabditis elegans vulval development provides an important paradigm for
    studying the process of cell fate determination and pattern formation during animal
    development. Although many genes controlling vulval cell fate specification have
    been identified, how they orchestrate themselves to generate a robust and invariant
    pattern of cell fates is not yet completely understood. Here, we have developed
    a dynamic computational model incorporating the current mechanistic understanding
    of gene interactions during this patterning process. A key feature of our model
    is the inclusion of multiple modes of crosstalk between the epidermal growth factor
    receptor (EGFR) and LIN-12/Notch signaling pathways, which together determine
    the fates of the six vulval precursor cells (VPCs). Computational analysis, using
    the model-checking technique, provides new biological insights into the regulatory
    network governing VPC fate specification and predicts novel negative feedback
    loops. In addition, our analysis shows that most mutations affecting vulval development
    lead to stable fate patterns in spite of variations in synchronicity between VPCs.
    Computational searches for the basis of this robustness show that a sequential
    activation of the EGFR-mediated inductive signaling and LIN-12 / Notch-mediated
    lateral signaling pathways is key to achieve a stable cell fate pattern. We demonstrate
    experimentally a time-delay between the activation of the inductive and lateral
    signaling pathways in wild-type animals and the loss of sequential signaling in
    mutants showing unstable fate patterns; thus, validating two key predictions provided
    by our modeling work. The insights gained by our modeling study further substantiate
    the usefulness of executing and analyzing mechanistic models to investigate complex
    biological behaviors.
acknowledgement: This work was supported in part by the Swiss National Science Foundation
  (grant 205321–111840).
author:
- first_name: Jasmin
  full_name: Fisher, Jasmin
  last_name: Fisher
- first_name: Nir
  full_name: Piterman, Nir
  last_name: Piterman
- first_name: Alex
  full_name: Hajnal, Alex
  last_name: Hajnal
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Fisher J, Piterman N, Hajnal A, Henzinger TA. Predictive modeling of signaling
    crosstalk during C. elegans vulval development. <i>PLoS Computational Biology</i>.
    2007;3(5):e92. doi:<a href="https://doi.org/10.1371/journal.pcbi.0030092">10.1371/journal.pcbi.0030092</a>
  apa: Fisher, J., Piterman, N., Hajnal, A., &#38; Henzinger, T. A. (2007). Predictive
    modeling of signaling crosstalk during C. elegans vulval development. <i>PLoS
    Computational Biology</i>. Public Library of Science. <a href="https://doi.org/10.1371/journal.pcbi.0030092">https://doi.org/10.1371/journal.pcbi.0030092</a>
  chicago: Fisher, Jasmin, Nir Piterman, Alex Hajnal, and Thomas A Henzinger. “Predictive
    Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” <i>PLoS
    Computational Biology</i>. Public Library of Science, 2007. <a href="https://doi.org/10.1371/journal.pcbi.0030092">https://doi.org/10.1371/journal.pcbi.0030092</a>.
  ieee: J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger, “Predictive modeling
    of signaling crosstalk during C. elegans vulval development,” <i>PLoS Computational
    Biology</i>, vol. 3(5):e92. Public Library of Science, 2007.
  ista: Fisher J, Piterman N, Hajnal A, Henzinger TA. 2007. Predictive modeling of
    signaling crosstalk during C. elegans vulval development. PLoS Computational Biology.
    3(5):e92.
  mla: Fisher, Jasmin, et al. “Predictive Modeling of Signaling Crosstalk during C.
    Elegans Vulval Development.” <i>PLoS Computational Biology</i>, vol. 3(5):e92,
    Public Library of Science, 2007, doi:<a href="https://doi.org/10.1371/journal.pcbi.0030092">10.1371/journal.pcbi.0030092</a>.
  short: J. Fisher, N. Piterman, A. Hajnal, T.A. Henzinger, PLoS Computational Biology
    3(5):e92 (2007).
date_created: 2018-12-11T12:09:20Z
date_published: 2007-05-18T00:00:00Z
date_updated: 2021-01-12T07:59:29Z
day: '18'
doi: 10.1371/journal.pcbi.0030092
extern: 1
month: '05'
publication: PLoS Computational Biology
publication_status: published
publisher: Public Library of Science
publist_id: '195'
quality_controlled: 0
status: public
title: Predictive modeling of signaling crosstalk during C. elegans vulval development
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
volume: 3(5):e92
year: '2007'
...
---
_id: '4537'
abstract:
- lang: eng
  text: The classical synthesis problem for reactive systems asks, given a proponent
    process A and an opponent process B, to refine A so that the closed-loop system
    A parallel to B satisfies a given specification Phi. The solution of this problem
    requires the computation of a winning strategy for proponent A in a game against
    opponent B. We define and study the co-synthesis problem, where the proponent
    A consists itself of two independent processes, A = A(1)parallel to A(2), with
    specifications Phi(1) and Phi(2), and the goal is to refine both A(1) and A(2)
    so that A(1)parallel to A(2)parallel to B satisfies Phi(1) boolean AND Phi(2).
    For example, if the opponent B is a fair scheduler for the two processes A(1)
    and A(2), and Phi(i) specifies the requirements of mutual exclusion for A(i) (e.g.,
    starvation freedom), then the co-synthesis problem asks for the automatic synthesis
    of a mutual-exclusion protocol. We show that co-synthesis defined classically,
    with the processes A(1) and A(2) either collaborating or competing, does not capture
    desirable solutions. Instead, the proper formulation of co-synthesis is the one
    where process A, competes with A(2) but not at the price of violating Phi(1),
    and vice versa. We call this assume-guarantee synthesis and show that it can be
    solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion
    requirements the assume-guarantee synthesis algorithm automatically computes Peterson's
    protocol.
acknowledgement: This research was supported in part by the Swiss National Science
  Foundation and by the NSF grants CCR-0225610 and CCR-0234690.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Chatterjee K, Henzinger TA. Assume-guarantee synthesis. In: Vol 4424. Springer;
    2007:261-275. doi:<a href="https://doi.org/10.1007/978-3-540-71209-1_21">10.1007/978-3-540-71209-1_21</a>'
  apa: 'Chatterjee, K., &#38; Henzinger, T. A. (2007). Assume-guarantee synthesis
    (Vol. 4424, pp. 261–275). Presented at the TACAS: Tools and Algorithms for the
    Construction and Analysis of Systems, Springer. <a href="https://doi.org/10.1007/978-3-540-71209-1_21">https://doi.org/10.1007/978-3-540-71209-1_21</a>'
  chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Assume-Guarantee Synthesis,”
    4424:261–75. Springer, 2007. <a href="https://doi.org/10.1007/978-3-540-71209-1_21">https://doi.org/10.1007/978-3-540-71209-1_21</a>.
  ieee: 'K. Chatterjee and T. A. Henzinger, “Assume-guarantee synthesis,” presented
    at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
    2007, vol. 4424, pp. 261–275.'
  ista: 'Chatterjee K, Henzinger TA. 2007. Assume-guarantee synthesis. TACAS: Tools
    and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 4424,
    261–275.'
  mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Assume-Guarantee Synthesis</i>.
    Vol. 4424, Springer, 2007, pp. 261–75, doi:<a href="https://doi.org/10.1007/978-3-540-71209-1_21">10.1007/978-3-540-71209-1_21</a>.
  short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2007, pp. 261–275.
conference:
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '01'
doi: 10.1007/978-3-540-71209-1_21
extern: 1
intvolume: '      4424'
month: '01'
page: 261 - 275
publication_status: published
publisher: Springer
publist_id: '186'
quality_controlled: 0
status: public
title: Assume-guarantee synthesis
type: conference
volume: 4424
year: '2007'
...
---
_id: '4547'
abstract:
- lang: eng
  text: We study observation-based strategies for two-player turn-based games on graphs
    with omega-regular objectives. An observation-based strategy relies on imperfect
    information about the history of a play, namely, on the past sequence of observations.
    Such games occur in the synthesis of a controller that does not see the private
    state of the plant. Our main results are twofold. First, we give a fixed-point
    algorithm for computing the set of states from which a player can win with a deterministic
    observation-based strategy for any omega-regular objective. The fixed point is
    computed in the lattice of antichains of state sets. This algorithm has the advantages
    of being directed by the objective and of avoiding an explicit subset construction
    on the game graph. Second, we give an algorithm for computing the set of states
    from which a player can win with probability 1 with a randomized observation-based
    strategy for a Buechi objective. This set is of interest because in the absence
    of perfect information, randomized strategies are more powerful than deterministic
    ones. We show that our algorithms are optimal by proving matching lower bounds.
acknowledgement: This research was supported in part by the NSF grants CCR-0225610
  and CCR-0234690 by the SNSF under the Indo-Swiss Joint Research Programme and by
  the FRFC project “Centre Fédéré en Vérification” funded by the FNRS under grant
  2.4530.02.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  ama: Chatterjee K, Doyen L, Henzinger TA, Raskin J. Algorithms for omega-regular
    games with imperfect information. <i>Logical Methods in Computer Science</i>.
    2007;3(184):1-23. doi:<a href="https://doi.org/10.2168/LMCS-3(3:4)2007">10.2168/LMCS-3(3:4)2007</a>
  apa: Chatterjee, K., Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2007). Algorithms
    for omega-regular games with imperfect information. <i>Logical Methods in Computer
    Science</i>. International Federation of Computational Logic. <a href="https://doi.org/10.2168/LMCS-3(3:4)2007">https://doi.org/10.2168/LMCS-3(3:4)2007</a>
  chicago: Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin.
    “Algorithms for Omega-Regular Games with Imperfect Information.” <i>Logical Methods
    in Computer Science</i>. International Federation of Computational Logic, 2007.
    <a href="https://doi.org/10.2168/LMCS-3(3:4)2007">https://doi.org/10.2168/LMCS-3(3:4)2007</a>.
  ieee: K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Algorithms for omega-regular
    games with imperfect information,” <i>Logical Methods in Computer Science</i>,
    vol. 3, no. 184. International Federation of Computational Logic, pp. 1–23, 2007.
  ista: Chatterjee K, Doyen L, Henzinger TA, Raskin J. 2007. Algorithms for omega-regular
    games with imperfect information. Logical Methods in Computer Science. 3(184),
    1–23.
  mla: Chatterjee, Krishnendu, et al. “Algorithms for Omega-Regular Games with Imperfect
    Information.” <i>Logical Methods in Computer Science</i>, vol. 3, no. 184, International
    Federation of Computational Logic, 2007, pp. 1–23, doi:<a href="https://doi.org/10.2168/LMCS-3(3:4)2007">10.2168/LMCS-3(3:4)2007</a>.
  short: K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, Logical Methods in Computer
    Science 3 (2007) 1–23.
date_created: 2018-12-11T12:09:25Z
date_published: 2007-07-27T00:00:00Z
date_updated: 2021-01-12T07:59:36Z
day: '27'
doi: 10.2168/LMCS-3(3:4)2007
extern: 1
intvolume: '         3'
issue: 184
month: '07'
page: 1 - 23
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '167'
quality_controlled: 0
status: public
title: Algorithms for omega-regular games with imperfect information
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
volume: 3
year: '2007'
...