---
_id: '4368'
alternative_title:
- LNCS
author:
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
citation:
ama: 'Nickovic D, Maler O. AMT: a property-based monitoring tool for analog systems.
In: Springer; 2007:304-319. doi:1567'
apa: 'Nickovic, D., & Maler, O. (2007). AMT: a property-based monitoring tool
for analog systems (pp. 304–319). Presented at the FORMATS: Formal Modeling and
Analysis of Timed Systems, Springer. https://doi.org/1567'
chicago: 'Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool
for Analog Systems,” 304–19. Springer, 2007. https://doi.org/1567.'
ieee: 'D. Nickovic and O. Maler, “AMT: a property-based monitoring tool for analog
systems,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems,
2007, pp. 304–319.'
ista: 'Nickovic D, Maler O. 2007. AMT: a property-based monitoring tool for analog
systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 304–319.'
mla: 'Nickovic, Dejan, and Oded Maler. AMT: A Property-Based Monitoring Tool
for Analog Systems. Springer, 2007, pp. 304–19, doi:1567.'
short: D. Nickovic, O. Maler, in:, Springer, 2007, pp. 304–319.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:30Z
date_published: 2007-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:27Z
day: '20'
doi: '1567'
extern: 1
month: '09'
page: 304 - 319
publication_status: published
publisher: Springer
publist_id: '1089'
quality_controlled: 0
status: public
title: 'AMT: a property-based monitoring tool for analog systems'
type: conference
year: '2007'
...
---
_id: '4370'
alternative_title:
- Lecture Notes in Computer Science
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli,Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. On synthesizing controllers from bounded-response
properties. In: Springer; 2007:95-107. doi:1568'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers
from bounded-response properties (pp. 95–107). Presented at the CAV: Computer
Aided Verification, Springer. https://doi.org/1568'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “On Synthesizing Controllers
from Bounded-Response Properties,” 95–107. Springer, 2007. https://doi.org/1568.
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “On synthesizing controllers from bounded-response
properties,” presented at the CAV: Computer Aided Verification, 2007, pp. 95–107.'
ista: 'Maler O, Nickovic D, Pnueli A. 2007. On synthesizing controllers from bounded-response
properties. CAV: Computer Aided Verification, Lecture Notes in Computer Science,
, 95–107.'
mla: Maler, Oded, et al. On Synthesizing Controllers from Bounded-Response Properties.
Springer, 2007, pp. 95–107, doi:1568.
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2007, pp. 95–107.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:30Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:28Z
day: '01'
doi: '1568'
extern: 1
month: '01'
page: 95 - 107
publication_status: published
publisher: Springer
publist_id: '1086'
quality_controlled: 0
status: public
title: On synthesizing controllers from bounded-response properties
type: conference
year: '2007'
...
---
_id: '4394'
alternative_title:
- LNCS 4349
author:
- first_name: Charles
full_name: Bouillaguet,Charles
last_name: Bouillaguet
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Karen
full_name: Zee,Karen
last_name: Zee
- first_name: Martin
full_name: Rinard,Martin C.
last_name: Rinard
citation:
ama: 'Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. Using First-Order Theorem
Provers in the Jahob Data Structure Verification System. In: Springer; 2007:74-88.
doi:1552'
apa: 'Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using
First-Order Theorem Provers in the Jahob Data Structure Verification System (pp.
74–88). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
Springer. https://doi.org/1552'
chicago: Bouillaguet, Charles, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin
Rinard. “Using First-Order Theorem Provers in the Jahob Data Structure Verification
System,” 74–88. Springer, 2007. https://doi.org/1552.
ieee: 'C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard, “Using First-Order
Theorem Provers in the Jahob Data Structure Verification System,” presented at
the VMCAI: Verification, Model Checking and Abstract Interpretation, 2007, pp.
74–88.'
ista: 'Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. 2007. Using First-Order
Theorem Provers in the Jahob Data Structure Verification System. VMCAI: Verification,
Model Checking and Abstract Interpretation, LNCS 4349, , 74–88.'
mla: Bouillaguet, Charles, et al. Using First-Order Theorem Provers in the Jahob
Data Structure Verification System. Springer, 2007, pp. 74–88, doi:1552.
short: C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 2007,
pp. 74–88.
conference:
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
date_created: 2018-12-11T12:08:37Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:39Z
day: '01'
doi: '1552'
extern: 1
month: '01'
page: 74 - 88
publication_status: published
publisher: Springer
publist_id: '1062'
quality_controlled: 0
status: public
title: Using First-Order Theorem Provers in the Jahob Data Structure Verification
System
type: conference
year: '2007'
...
---
_id: '4398'
alternative_title:
- LNCS 4590
author:
- first_name: Josh
full_name: Berdine,Josh
last_name: Berdine
- first_name: Cristiano
full_name: Calcagno,Cristiano
last_name: Calcagno
- first_name: Byron
full_name: Cook,Byron
last_name: Cook
- first_name: Dino
full_name: Distefano,Dino
last_name: Distefano
- first_name: Peter
full_name: O'Hearn,Peter W.
last_name: O'Hearn
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Hongseok
full_name: Yang,Hongseok
last_name: Yang
citation:
ama: 'Berdine J, Calcagno C, Cook B, et al. Shape Analysis for Composite Data Structures.
In: Springer; 2007:178-192. doi:1553'
apa: 'Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T.,
& Yang, H. (2007). Shape Analysis for Composite Data Structures (pp. 178–192).
Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1553'
chicago: Berdine, Josh, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn,
Thomas Wies, and Hongseok Yang. “Shape Analysis for Composite Data Structures,”
178–92. Springer, 2007. https://doi.org/1553.
ieee: 'J. Berdine et al., “Shape Analysis for Composite Data Structures,”
presented at the CAV: Computer Aided Verification, 2007, pp. 178–192.'
ista: 'Berdine J, Calcagno C, Cook B, Distefano D, O’Hearn P, Wies T, Yang H. 2007.
Shape Analysis for Composite Data Structures. CAV: Computer Aided Verification,
LNCS 4590, , 178–192.'
mla: Berdine, Josh, et al. Shape Analysis for Composite Data Structures.
Springer, 2007, pp. 178–92, doi:1553.
short: J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang,
in:, Springer, 2007, pp. 178–192.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:39Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:40Z
day: '01'
doi: '1553'
extern: 1
month: '01'
page: 178 - 192
publication_status: published
publisher: Springer
publist_id: '1058'
quality_controlled: 0
status: public
title: Shape Analysis for Composite Data Structures
type: conference
year: '2007'
...
---
_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:10.1007/978-3-540-73368-3_4'
apa: 'Beyer, D., Henzinger, T. A., & Singh, V. (2007). Algorithms for interface
synthesis (Vol. 4590, pp. 4–19). Presented at the CAV: Computer Aided Verification,
Springer. https://doi.org/10.1007/978-3-540-73368-3_4'
chicago: Beyer, Dirk, Thomas A Henzinger, and Vasu Singh. “Algorithms for Interface
Synthesis,” 4590:4–19. Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_4.
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. Algorithms for Interface Synthesis. Vol. 4590, Springer,
2007, pp. 4–19, doi:10.1007/978-3-540-73368-3_4.
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:1544'
apa: 'Alur, R., Cerny, P., & 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. https://doi.org/1544'
chicago: Alur, Rajeev, Pavol Cerny, and Swarat Chaudhuri. “Model Checking on Trees
with Path Equivalences,” 664–78. Springer, 2007. https://doi.org/1544.
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. Model Checking on Trees with Path Equivalences.
Springer, 2007, pp. 664–78, doi:1544.
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. BMC Systems Biology. 2007;1(4).
doi:10.1186/1752-0509-1-4'
apa: 'Schaub, M., Henzinger, T. A., & Fisher, J. (2007). Qualitative networks:
A symbolic approach to analyze biological signaling networks. BMC Systems Biology.
BioMed Central. https://doi.org/10.1186/1752-0509-1-4'
chicago: 'Schaub, Marc, Thomas A Henzinger, and Jasmin Fisher. “Qualitative Networks:
A Symbolic Approach to Analyze Biological Signaling Networks.” BMC Systems
Biology. BioMed Central, 2007. https://doi.org/10.1186/1752-0509-1-4.'
ieee: 'M. Schaub, T. A. Henzinger, and J. Fisher, “Qualitative networks: A symbolic
approach to analyze biological signaling networks,” BMC Systems Biology,
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.” BMC Systems Biology, vol. 1, no. 4, BioMed
Central, 2007, doi:10.1186/1752-0509-1-4.'
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: Program Analysis and Compilation, Theory
and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th
Birthday. Vol 4444. Springer; 2007:273-292. doi:10.1007/978-3-540-71322-7_13'
apa: 'Manevich, R., Field, J., Henzinger, T. A., 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 (Vol. 4444, pp. 273–292). Springer. https://doi.org/10.1007/978-3-540-71322-7_13'
chicago: 'Manevich, Roman, John Field, Thomas A Henzinger, Ganesan Ramalingam, and
Mooly Sagiv. “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, 4444:273–92. Springer,
2007. https://doi.org/10.1007/978-3-540-71322-7_13.'
ieee: 'R. Manevich, J. Field, T. A. Henzinger, G. Ramalingam, and M. Sagiv, “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, 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.” Program Analysis and Compilation, Theory and Practice: Essays Dedicated
to Reinhard Wilhelm on the Occasion of His 60th Birthday, vol. 4444, Springer,
2007, pp. 273–92, doi:10.1007/978-3-540-71322-7_13.'
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. ACM Transactions on Programming Languages and Systems (TOPLAS). 2007;29(393).
doi:10.1145/1286821.1286824'
apa: 'Henzinger, T. A., & Kirsch, C. (2007). The embedded machine: Predictable,
portable real-time code. ACM Transactions on Programming Languages and Systems
(TOPLAS). ACM. https://doi.org/10.1145/1286821.1286824'
chicago: 'Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable,
Portable Real-Time Code.” ACM Transactions on Programming Languages and Systems
(TOPLAS). ACM, 2007. https://doi.org/10.1145/1286821.1286824.'
ieee: 'T. A. Henzinger and C. Kirsch, “The embedded machine: Predictable, portable
real-time code,” ACM Transactions on Programming Languages and Systems (TOPLAS),
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.” ACM Transactions on Programming Languages and Systems
(TOPLAS), vol. 29, no. 393, ACM, 2007, doi:10.1145/1286821.1286824.'
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:10.1007/978-3-540-73208-2_2'
apa: 'Henzinger, T. A. (2007). Quantitative generalizations of languages (Vol. 4588,
pp. 20–22). Presented at the DLT: Developments in Language Theory, Springer. https://doi.org/10.1007/978-3-540-73208-2_2'
chicago: Henzinger, Thomas A. “Quantitative Generalizations of Languages,” 4588:20–22.
Springer, 2007. https://doi.org/10.1007/978-3-540-73208-2_2.
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. Quantitative Generalizations of Languages. Vol.
4588, Springer, 2007, pp. 20–22, doi:10.1007/978-3-540-73208-2_2.
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:10.1007/978-3-540-69507-3_7'
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. https://doi.org/10.1007/978-3-540-69507-3_7'
chicago: 'Henzinger, Thomas A. “Games, Time, and Probability: Graph Models for System
Design and Analysis,” 4362:103–10. Springer, 2007. https://doi.org/10.1007/978-3-540-69507-3_7.'
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. Games, Time, and Probability: Graph Models for System
Design and Analysis. Vol. 4362, Springer, 2007, pp. 103–10, doi:10.1007/978-3-540-69507-3_7.'
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. Nature Biotechnology.
2007;25:1239-1249. doi:10.1038/nbt1356
apa: Fisher, J., & Henzinger, T. A. (2007). Executable cell biology. Nature
Biotechnology. Nature Publishing Group. https://doi.org/10.1038/nbt1356
chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Cell Biology.” Nature
Biotechnology. Nature Publishing Group, 2007. https://doi.org/10.1038/nbt1356.
ieee: J. Fisher and T. A. Henzinger, “Executable cell biology,” Nature Biotechnology,
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.” Nature
Biotechnology, vol. 25, Nature Publishing Group, 2007, pp. 1239–49, doi:10.1038/nbt1356.
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. CSL: Computer Science Logic . Vol 4646. Springer;
2007. doi:10.1007/978-3-540-74915-8'
apa: 'Duparc, J., & Henzinger, T. A. (2007). CSL: Computer Science Logic
. CSL: Computer Science Logic (Vol. 4646). Springer. https://doi.org/10.1007/978-3-540-74915-8'
chicago: 'Duparc, Jacques, and Thomas A Henzinger. CSL: Computer Science Logic
. CSL: Computer Science Logic. Vol. 4646. Springer, 2007. https://doi.org/10.1007/978-3-540-74915-8.'
ieee: 'J. Duparc and T. A. Henzinger, CSL: Computer Science Logic , 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 .”
CSL: Computer Science Logic, vol. 4646, Springer, 2007, doi:10.1007/978-3-540-74915-8.'
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. PLoS Computational Biology.
2007;3(5):e92. doi:10.1371/journal.pcbi.0030092
apa: Fisher, J., Piterman, N., Hajnal, A., & Henzinger, T. A. (2007). Predictive
modeling of signaling crosstalk during C. elegans vulval development. PLoS
Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.0030092
chicago: Fisher, Jasmin, Nir Piterman, Alex Hajnal, and Thomas A Henzinger. “Predictive
Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” PLoS
Computational Biology. Public Library of Science, 2007. https://doi.org/10.1371/journal.pcbi.0030092.
ieee: J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger, “Predictive modeling
of signaling crosstalk during C. elegans vulval development,” PLoS Computational
Biology, 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.” PLoS Computational Biology, vol. 3(5):e92,
Public Library of Science, 2007, doi:10.1371/journal.pcbi.0030092.
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:10.1007/978-3-540-71209-1_21'
apa: 'Chatterjee, K., & 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. https://doi.org/10.1007/978-3-540-71209-1_21'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Assume-Guarantee Synthesis,”
4424:261–75. Springer, 2007. https://doi.org/10.1007/978-3-540-71209-1_21.
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. Assume-Guarantee Synthesis.
Vol. 4424, Springer, 2007, pp. 261–75, doi:10.1007/978-3-540-71209-1_21.
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. Logical Methods in Computer Science.
2007;3(184):1-23. doi:10.2168/LMCS-3(3:4)2007
apa: Chatterjee, K., Doyen, L., Henzinger, T. A., & Raskin, J. (2007). Algorithms
for omega-regular games with imperfect information. Logical Methods in Computer
Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-3(3:4)2007
chicago: Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin.
“Algorithms for Omega-Regular Games with Imperfect Information.” Logical Methods
in Computer Science. International Federation of Computational Logic, 2007.
https://doi.org/10.2168/LMCS-3(3:4)2007.
ieee: K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Algorithms for omega-regular
games with imperfect information,” Logical Methods in Computer Science,
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.” Logical Methods in Computer Science, vol. 3, no. 184, International
Federation of Computational Logic, 2007, pp. 1–23, doi:10.2168/LMCS-3(3:4)2007.
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'
...
---
_id: '2657'
abstract:
- lang: eng
text: The highest densities of the two metabotropic GABA subunits, GABA B1 and GABAB2,
have been reported as occurring around the glutamatergic synapses between Purkinje
cell spines and parallel fibre varicosities. In order to determine how this distribution
is achieved during development, we investigated the expression pattern and the
cellular and subcellular localization of the GABAB1 and GABAB2 subunits in the
rat cerebellum during postnatal development. At the light microscopic level, immunoreactivity
for the GABAB1 and GABAB2 subunits was very prominent in the developing molecular
layer, especially in Purkinje cells. Using double immunofluorescence, we demonstrated
that GABAB1 was transiently expressed in glial cells. At the electron microscopic
level, immunoreactivity for GABAB receptors was always detected both pre- and
postsynaptically. Presynaptically, GABAB1 and GABAB2 were localized in the extrasynaptic
membrane of parallel fibres at all ages, and only rarely in GABAergic axons. Postsynaptically,
GABAB receptors were localized to the extrasynaptic and perisynaptic plasma membrane
of Purkinje cell dendrites and spines throughout development. Quantitative analysis
and three-dimensional reconstructions further revealed a progressive developmental
movement of the GABAB1 subunit on the surface of Purkinje cells from dendritic
shafts to its final destination, the dendritic spines. Together, these results
indicate that GABAB receptors undergo dynamic regulation during cerebellar development
in association with the establishment and maturation of glutamatergic synapses
to Purkinje cells.
author:
- first_name: Rafael
full_name: Luján, Rafael
last_name: Luján
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
citation:
ama: Luján R, Shigemoto R. Localization of metabotropic GABA receptor subunits GABAB1
and GABAB2 relative to synaptic sites in the rat developing cerebellum. European
Journal of Neuroscience. 2006;23(6):1479-1490. doi:10.1111/j.1460-9568.2006.04669.x
apa: Luján, R., & Shigemoto, R. (2006). Localization of metabotropic GABA receptor
subunits GABAB1 and GABAB2 relative to synaptic sites in the rat developing cerebellum.
European Journal of Neuroscience. Wiley-Blackwell. https://doi.org/10.1111/j.1460-9568.2006.04669.x
chicago: Luján, Rafael, and Ryuichi Shigemoto. “Localization of Metabotropic GABA
Receptor Subunits GABAB1 and GABAB2 Relative to Synaptic Sites in the Rat Developing
Cerebellum.” European Journal of Neuroscience. Wiley-Blackwell, 2006. https://doi.org/10.1111/j.1460-9568.2006.04669.x.
ieee: R. Luján and R. Shigemoto, “Localization of metabotropic GABA receptor subunits
GABAB1 and GABAB2 relative to synaptic sites in the rat developing cerebellum,”
European Journal of Neuroscience, vol. 23, no. 6. Wiley-Blackwell, pp.
1479–1490, 2006.
ista: Luján R, Shigemoto R. 2006. Localization of metabotropic GABA receptor subunits
GABAB1 and GABAB2 relative to synaptic sites in the rat developing cerebellum.
European Journal of Neuroscience. 23(6), 1479–1490.
mla: Luján, Rafael, and Ryuichi Shigemoto. “Localization of Metabotropic GABA Receptor
Subunits GABAB1 and GABAB2 Relative to Synaptic Sites in the Rat Developing Cerebellum.”
European Journal of Neuroscience, vol. 23, no. 6, Wiley-Blackwell, 2006,
pp. 1479–90, doi:10.1111/j.1460-9568.2006.04669.x.
short: R. Luján, R. Shigemoto, European Journal of Neuroscience 23 (2006) 1479–1490.
date_created: 2018-12-11T11:58:54Z
date_published: 2006-03-01T00:00:00Z
date_updated: 2021-01-12T06:58:52Z
day: '01'
doi: 10.1111/j.1460-9568.2006.04669.x
extern: 1
intvolume: ' 23'
issue: '6'
month: '03'
page: 1479 - 1490
publication: European Journal of Neuroscience
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4239'
quality_controlled: 0
status: public
title: Localization of metabotropic GABA receptor subunits GABAB1 and GABAB2 relative
to synaptic sites in the rat developing cerebellum
type: journal_article
volume: 23
year: '2006'
...
---
_id: '2659'
abstract:
- lang: eng
text: Transmembrane AMPA receptor regulatory proteins (TARPs), including stargazin/γ-2,
are associated with AMPA receptors and participate in their surface delivery and
anchoring at the postsynaptic membrane. TARPs may also act as a positive modulator
of the AMPA receptor ion channel function; however, little is known about other
TARP members except for stargazin/γ-2. We examined the synaptic localization of
stargazin/γ-2 and γ-8 by immunoelectron microscopy and biochemical analysis. The
analysis of sodium dodecyl sulfate-digested freeze-fracture replica labeling revealed
that stargazin/γ-2 was concentrated in the postsynaptic area, whereas γ-8 was
distributed both in synaptic and extra-synaptic plasma membranes of the hippocampal
neuron. When a synaptic plasma membrane-enriched brain fraction was treated with
Triton X-100 and separated by sucrose density gradient ultracentrifugation, a
large proportion of NMDA receptor and stargazin/γ-2 was accumulated in raft-enriched
fractions, whereas AMPA receptor and γ-8 were distributed in both the raft-enriched
fractions and other Triton-insoluble fractions. Phosphorylation of stargazin/γ-2
and γ-8 was regulated by different sets of kinases and phosphatases in cultured
cortical neurons. These results suggested that stargazin/γ-2 and γ-8 have distinct
roles in postsynaptic membranes under the regulation of different intracellular
signaling pathways.
author:
- first_name: Mihoko
full_name: Inamura, Mihoko
last_name: Inamura
- first_name: Makoto
full_name: Itakura, Makoto
last_name: Itakura
- first_name: Hirotsugu
full_name: Okamoto, Hirotsugu
last_name: Okamoto
- first_name: Sumio
full_name: Hoka, Sumio
last_name: Hoka
- first_name: Akira
full_name: Mizoguchi, Akira
last_name: Mizoguchi
- first_name: Yugo
full_name: Fukazawa, Yugo
last_name: Fukazawa
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Saori
full_name: Yamamori, Saori
last_name: Yamamori
- first_name: Masami
full_name: Takahashi, Masami
last_name: Takahashi
citation:
ama: Inamura M, Itakura M, Okamoto H, et al. Differential localization and regulation
of stargazin-like protein, γ-8 and stargazin in the plasma membrane of hippocampal
and cortical neurons. Neuroscience Research. 2006;55(1):45-53. doi:10.1016/j.neures.2006.01.004
apa: Inamura, M., Itakura, M., Okamoto, H., Hoka, S., Mizoguchi, A., Fukazawa, Y.,
… Takahashi, M. (2006). Differential localization and regulation of stargazin-like
protein, γ-8 and stargazin in the plasma membrane of hippocampal and cortical
neurons. Neuroscience Research. Elsevier. https://doi.org/10.1016/j.neures.2006.01.004
chicago: Inamura, Mihoko, Makoto Itakura, Hirotsugu Okamoto, Sumio Hoka, Akira Mizoguchi,
Yugo Fukazawa, Ryuichi Shigemoto, Saori Yamamori, and Masami Takahashi. “ Differential
Localization and Regulation of Stargazin-like Protein, γ-8 and Stargazin in the
Plasma Membrane of Hippocampal and Cortical Neurons.” Neuroscience Research.
Elsevier, 2006. https://doi.org/10.1016/j.neures.2006.01.004.
ieee: M. Inamura et al., “ Differential localization and regulation of stargazin-like
protein, γ-8 and stargazin in the plasma membrane of hippocampal and cortical
neurons,” Neuroscience Research, vol. 55, no. 1. Elsevier, pp. 45–53, 2006.
ista: Inamura M, Itakura M, Okamoto H, Hoka S, Mizoguchi A, Fukazawa Y, Shigemoto
R, Yamamori S, Takahashi M. 2006. Differential localization and regulation of
stargazin-like protein, γ-8 and stargazin in the plasma membrane of hippocampal
and cortical neurons. Neuroscience Research. 55(1), 45–53.
mla: Inamura, Mihoko, et al. “ Differential Localization and Regulation of Stargazin-like
Protein, γ-8 and Stargazin in the Plasma Membrane of Hippocampal and Cortical
Neurons.” Neuroscience Research, vol. 55, no. 1, Elsevier, 2006, pp. 45–53,
doi:10.1016/j.neures.2006.01.004.
short: M. Inamura, M. Itakura, H. Okamoto, S. Hoka, A. Mizoguchi, Y. Fukazawa, R.
Shigemoto, S. Yamamori, M. Takahashi, Neuroscience Research 55 (2006) 45–53.
date_created: 2018-12-11T11:58:55Z
date_published: 2006-05-01T00:00:00Z
date_updated: 2021-01-12T06:58:52Z
day: '01'
doi: 10.1016/j.neures.2006.01.004
extern: 1
intvolume: ' 55'
issue: '1'
month: '05'
page: 45 - 53
publication: Neuroscience Research
publication_status: published
publisher: Elsevier
publist_id: '4238'
quality_controlled: 0
status: public
title: ' Differential localization and regulation of stargazin-like protein, γ-8 and
stargazin in the plasma membrane of hippocampal and cortical neurons'
type: journal_article
volume: 55
year: '2006'
...
---
_id: '2660'
abstract:
- lang: eng
text: Pavlovian fear conditioning, a simple form of associative learning, is thought
to involve the induction of associative, NMDA receptor-dependent long-term potentiation
(LTP) in the lateral amygdala. Using a combined genetic and electrophysiological
approach, we show here that lack of a specific GABAB receptor subtype, GABAB(1a,2),
unmasks a nonassociative, NMDA receptor-independent form of presynaptic LTP at
cortico-amygdala afferents. Moreover, the level of presynaptic GABA B(1a,2) receptor
activation, and hence the balance between associative and nonassociative forms
of LTP, can be dynamically modulated by local inhibitory activity. At the behavioral
level, genetic loss of GABA B(1a) results in a generalization of conditioned fear
to nonconditioned stimuli. Our findings indicate that presynaptic inhibition through
GABAB(1a,2) receptors serves as an activity-dependent constraint on the induction
of homosynaptic plasticity, which may be important to prevent the generalization
of conditioned fear.
author:
- first_name: Hamdy
full_name: Shaban, Hamdy
last_name: Shaban
- first_name: Yann
full_name: Humeau, Yann
last_name: Humeau
- first_name: Cyril
full_name: Herry, Cyril
last_name: Herry
- first_name: Guillaume
full_name: Cassasus, Guillaume
last_name: Cassasus
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Stéphane
full_name: Ciocchi, Stéphane
last_name: Ciocchi
- first_name: Samuel
full_name: Barbieri, Samuel
last_name: Barbieri
- first_name: Herman
full_name: Van Der Putten, Herman V
last_name: Van Der Putten
- first_name: Klemens
full_name: Kaupmann, Klemens
last_name: Kaupmann
- first_name: Bernhard
full_name: Bettler, Bernhard
last_name: Bettler
- first_name: Andreas
full_name: Lüthi, Andreas
last_name: Lüthi
citation:
ama: Shaban H, Humeau Y, Herry C, et al. Generalization of amygdala LTP and conditioned
fear in the absence of presynaptic inhibition. Nature Neuroscience. 2006;9(8):1028-1035.
doi:10.1038/nn1732
apa: Shaban, H., Humeau, Y., Herry, C., Cassasus, G., Shigemoto, R., Ciocchi, S.,
… Lüthi, A. (2006). Generalization of amygdala LTP and conditioned fear in the
absence of presynaptic inhibition. Nature Neuroscience. Nature Publishing
Group. https://doi.org/10.1038/nn1732
chicago: Shaban, Hamdy, Yann Humeau, Cyril Herry, Guillaume Cassasus, Ryuichi Shigemoto,
Stéphane Ciocchi, Samuel Barbieri, et al. “Generalization of Amygdala LTP and
Conditioned Fear in the Absence of Presynaptic Inhibition.” Nature Neuroscience.
Nature Publishing Group, 2006. https://doi.org/10.1038/nn1732.
ieee: H. Shaban et al., “Generalization of amygdala LTP and conditioned fear
in the absence of presynaptic inhibition,” Nature Neuroscience, vol. 9,
no. 8. Nature Publishing Group, pp. 1028–1035, 2006.
ista: Shaban H, Humeau Y, Herry C, Cassasus G, Shigemoto R, Ciocchi S, Barbieri
S, Van Der Putten H, Kaupmann K, Bettler B, Lüthi A. 2006. Generalization of amygdala
LTP and conditioned fear in the absence of presynaptic inhibition. Nature Neuroscience.
9(8), 1028–1035.
mla: Shaban, Hamdy, et al. “Generalization of Amygdala LTP and Conditioned Fear
in the Absence of Presynaptic Inhibition.” Nature Neuroscience, vol. 9,
no. 8, Nature Publishing Group, 2006, pp. 1028–35, doi:10.1038/nn1732.
short: H. Shaban, Y. Humeau, C. Herry, G. Cassasus, R. Shigemoto, S. Ciocchi, S.
Barbieri, H. Van Der Putten, K. Kaupmann, B. Bettler, A. Lüthi, Nature Neuroscience
9 (2006) 1028–1035.
date_created: 2018-12-11T11:58:55Z
date_published: 2006-08-01T00:00:00Z
date_updated: 2021-01-12T06:58:53Z
day: '01'
doi: 10.1038/nn1732
extern: 1
intvolume: ' 9'
issue: '8'
month: '08'
page: 1028 - 1035
publication: Nature Neuroscience
publication_status: published
publisher: Nature Publishing Group
publist_id: '4236'
quality_controlled: 0
status: public
title: Generalization of amygdala LTP and conditioned fear in the absence of presynaptic
inhibition
type: journal_article
volume: 9
year: '2006'
...
---
_id: '2661'
abstract:
- lang: eng
text: GABAB receptors are the G protein-coupled receptors for the main inhibitory
neurotransmitter in the brain, γ-aminobutyric acid (GABA). Molecular diversity
in the GABAB system arises from the GABAB1a and GABAB1b subunit isoforms that
solely differ in their ectodomains by a pair of sushi repeats that is unique to
GABAB1a. Using a combined genetic, physiological, and morphological approach,
we now demonstrate that GABAB1 isoforms localize to distinct synaptic sites and
convey separate functions in vivo. At hippocampal CA3-to-CA1 synapses, GABAB1a
assembles heteroreceptors inhibiting glutamate release, while predominantly GABAB1b
mediates postsynaptic inhibition. Electron microscopy reveals a synaptic distribution
of GABAB1 isoforms that agrees with the observed functional differences. Transfected
CA3 neurons selectively express GABAB1a in distal axons, suggesting that the sushi
repeats, a conserved protein interaction motif, specify heteroreceptor localization.
The constitutive absence of GABAB1a but not GABAB1b results in impaired synaptic
plasticity and hippocampus-dependent memory, emphasizing molecular differences
in synaptic GABAB functions.
author:
- first_name: Réjan
full_name: Vigot, Réjan
last_name: Vigot
- first_name: Samuel
full_name: Barbieri, Samuel
last_name: Barbieri
- first_name: Hans
full_name: Bräuner-Osborne, Hans
last_name: Bräuner Osborne
- first_name: Rostislav
full_name: Tureček, Rostislav
last_name: Tureček
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Yan
full_name: Zhang, Yan Ping
last_name: Zhang
- first_name: Rafael
full_name: Luján, Rafael
last_name: Luján
- first_name: Laura
full_name: Jacobson, Laura H
last_name: Jacobson
- first_name: Barbara
full_name: Biermann, Barbara
last_name: Biermann
- first_name: Jean
full_name: Fritschy, Jean-Marc
last_name: Fritschy
- first_name: Claire
full_name: Vacher, Claire-Marie
last_name: Vacher
- first_name: Matthias
full_name: Müller, Matthias P
last_name: Müller
- first_name: Gilles
full_name: Sansig, Gilles
last_name: Sansig
- first_name: Nicole
full_name: Guetg, Nicole
last_name: Guetg
- first_name: John
full_name: Cryan, John F
last_name: Cryan
- first_name: Klemens
full_name: Kaupmann, Klemens
last_name: Kaupmann
- first_name: Martin
full_name: Gassmann, Martin
last_name: Gassmann
- first_name: Thomas
full_name: Oertner, Thomas G
last_name: Oertner
- first_name: Bernhard
full_name: Bettler, Bernhard
last_name: Bettler
citation:
ama: Vigot R, Barbieri S, Bräuner Osborne H, et al. Differential Compartmentalization
and Distinct Functions of GABAB Receptor Variants. Neuron. 2006;50(4):589-601.
doi:10.1016/j.neuron.2006.04.014
apa: Vigot, R., Barbieri, S., Bräuner Osborne, H., Tureček, R., Shigemoto, R., Zhang,
Y., … Bettler, B. (2006). Differential Compartmentalization and Distinct Functions
of GABAB Receptor Variants. Neuron. Elsevier. https://doi.org/10.1016/j.neuron.2006.04.014
chicago: Vigot, Réjan, Samuel Barbieri, Hans Bräuner Osborne, Rostislav Tureček,
Ryuichi Shigemoto, Yan Zhang, Rafael Luján, et al. “Differential Compartmentalization
and Distinct Functions of GABAB Receptor Variants.” Neuron. Elsevier, 2006.
https://doi.org/10.1016/j.neuron.2006.04.014.
ieee: R. Vigot et al., “Differential Compartmentalization and Distinct Functions
of GABAB Receptor Variants,” Neuron, vol. 50, no. 4. Elsevier, pp. 589–601,
2006.
ista: Vigot R, Barbieri S, Bräuner Osborne H, Tureček R, Shigemoto R, Zhang Y, Luján
R, Jacobson L, Biermann B, Fritschy J, Vacher C, Müller M, Sansig G, Guetg N,
Cryan J, Kaupmann K, Gassmann M, Oertner T, Bettler B. 2006. Differential Compartmentalization
and Distinct Functions of GABAB Receptor Variants. Neuron. 50(4), 589–601.
mla: Vigot, Réjan, et al. “Differential Compartmentalization and Distinct Functions
of GABAB Receptor Variants.” Neuron, vol. 50, no. 4, Elsevier, 2006, pp.
589–601, doi:10.1016/j.neuron.2006.04.014.
short: R. Vigot, S. Barbieri, H. Bräuner Osborne, R. Tureček, R. Shigemoto, Y. Zhang,
R. Luján, L. Jacobson, B. Biermann, J. Fritschy, C. Vacher, M. Müller, G. Sansig,
N. Guetg, J. Cryan, K. Kaupmann, M. Gassmann, T. Oertner, B. Bettler, Neuron 50
(2006) 589–601.
date_created: 2018-12-11T11:58:56Z
date_published: 2006-05-18T00:00:00Z
date_updated: 2021-01-12T06:58:54Z
day: '18'
doi: 10.1016/j.neuron.2006.04.014
extern: 1
intvolume: ' 50'
issue: '4'
month: '05'
page: 589 - 601
publication: Neuron
publication_status: published
publisher: Elsevier
publist_id: '4237'
quality_controlled: 0
status: public
title: Differential Compartmentalization and Distinct Functions of GABAB Receptor
Variants
type: journal_article
volume: 50
year: '2006'
...