---
_id: '4462'
abstract:
- lang: eng
text: 'A major hurdle in the algorithmic verification and control of systems is
the need to find suitable abstract models, which omit enough details to overcome
the state-explosion problem, but retain enough details to exhibit satisfaction
or controllability with respect to the specification. The paradigm of counterexample-guided
abstraction refinement suggests a fully automatic way of finding suitable abstract
models: one starts with a coarse abstraction, attempts to verify or control the
abstract model, and if this attempt fails and the abstract counterexample does
not correspond to a concrete counterexample, then one uses the spurious counterexample
to guide the refinement of the abstract model. We present a counterexample-guided
refinement algorithm for solving ω-regular control objectives. The main difficulty
is that in control, unlike in verification, counterexamples are strategies in
a game between system and controller. In the case that the controller has no choices,
our scheme subsumes known counterexample-guided refinement algorithms for the
verification of ω-regular specifications. Our algorithm is useful in all situations
where ω-regular games need to be solved, such as supervisory control, sequential
and program synthesis, and modular verification. The algorithm is fully symbolic,
and therefore applicable also to infinite-state systems.'
acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614,
the ONR grant N00014-02-1-0671, and the NSF grants CCR-9988172, CCR-0085949, and
CCR-0225610.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R. Counterexample-guided control. In: Proceedings
of the 30th International Colloquium on Automata, Languages and Programming.
Vol 2719. Springer; 2003:886-902. doi:10.1007/3-540-45061-0_69'
apa: 'Henzinger, T. A., Jhala, R., & Majumdar, R. (2003). Counterexample-guided
control. In Proceedings of the 30th International Colloquium on Automata, Languages
and Programming (Vol. 2719, pp. 886–902). Eindhoven, The Netherlands: Springer.
https://doi.org/10.1007/3-540-45061-0_69'
chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Counterexample-Guided
Control.” In Proceedings of the 30th International Colloquium on Automata,
Languages and Programming, 2719:886–902. Springer, 2003. https://doi.org/10.1007/3-540-45061-0_69.
ieee: T. A. Henzinger, R. Jhala, and R. Majumdar, “Counterexample-guided control,”
in Proceedings of the 30th International Colloquium on Automata, Languages
and Programming, Eindhoven, The Netherlands, 2003, vol. 2719, pp. 886–902.
ista: 'Henzinger TA, Jhala R, Majumdar R. 2003. Counterexample-guided control. Proceedings
of the 30th International Colloquium on Automata, Languages and Programming. ICALP:
Automata, Languages and Programming, LNCS, vol. 2719, 886–902.'
mla: Henzinger, Thomas A., et al. “Counterexample-Guided Control.” Proceedings
of the 30th International Colloquium on Automata, Languages and Programming,
vol. 2719, Springer, 2003, pp. 886–902, doi:10.1007/3-540-45061-0_69.
short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 30th International
Colloquium on Automata, Languages and Programming, Springer, 2003, pp. 886–902.
conference:
end_date: 2003-07-04
location: Eindhoven, The Netherlands
name: 'ICALP: Automata, Languages and Programming'
start_date: 2003-06-30
date_created: 2018-12-11T12:08:58Z
date_published: 2003-06-25T00:00:00Z
date_updated: 2024-01-10T11:19:41Z
day: '25'
doi: 10.1007/3-540-45061-0_69
extern: '1'
intvolume: ' 2719'
language:
- iso: eng
month: '06'
oa_version: None
page: 886 - 902
publication: Proceedings of the 30th International Colloquium on Automata, Languages
and Programming
publication_identifier:
isbn:
- '9783540404934'
publication_status: published
publisher: Springer
publist_id: '265'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Counterexample-guided control
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2719
year: '2003'
...
---
_id: '4463'
abstract:
- lang: eng
text: We present an algorithm called TAR (“Thread-modular Abstraction Refinement”)
for model checking safety properties of concurrent software. The TAR algorithm
uses thread-modular assume-guarantee reasoning to overcome the exponential complexity
in the control state of multithreaded programs. Thread modularity means that TAR
explores the state space of one thread at a time, making assumptions about how
the environment can interfere. The TAR algorithm uses counterexample-guided predicate-abstraction
refinement to overcome the usually infinite complexity in the data state of C
programs. A successive approximation scheme automatically infers the necessary
precision on data variables as well as suitable environment assumptions. The scheme
is novel in that transition relations are approximated from above, while at the
same time environment assumptions are approximated from below. In our software
verification tool BLAST we have implemented a fully automatic race checker for
multithreaded C programs which is based on the TAR algorithm. This tool has verified
a wide variety of commonly used locking idioms, including locking schemes that
are not amenable to existing dynamic and static race checkers such as ERASER or
WARLOCK.
acknowledgement: This work was supported in part by the NSF grants CCR-0085949 and
CCR-0234690, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Qadeer S. Thread-modular abstraction refinement.
In: Proceedings of the 15th International Conference on Computer Aided Verification.
Vol 2725. Springer; 2003:262-274. doi:10.1007/978-3-540-45069-6_27'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Qadeer, S. (2003). Thread-modular
abstraction refinement. In Proceedings of the 15th International Conference
on Computer Aided Verification (Vol. 2725, pp. 262–274). Boulder, CO, USA:
Springer. https://doi.org/10.1007/978-3-540-45069-6_27'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Shaz Qadeer.
“Thread-Modular Abstraction Refinement.” In Proceedings of the 15th International
Conference on Computer Aided Verification, 2725:262–74. Springer, 2003. https://doi.org/10.1007/978-3-540-45069-6_27.
ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer, “Thread-modular abstraction
refinement,” in Proceedings of the 15th International Conference on Computer
Aided Verification, Boulder, CO, USA, 2003, vol. 2725, pp. 262–274.
ista: 'Henzinger TA, Jhala R, Majumdar R, Qadeer S. 2003. Thread-modular abstraction
refinement. Proceedings of the 15th International Conference on Computer Aided
Verification. CAV: Computer Aided Verification, LNCS, vol. 2725, 262–274.'
mla: Henzinger, Thomas A., et al. “Thread-Modular Abstraction Refinement.” Proceedings
of the 15th International Conference on Computer Aided Verification, vol.
2725, Springer, 2003, pp. 262–74, doi:10.1007/978-3-540-45069-6_27.
short: T.A. Henzinger, R. Jhala, R. Majumdar, S. Qadeer, in:, Proceedings of the
15th International Conference on Computer Aided Verification, Springer, 2003,
pp. 262–274.
conference:
end_date: 2003-07-12
location: Boulder, CO, USA
name: 'CAV: Computer Aided Verification'
start_date: 2003-07-08
date_created: 2018-12-11T12:08:59Z
date_published: 2003-06-27T00:00:00Z
date_updated: 2024-01-10T11:05:53Z
day: '27'
doi: 10.1007/978-3-540-45069-6_27
extern: '1'
intvolume: ' 2725'
language:
- iso: eng
month: '06'
oa_version: None
page: 262 - 274
publication: Proceedings of the 15th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540405245'
publication_status: published
publisher: Springer
publist_id: '266'
quality_controlled: '1'
status: public
title: Thread-modular abstraction refinement
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2725
year: '2003'
...
---
_id: '4464'
abstract:
- lang: eng
text: We introduce the paradigm of schedule-carrying code (SCC). A hard real-time
program can be executed on a given platform only if there exists a feasible schedule
for the real-time tasks of the program. Traditionally, a scheduler determines
the existence of a feasible schedule according to some scheduling strategy. With
SCC, a compiler proves the existence of a feasible schedule by generating executable
code that is attached to the program and represents its schedule. An SCC executable
is a real-time program that carries its schedule as code, which is produced once
and can be revalidated and executed with each use. We evaluate SCC both in theory
and practice. In theory, we give two scenarios, of nonpreemptive and distributed
scheduling for Giotto programs, where the generation of a feasible schedule is
hard, while the validation of scheduling instructions that are attached to the
programs is easy. In practice, we implement SCC and show that explicit scheduling
instructions can reduce the scheduling overhead up to 35% and can provide an efficient,
flexible, and verifiable means for compiling Giotto programs on complex architectures,
such as the TTA.
acknowledgement: This work was supported by the AFOSR MURI grant F49620-00-1-0327,
the California MICRO grant 01-037, the DARPA grant F33615-C-98-3614, the MARCO grant
98-DT-660, and the NSF grants CCR-0208875, CCR-0085949, and CCR-0225610.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: 'Henzinger TA, Kirsch C, Matic S. Schedule-carrying code. In: Proceedings
of the 3rd International Conference on Embedded Software. Vol 2855. ACM; 2003:241-256.
doi:10.1007/978-3-540-45212-6_16'
apa: 'Henzinger, T. A., Kirsch, C., & Matic, S. (2003). Schedule-carrying code.
In Proceedings of the 3rd International Conference on Embedded Software
(Vol. 2855, pp. 241–256). Philadelphia, PA, USA: ACM. https://doi.org/10.1007/978-3-540-45212-6_16'
chicago: Henzinger, Thomas A, Christoph Kirsch, and Slobodan Matic. “Schedule-Carrying
Code.” In Proceedings of the 3rd International Conference on Embedded Software,
2855:241–56. ACM, 2003. https://doi.org/10.1007/978-3-540-45212-6_16.
ieee: T. A. Henzinger, C. Kirsch, and S. Matic, “Schedule-carrying code,” in Proceedings
of the 3rd International Conference on Embedded Software, Philadelphia, PA,
USA, 2003, vol. 2855, pp. 241–256.
ista: 'Henzinger TA, Kirsch C, Matic S. 2003. Schedule-carrying code. Proceedings
of the 3rd International Conference on Embedded Software. EMSOFT: Embedded Software
, LNCS, vol. 2855, 241–256.'
mla: Henzinger, Thomas A., et al. “Schedule-Carrying Code.” Proceedings of the
3rd International Conference on Embedded Software, vol. 2855, ACM, 2003, pp.
241–56, doi:10.1007/978-3-540-45212-6_16.
short: T.A. Henzinger, C. Kirsch, S. Matic, in:, Proceedings of the 3rd International
Conference on Embedded Software, ACM, 2003, pp. 241–256.
conference:
end_date: 2003-10-15
location: Philadelphia, PA, USA
name: 'EMSOFT: Embedded Software '
start_date: 2003-10-13
date_created: 2018-12-11T12:08:59Z
date_published: 2003-09-29T00:00:00Z
date_updated: 2024-01-10T11:33:57Z
day: '29'
doi: 10.1007/978-3-540-45212-6_16
extern: '1'
intvolume: ' 2855'
language:
- iso: eng
month: '09'
oa_version: None
page: 241 - 256
publication: Proceedings of the 3rd International Conference on Embedded Software
publication_identifier:
isbn:
- '9783540202233'
publication_status: published
publisher: ACM
publist_id: '267'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Schedule-carrying code
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2855
year: '2003'
...
---
_id: '4465'
abstract:
- lang: eng
text: Giotto is a principled, tool-supported design methodology for implementing
embedded control systems on platforms of possibly distributed sensors, actuators,
CPUs, and networks. Giotto is based on the principle that time-triggered task
invocations plus time-triggered mode switches can form the abstract essence of
programming real-time control systems. Giotto consists of a programming language
with a formal semantics, and a retargetable compiler and runtime library. Giotto
supports the automation of control system design by strictly separating platform-independent
functionality and timing concerns from platform-dependent scheduling and communication
issues. The time-triggered predictability of Giotto makes it particularly suitable
for safety-critical applications with hard real-time constraints. We illustrate
the platform independence and time-triggered execution of Giotto by coordinating
a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots.
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Henzinger TA, Horowitz B, Kirsch C. Embedded control systems development with
Giotto. In: Software-Enabled Control: Information Technology for Dynamical
Systems. Wiley-Blackwell; 2003:123-146. doi:10.1002/047172288X.ch8'
apa: 'Henzinger, T. A., Horowitz, B., & Kirsch, C. (2003). Embedded control
systems development with Giotto. In Software-Enabled Control: Information Technology
for Dynamical Systems (pp. 123–146). Wiley-Blackwell. https://doi.org/10.1002/047172288X.ch8'
chicago: 'Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Embedded
Control Systems Development with Giotto.” In Software-Enabled Control: Information
Technology for Dynamical Systems, 123–46. Wiley-Blackwell, 2003. https://doi.org/10.1002/047172288X.ch8.'
ieee: 'T. A. Henzinger, B. Horowitz, and C. Kirsch, “Embedded control systems development
with Giotto,” in Software-Enabled Control: Information Technology for Dynamical
Systems, Wiley-Blackwell, 2003, pp. 123–146.'
ista: 'Henzinger TA, Horowitz B, Kirsch C. 2003.Embedded control systems development
with Giotto. In: Software-Enabled Control: Information Technology for Dynamical
Systems. , 123–146.'
mla: 'Henzinger, Thomas A., et al. “Embedded Control Systems Development with Giotto.”
Software-Enabled Control: Information Technology for Dynamical Systems,
Wiley-Blackwell, 2003, pp. 123–46, doi:10.1002/047172288X.ch8.'
short: 'T.A. Henzinger, B. Horowitz, C. Kirsch, in:, Software-Enabled Control: Information
Technology for Dynamical Systems, Wiley-Blackwell, 2003, pp. 123–146.'
date_created: 2018-12-11T12:08:59Z
date_published: 2003-05-20T00:00:00Z
date_updated: 2024-01-08T12:24:01Z
day: '20'
doi: 10.1002/047172288X.ch8
extern: '1'
language:
- iso: eng
month: '05'
oa_version: None
page: 123 - 146
publication: 'Software-Enabled Control: Information Technology for Dynamical Systems'
publication_identifier:
isbn:
- '9780471234364 '
publication_status: published
publisher: Wiley-Blackwell
publist_id: '262'
quality_controlled: '1'
status: public
title: Embedded control systems development with Giotto
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2003'
...
---
_id: '4466'
abstract:
- lang: eng
text: One source of complexity in the μ-calculus is its ability to specify an unbounded
number of switches between universal (AX) and existential (EX) branching modes.
We therefore study the problems of satisfiability, validity, model checking, and
implication for the universal and existential fragments of the μ-calculus, in
which only one branching mode is allowed. The universal fragment is rich enough
to express most specifications of interest, and therefore improved algorithms
are of practical importance. We show that while the satisfiability and validity
problems become indeed simpler for the existential and universal fragments, this
is, unfortunately, not the case for model checking and implication. We also show
the corresponding results for the alternationfree fragment of the μ-calculus,
where no alternations between least and greatest fixed points are allowed. Our
results imply that efforts to find a polynomial-time model-checking algorithm
for the μ-calculus can be replaced by efforts to find such an algorithm for the
universal or existential fragment.
acknowledgement: This work was supported in part by NSF grant CCR-9988172, the AFOSR
MURI grant F49620-00-1-0327, and a Microsoft Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments
of the mu-calculus. In: Proceedings of the 9th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems . Vol 2619.
Springer; 2003:49-64. doi:10.1007/3-540-36577-X_5'
apa: 'Henzinger, T. A., Kupferman, O., & Majumdar, R. (2003). On the universal
and existential fragments of the mu-calculus. In Proceedings of the 9th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 2619, pp. 49–64). Warsaw, Poland: Springer. https://doi.org/10.1007/3-540-36577-X_5'
chicago: Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal
and Existential Fragments of the Mu-Calculus.” In Proceedings of the 9th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
, 2619:49–64. Springer, 2003. https://doi.org/10.1007/3-540-36577-X_5.
ieee: T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential
fragments of the mu-calculus,” in Proceedings of the 9th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems , Warsaw,
Poland, 2003, vol. 2619, pp. 49–64.
ista: 'Henzinger TA, Kupferman O, Majumdar R. 2003. On the universal and existential
fragments of the mu-calculus. Proceedings of the 9th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems . TACAS:
Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.
2619, 49–64.'
mla: Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of
the Mu-Calculus.” Proceedings of the 9th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems , vol. 2619, Springer,
2003, pp. 49–64, doi:10.1007/3-540-36577-X_5.
short: T.A. Henzinger, O. Kupferman, R. Majumdar, in:, Proceedings of the 9th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
, Springer, 2003, pp. 49–64.
conference:
end_date: 2003-04-11
location: Warsaw, Poland
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2003-04-07
date_created: 2018-12-11T12:08:59Z
date_published: 2003-03-14T00:00:00Z
date_updated: 2024-01-08T13:17:35Z
day: '14'
doi: 10.1007/3-540-36577-X_5
extern: '1'
intvolume: ' 2619'
language:
- iso: eng
month: '03'
oa_version: None
page: 49 - 64
publication: 'Proceedings of the 9th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems '
publication_identifier:
isbn:
- '9783540008989'
publication_status: published
publisher: Springer
publist_id: '263'
quality_controlled: '1'
status: public
title: On the universal and existential fragments of the mu-calculus
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2619
year: '2003'
...
---
_id: '4467'
abstract:
- lang: eng
text: 'BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification
system for checking safety properties of C programs using automatic property-driven
construction and model checking of software abstractions. Blast implements an
abstract-model check-refine loop to check for reachability of a specified label
in the program. The abstract model is built on the fly using predicate abstraction.
This model is then checked for reachability. If there is no (abstract) path to
the specified error label, Blast reports that the system is safe and produces
a succinct proof. Otherwise, it checks if the path is feasible using symbolic
execution of the program. If the path is feasible, Blast outputs the path as an
error trace, otherwise, it uses the infeasibility of the path to refine the abstract
model. Blast short-circuits the loop from abstraction to verification to refinement,
integrating the three steps tightly through “lazy abstraction” [5]. This integration
can offer significant advantages in performance by avoiding the repetition of
work from one iteration of the loop to the next. '
acknowledgement: This work was supported in part by the NSF grants CCR-0085949 and
CCR-9988172, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660,
and a Microsoft Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Grégoire
full_name: Sutre, Grégoire
last_name: Sutre
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST.
In: Proceedings of the 10th International SPIN Workshop . Vol 2648. Springer;
2003:235-239. doi:10.1007/3-540-44829-2_17'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Sutre, G. (2003). Software
verification with BLAST. In Proceedings of the 10th International SPIN Workshop
(Vol. 2648, pp. 235–239). Portland, OR, USA: Springer. https://doi.org/10.1007/3-540-44829-2_17'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre.
“Software Verification with BLAST.” In Proceedings of the 10th International
SPIN Workshop , 2648:235–39. Springer, 2003. https://doi.org/10.1007/3-540-44829-2_17.
ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Software verification
with BLAST,” in Proceedings of the 10th International SPIN Workshop , Portland,
OR, USA, 2003, vol. 2648, pp. 235–239.
ista: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. 2003. Software verification with
BLAST. Proceedings of the 10th International SPIN Workshop . SPIN: Model Checking
Software, LNCS, vol. 2648, 235–239.'
mla: Henzinger, Thomas A., et al. “Software Verification with BLAST.” Proceedings
of the 10th International SPIN Workshop , vol. 2648, Springer, 2003, pp. 235–39,
doi:10.1007/3-540-44829-2_17.
short: T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the
10th International SPIN Workshop , Springer, 2003, pp. 235–239.
conference:
end_date: 2003-05-10
location: Portland, OR, USA
name: 'SPIN: Model Checking Software'
start_date: 2003-05-09
date_created: 2018-12-11T12:09:00Z
date_published: 2003-04-28T00:00:00Z
date_updated: 2024-01-08T14:05:29Z
day: '28'
doi: 10.1007/3-540-44829-2_17
extern: '1'
intvolume: ' 2648'
language:
- iso: eng
month: '04'
oa_version: None
page: 235 - 239
publication: 'Proceedings of the 10th International SPIN Workshop '
publication_identifier:
isbn:
- '9783540401179'
publication_status: published
publisher: Springer
publist_id: '264'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Software verification with BLAST
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2648
year: '2003'
...
---
_id: '4468'
abstract:
- lang: eng
text: Giotto is a high-level programming language for time-triggered control applications.
The authors begin with a conceptual overview of its methodology, discuss the Giotto
helicopter project, and summarize available Giotto implementations.
acknowledgement: We thank Niklaus Wirth and Walter Schaufelberger for their advice
and support of the reengineering effort of the ETH Zurich helicopter control system
using Giotto. This research was supported in part by DARPA SEC grant F33615-C-98–3614,
MARCO GSRC grant 98-DT-660, and AFOSR MURI grant F49620–00-1–0327. A preliminary
version of this article appeared as [1].
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Marco
full_name: Sanvido, Marco
last_name: Sanvido
- first_name: Wolfgang
full_name: Pree, Wolfgang
last_name: Pree
citation:
ama: Henzinger TA, Kirsch C, Sanvido M, Pree W. From control models to real-time
code using Giotto. IEEE Control Systems Magazine. 2003;23(1):50-64. doi:10.1109/MCS.2003.1172829
apa: Henzinger, T. A., Kirsch, C., Sanvido, M., & Pree, W. (2003). From control
models to real-time code using Giotto. IEEE Control Systems Magazine. IEEE.
https://doi.org/10.1109/MCS.2003.1172829
chicago: Henzinger, Thomas A, Christoph Kirsch, Marco Sanvido, and Wolfgang Pree.
“From Control Models to Real-Time Code Using Giotto.” IEEE Control Systems
Magazine. IEEE, 2003. https://doi.org/10.1109/MCS.2003.1172829.
ieee: T. A. Henzinger, C. Kirsch, M. Sanvido, and W. Pree, “From control models
to real-time code using Giotto,” IEEE Control Systems Magazine, vol. 23,
no. 1. IEEE, pp. 50–64, 2003.
ista: Henzinger TA, Kirsch C, Sanvido M, Pree W. 2003. From control models to real-time
code using Giotto. IEEE Control Systems Magazine. 23(1), 50–64.
mla: Henzinger, Thomas A., et al. “From Control Models to Real-Time Code Using Giotto.”
IEEE Control Systems Magazine, vol. 23, no. 1, IEEE, 2003, pp. 50–64, doi:10.1109/MCS.2003.1172829.
short: T.A. Henzinger, C. Kirsch, M. Sanvido, W. Pree, IEEE Control Systems Magazine
23 (2003) 50–64.
date_created: 2018-12-11T12:09:00Z
date_published: 2003-01-29T00:00:00Z
date_updated: 2024-01-08T10:54:53Z
day: '29'
doi: 10.1109/MCS.2003.1172829
extern: '1'
intvolume: ' 23'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 50 - 64
publication: IEEE Control Systems Magazine
publication_identifier:
issn:
- '1066-033X '
publication_status: published
publisher: IEEE
publist_id: '260'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From control models to real-time code using Giotto
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 23
year: '2003'
...
---
_id: '4469'
abstract:
- lang: eng
text: Giotto provides an abstract programmer's model for the implementation of embedded
control systems with hard real-time constraints. A typical control application
consists of periodic software tasks together with a mode-switching logic for enabling
and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations,
actuator updates, and mode switches independent of any implementation platform.
Giotto can be annotated with platform constraints such as task-to-host mappings,
and task and communication schedules. The annotations are directives for the Giotto
compiler, but they do not alter the functionality and timing of a Giotto program.
By separating the platform-independent from the platform-dependent concerns, Giotto
enables a great deal of flexibility in choosing control platforms as well as a
great deal of automation in the validation and synthesis of control software.
The time-triggered nature of Giotto achieves timing predictability, which makes
Giotto particularly suitable for safety-critical applications.
acknowledgement: The authors would like to thank R. Majumdar for implementing a prototype
Giotto compiler for Lego Mindstorms robots. They would like to thank D. Derevyanko
and W. Williams for building the Intel x86 robots; and E. Lee and X. Liu for help
with implementing Giotto as a “model of computation” in Ptolemy II [26]. Finally,
they would also like to thank M. Sanvido for his suggestions on the design of the
Giotto drivers; and P. Griffiths for implementing the functionality code of the
electronic throttle controller.
article_processing_charge: No
article_type: original
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Henzinger TA, Horowitz B, Kirsch C. Giotto: A time-triggered language for
embedded programming. Proceedings of the IEEE. 2003;91(1):84-99. doi:10.1109/JPROC.2002.805825'
apa: 'Henzinger, T. A., Horowitz, B., & Kirsch, C. (2003). Giotto: A time-triggered
language for embedded programming. Proceedings of the IEEE. IEEE. https://doi.org/10.1109/JPROC.2002.805825'
chicago: 'Henzinger, Thomas A, Benjamin Horowitz, and Christoph Kirsch. “Giotto:
A Time-Triggered Language for Embedded Programming.” Proceedings of the IEEE.
IEEE, 2003. https://doi.org/10.1109/JPROC.2002.805825.'
ieee: 'T. A. Henzinger, B. Horowitz, and C. Kirsch, “Giotto: A time-triggered language
for embedded programming,” Proceedings of the IEEE, vol. 91, no. 1. IEEE,
pp. 84–99, 2003.'
ista: 'Henzinger TA, Horowitz B, Kirsch C. 2003. Giotto: A time-triggered language
for embedded programming. Proceedings of the IEEE. 91(1), 84–99.'
mla: 'Henzinger, Thomas A., et al. “Giotto: A Time-Triggered Language for Embedded
Programming.” Proceedings of the IEEE, vol. 91, no. 1, IEEE, 2003, pp.
84–99, doi:10.1109/JPROC.2002.805825.'
short: T.A. Henzinger, B. Horowitz, C. Kirsch, Proceedings of the IEEE 91 (2003)
84–99.
date_created: 2018-12-11T12:09:00Z
date_published: 2003-01-29T00:00:00Z
date_updated: 2024-01-10T11:55:18Z
day: '29'
doi: 10.1109/JPROC.2002.805825
extern: '1'
intvolume: ' 91'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 84 - 99
publication: Proceedings of the IEEE
publication_identifier:
issn:
- '0018-9219 '
publication_status: published
publisher: IEEE
publist_id: '261'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Giotto: A time-triggered language for embedded programming'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 91
year: '2003'
...
---
_id: '4561'
abstract:
- lang: eng
text: 'We present a formalism for specifying component interfaces that expose component
requirements on limited resources. The formalism permits an algorithmic check
if two or more components, when put together, exceed the available resources.
Moreover, the formalism can be used to compute the quantity of resources necessary
for satisfying the requirements of a collection of components. The formalism can
be instantiated in several ways. For example, several components may draw power
from the same source. Then, the formalism supports compatibility checks such as:
can two components, when put together, achieve their tasks without ever exceeding
the available amount of peak power? or, can they achieve their tasks by using
no more than the initially available amount of energy (i.e., power accumulated
over time)? The corresponding quantitative questions that our algorithms answer
are the following: what is the amount of peak power needed for two components
to be put together? what is the corresponding amount of initial energy? To solve
these questions, we model interfaces with resource requirements as games with
quantitative objectives. The games are played on state spaces where each state
is labeled by a number (representing, e.g., power consumption), and a play produces
an infinite path of labels. The objective may be, for example, to minimize the
largest label that occurs during a play. We illustrate our approach by modeling
compatibility questions for the components of robot control software, and of wireless
sensor networks.'
acknowledgement: This research was supported in part by the DARPA grant F33615-00-C-1693,
the MARCO grant 98-DT-660, the ONR grant N00014-02-1-0671, and the NSF grants CCR-0085949,
CCR-0132780, CCR-0234690, and CCR-9988172.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'Chakrabarti A, De Alfaro L, Henzinger TA, Stoelinga M. Resource interfaces.
In: Third International Conference on Embedded Software. Vol 2855. ACM;
2003:117-133. doi:10.1007/978-3-540-45212-6_9'
apa: 'Chakrabarti, A., De Alfaro, L., Henzinger, T. A., & Stoelinga, M. (2003).
Resource interfaces. In Third International Conference on Embedded Software
(Vol. 2855, pp. 117–133). Philadelphia, PA, USA: ACM. https://doi.org/10.1007/978-3-540-45212-6_9'
chicago: Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, and Mariëlle
Stoelinga. “Resource Interfaces.” In Third International Conference on Embedded
Software, 2855:117–33. ACM, 2003. https://doi.org/10.1007/978-3-540-45212-6_9.
ieee: A. Chakrabarti, L. De Alfaro, T. A. Henzinger, and M. Stoelinga, “Resource
interfaces,” in Third International Conference on Embedded Software, Philadelphia,
PA, USA, 2003, vol. 2855, pp. 117–133.
ista: 'Chakrabarti A, De Alfaro L, Henzinger TA, Stoelinga M. 2003. Resource interfaces.
Third International Conference on Embedded Software. EMSOFT: Embedded Software
, LNCS, vol. 2855, 117–133.'
mla: Chakrabarti, Arindam, et al. “Resource Interfaces.” Third International
Conference on Embedded Software, vol. 2855, ACM, 2003, pp. 117–33, doi:10.1007/978-3-540-45212-6_9.
short: A. Chakrabarti, L. De Alfaro, T.A. Henzinger, M. Stoelinga, in:, Third International
Conference on Embedded Software, ACM, 2003, pp. 117–133.
conference:
end_date: 2003-10-15
location: Philadelphia, PA, USA
name: 'EMSOFT: Embedded Software '
start_date: 2003-10-13
date_created: 2018-12-11T12:09:29Z
date_published: 2003-09-29T00:00:00Z
date_updated: 2024-01-08T10:48:11Z
day: '29'
doi: 10.1007/978-3-540-45212-6_9
extern: '1'
intvolume: ' 2855'
language:
- iso: eng
month: '09'
oa_version: None
page: 117 - 133
publication: Third International Conference on Embedded Software
publication_identifier:
isbn:
- '9783540202233'
publication_status: published
publisher: ACM
publist_id: '148'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Resource interfaces
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2855
year: '2003'
...
---
_id: '4628'
abstract:
- lang: eng
text: 'Discounting the future means that the value, today, of a unit payoffis 1
if the payoffo ccurs today, a if it occurs tomorrow, a 2 if it occurs the day
after tomorrow, and so on, for some real-valued discount factor 0 < a <
1. Discounting (or inflation) is a key paradigm in economics and has been studied
in Markov decision processes as well as game theory. We submit that discounting
also has a natural place in systems engineering: for nonterminating systems, a
potential bug in the far-away future is less troubling than a potential bug today.
We therefore develop a systems theory with discounting. Our theory includes several
basic elements: discounted versions of system properties that correspond to the
ω-regular properties, fixpoint-based algorithms for checking discounted properties,
and a quantitative notion of bisimilarity for capturing the difference between
two states with respect to discounted properties. We present the theory in a general
form that applies to probabilistic systems as well as multicomponent systems (games),
but it readily specializes to classical transition systems. We show that discounting,
besides its natural practical appeal, has also several mathematical benefits.
First, the resulting theory is robust, in that small perturbations of a system
can cause only small changes in the properties of the system. Second, the theory
is computational, in that the values of discounted properties, as well as the
discounted bisimilarity distance between states, can be computed to any desired
degree of precision.'
acknowledgement: This research was supported in part by the NSF CAREER award CCR-0132780,
the DARPA grant F33615-C-98-3614, the NSF grants CCR-9988172, CCR-0234690 and CCR-0225610,
and the ONR grant N00014-02-1-0671.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'De Alfaro L, Henzinger TA, Majumdar R. Discounting the future in systems theory.
In: Proceedings of the 30th International Colloquium on Automata, Languages
and Programming. Vol 2719. Springer; 2003:1022-1037. doi:10.1007/3-540-45061-0_79'
apa: 'De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2003). Discounting the
future in systems theory. In Proceedings of the 30th International Colloquium
on Automata, Languages and Programming (Vol. 2719, pp. 1022–1037). Eindhoven,
The Netherlands: Springer. https://doi.org/10.1007/3-540-45061-0_79'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Discounting
the Future in Systems Theory.” In Proceedings of the 30th International Colloquium
on Automata, Languages and Programming, 2719:1022–37. Springer, 2003. https://doi.org/10.1007/3-540-45061-0_79.
ieee: L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Discounting the future in
systems theory,” in Proceedings of the 30th International Colloquium on Automata,
Languages and Programming, Eindhoven, The Netherlands, 2003, vol. 2719, pp.
1022–1037.
ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2003. Discounting the future in systems
theory. Proceedings of the 30th International Colloquium on Automata, Languages
and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2719,
1022–1037.'
mla: De Alfaro, Luca, et al. “Discounting the Future in Systems Theory.” Proceedings
of the 30th International Colloquium on Automata, Languages and Programming,
vol. 2719, Springer, 2003, pp. 1022–37, doi:10.1007/3-540-45061-0_79.
short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 30th International
Colloquium on Automata, Languages and Programming, Springer, 2003, pp. 1022–1037.
conference:
end_date: 2003-07-04
location: Eindhoven, The Netherlands
name: 'ICALP: Automata, Languages and Programming'
start_date: 2003-06-30
date_created: 2018-12-11T12:09:50Z
date_published: 2003-06-25T00:00:00Z
date_updated: 2023-07-26T13:07:31Z
day: '25'
doi: 10.1007/3-540-45061-0_79
extern: '1'
intvolume: ' 2719'
language:
- iso: eng
month: '06'
oa_version: None
page: 1022 - 1037
publication: Proceedings of the 30th International Colloquium on Automata, Languages
and Programming
publication_identifier:
isbn:
- '9783540404934'
publication_status: published
publisher: Springer
publist_id: '77'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discounting the future in systems theory
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2719
year: '2003'
...
---
_id: '4630'
abstract:
- lang: eng
text: We consider concurrent two-person games played in real time, in which the
players decide both which action to play, and when to play it. Such timed games
differ from untimed games in two essential ways. First, players can take each
other by surprise, because actions are played with delays that cannot be anticipated
by the opponent. Second, a player should not be able to win the game by preventing
time from diverging. We present a model of timed games that preserves the element
of surprise and accounts for time divergence in a way that treats both players
symmetrically and applies to all ω-regular winning conditions. We prove that the
ability to take each other by surprise adds extra power to the players. For the
case that the games are specified in the style of timed automata, we provide symbolic
algorithms for their solution with respect to all ω-regular winning conditions.
We also show that for these timed games, memory strategies are more powerful than
memoryless strategies already in the case of reachability objectives.
acknowledgement: Supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA
grant F33615-C-98-3614, the MARCO grant 98-DT-660, -the ONR grant N00014-02-1-0671,
the NSF grants CCR-9988172, CCR-0225610, and CCR-0234690, the NSF CAREER award CCR-0132780,
and the MIUR grant MEFISTO.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Marco
full_name: Faella, Marco
last_name: Faella
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. The element
of surprise in timed games. In: Proceedings of the 14th International Conference
on Concurrency Theory. Vol 2761. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2003:144-158. doi:10.1007/978-3-540-45187-7_9'
apa: 'De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., & Stoelinga,
M. (2003). The element of surprise in timed games. In Proceedings of the 14th
International Conference on Concurrency Theory (Vol. 2761, pp. 144–158). Marseille,
France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-540-45187-7_9'
chicago: De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and
Mariëlle Stoelinga. “The Element of Surprise in Timed Games.” In Proceedings
of the 14th International Conference on Concurrency Theory, 2761:144–58. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2003. https://doi.org/10.1007/978-3-540-45187-7_9.
ieee: L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, “The
element of surprise in timed games,” in Proceedings of the 14th International
Conference on Concurrency Theory, Marseille, France, 2003, vol. 2761, pp.
144–158.
ista: 'De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2003. The element
of surprise in timed games. Proceedings of the 14th International Conference on
Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2761, 144–158.'
mla: De Alfaro, Luca, et al. “The Element of Surprise in Timed Games.” Proceedings
of the 14th International Conference on Concurrency Theory, vol. 2761, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2003, pp. 144–58, doi:10.1007/978-3-540-45187-7_9.
short: L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:,
Proceedings of the 14th International Conference on Concurrency Theory, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2003, pp. 144–158.
conference:
end_date: 2003-09-05
location: Marseille, France
name: 'CONCUR: Concurrency Theory'
start_date: 2003-09-03
date_created: 2018-12-11T12:09:51Z
date_published: 2003-08-21T00:00:00Z
date_updated: 2024-01-08T10:05:30Z
day: '21'
doi: 10.1007/978-3-540-45187-7_9
extern: '1'
intvolume: ' 2761'
language:
- iso: eng
month: '08'
oa_version: None
page: 144 - 158
publication: Proceedings of the 14th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540407539'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '78'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The element of surprise in timed games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2761
year: '2003'
...
---
_id: '12659'
abstract:
- lang: eng
text: "For many years considerable efforts have been put into investigating and
modelling hydrological processes of mountainous catchments. On the one hand, the
complexity and intrinsically high variability of the involved processes as well
as insufficient knowledge of the underlying physical mechanisms still induce large
uncertainties in understanding observed phenomena and predicting the behaviour
of the system. On the other hand, the demand for models that are able to simulate
mountainous water resource systems is increasing because of the needs related
to both water exploitation and water conservation, which clearly call for an integrated
vision and modelling of these systems.\r\nAccordingly, this paper moves from a
brief survey of the most significant achievements in mountain hydrology to discuss
what could be future challenging issues related to the broader spectrum of questions,
which hydrologic modelling of mountainous river systems may face in the next decades.
Firstly, reference is made to existing methodologies for modelling alpine water
systems, focussing on some specific aspects that provide a basis for the discussion
of the weaknesses and perspectives of present simulation tools. The future is
thus discussed, delineating some of the research challenges that may foster a
comprehensive and integrated vision of water related issues in mountainous regions."
article_processing_charge: No
article_type: original
author:
- first_name: Paolo
full_name: Burlando, Paolo
last_name: Burlando
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: Ulrich
full_name: Strasser, Ulrich
last_name: Strasser
citation:
ama: Burlando P, Pellicciotti F, Strasser U. Modelling mountainous water systems
between learning and speculating looking for challenges. Hydrology Research.
2002;33(1):47-74. doi:10.2166/nh.2002.0004
apa: Burlando, P., Pellicciotti, F., & Strasser, U. (2002). Modelling mountainous
water systems between learning and speculating looking for challenges. Hydrology
Research. IWA Publishing. https://doi.org/10.2166/nh.2002.0004
chicago: Burlando, Paolo, Francesca Pellicciotti, and Ulrich Strasser. “Modelling
Mountainous Water Systems between Learning and Speculating Looking for Challenges.”
Hydrology Research. IWA Publishing, 2002. https://doi.org/10.2166/nh.2002.0004.
ieee: P. Burlando, F. Pellicciotti, and U. Strasser, “Modelling mountainous water
systems between learning and speculating looking for challenges,” Hydrology
Research, vol. 33, no. 1. IWA Publishing, pp. 47–74, 2002.
ista: Burlando P, Pellicciotti F, Strasser U. 2002. Modelling mountainous water
systems between learning and speculating looking for challenges. Hydrology Research.
33(1), 47–74.
mla: Burlando, Paolo, et al. “Modelling Mountainous Water Systems between Learning
and Speculating Looking for Challenges.” Hydrology Research, vol. 33, no.
1, IWA Publishing, 2002, pp. 47–74, doi:10.2166/nh.2002.0004.
short: P. Burlando, F. Pellicciotti, U. Strasser, Hydrology Research 33 (2002) 47–74.
date_created: 2023-02-20T08:19:02Z
date_published: 2002-02-01T00:00:00Z
date_updated: 2023-02-20T08:30:15Z
day: '01'
doi: 10.2166/nh.2002.0004
extern: '1'
intvolume: ' 33'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.2166/nh.2002.0004
month: '02'
oa: 1
oa_version: Published Version
page: 47-74
publication: Hydrology Research
publication_identifier:
eissn:
- 2224-7955
issn:
- 0029-1277
publication_status: published
publisher: IWA Publishing
quality_controlled: '1'
scopus_import: '1'
status: public
title: Modelling mountainous water systems between learning and speculating looking
for challenges
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 33
year: '2002'
...
---
_id: '859'
abstract:
- lang: eng
text: The polymeric ubiquitin (poly-u) genes are composed of tandem 228-bp repeats
with no spacer sequences between individual monomer units. Ubiquitin is one of
the most conserved proteins known to date, and the individual units within a number
of poly-u genes are significantly more similar to each other than would be expected
if each unit evolved independently. It has been proposed that the rather striking
similarity among poly-u monomers in some lineages is caused by a series of homogenization
events. Here we report the sequences of the polyubiquitin-C (Ubc) genes in two
mouse strains. Analysis of these sequences, as well as those of the previously
reported Chinese hamster and rat poly-u genes, supports the assertion that the
homogenization of the ubiquitin-C gene in rodents is due to unequal crossing-over
events. The sequence divergence of noncoding DNA was used to estimate the frequency
of unequal crossing-over events (6.3 x 10-5 events per generation) in the Ubc
gene, as well as to provide evidence of apparent selection in the poly-u gene.
acknowledgement: We are thankful to J.A. Southerland and P.L. Jiang for technical
assistance in DNA sequencing, as well as to Y.I. Pavlov for helpful discussions.
This work was supported by public Health Service Research Grant AI45135 from the
Institute of Allergy and Infectious Diseases, National Institutes of Health.
article_processing_charge: No
article_type: original
author:
- first_name: Andrey
full_name: Perelygin, Andrey
last_name: Perelygin
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Igor
full_name: Rogozin, Igor
last_name: Rogozin
- first_name: Margo
full_name: Brinton, Margo
last_name: Brinton
citation:
ama: Perelygin A, Kondrashov F, Rogozin I, Brinton M. Evolution of the mouse polyubiquitin
C gene. Journal of Molecular Evolution. 2002;55(2):202-210. doi:10.1007/s00239-002-2318-0
apa: Perelygin, A., Kondrashov, F., Rogozin, I., & Brinton, M. (2002). Evolution
of the mouse polyubiquitin C gene. Journal of Molecular Evolution. Springer.
https://doi.org/10.1007/s00239-002-2318-0
chicago: Perelygin, Andrey, Fyodor Kondrashov, Igor Rogozin, and Margo Brinton.
“Evolution of the Mouse Polyubiquitin C Gene.” Journal of Molecular Evolution.
Springer, 2002. https://doi.org/10.1007/s00239-002-2318-0.
ieee: A. Perelygin, F. Kondrashov, I. Rogozin, and M. Brinton, “Evolution of the
mouse polyubiquitin C gene,” Journal of Molecular Evolution, vol. 55, no.
2. Springer, pp. 202–210, 2002.
ista: Perelygin A, Kondrashov F, Rogozin I, Brinton M. 2002. Evolution of the mouse
polyubiquitin C gene. Journal of Molecular Evolution. 55(2), 202–210.
mla: Perelygin, Andrey, et al. “Evolution of the Mouse Polyubiquitin C Gene.” Journal
of Molecular Evolution, vol. 55, no. 2, Springer, 2002, pp. 202–10, doi:10.1007/s00239-002-2318-0.
short: A. Perelygin, F. Kondrashov, I. Rogozin, M. Brinton, Journal of Molecular
Evolution 55 (2002) 202–210.
date_created: 2018-12-11T11:48:53Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-07-26T12:01:34Z
day: '01'
doi: 10.1007/s00239-002-2318-0
extern: '1'
external_id:
pmid:
- '12107596'
intvolume: ' 55'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 202 - 210
pmid: 1
publication: Journal of Molecular Evolution
publication_identifier:
issn:
- 0022-2844
publication_status: published
publisher: Springer
publist_id: '6787'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolution of the mouse polyubiquitin C gene
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 55
year: '2002'
...
---
_id: '871'
abstract:
- lang: eng
text: 'BACKGROUND: Gene duplications have a major role in the evolution of new biological
functions. Theoretical studies often assume that a duplication per se is selectively
neutral and that, following a duplication, one of the gene copies is freed from
purifying (stabilizing) selection, which creates the potential for evolution of
a new function. RESULTS: In search of systematic evidence of accelerated evolution
after duplication, we used data from 26 bacterial, six archaeal, and seven eukaryotic
genomes to compare the mode and strength of selection acting on recently duplicated
genes (paralogs) and on similarly diverged, unduplicated orthologous genes in
different species. We find that the ratio of nonsynonymous to synonymous substitutions
(Kn/Ks) in most paralogous pairs is <<1 and that paralogs typically evolve
at similar rates, without significant asymmetry, indicating that both paralogs
produced by a duplication are subject to purifying selection. This selection is,
however, substantially weaker than the purifying selection affecting unduplicated
orthologs that have diverged to the same extent as the analyzed paralogs. Most
of the recently duplicated genes appear to be involved in various forms of environmental
response; in particular, many of them encode membrane and secreted proteins. CONCLUSIONS:
The results of this analysis indicate that recently duplicated paralogs evolve
faster than orthologs with the same level of divergence and similar functions,
but apparently do not experience a phase of neutral evolution. We hypothesize
that gene duplications that persist in an evolving lineage are beneficial from
the time of their origin, due primarily to a protein dosage effect in response
to variable environmental conditions; duplications are likely to give rise to
new functions at a later phase of their evolution once a higher level of divergence
is reached.'
acknowledgement: We are grateful to A.S. Kondrashov for numerous helpful suggestions,
to I. King Jordan, M.A. Roytberg, J.L. Spouge and D.A. Kondrashov for useful discussions
and to A.S. Kondrashov, I. King Jordan and D.J. Lipman for critical reading of the
manuscript.
article_processing_charge: No
article_type: original
author:
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Igor
full_name: Rogozin, Igor
last_name: Rogozin
- first_name: Yuri
full_name: Wolf, Yuri
last_name: Wolf
- first_name: Eugene
full_name: Koonin, Eugene
last_name: Koonin
citation:
ama: Kondrashov F, Rogozin I, Wolf Y, Koonin E. Selection in the evolution of gene
duplications . Genome Biology. 2002;3(2). doi:10.1186/gb-2002-3-2-research0008
apa: Kondrashov, F., Rogozin, I., Wolf, Y., & Koonin, E. (2002). Selection in
the evolution of gene duplications . Genome Biology. BioMed Central. https://doi.org/10.1186/gb-2002-3-2-research0008
chicago: Kondrashov, Fyodor, Igor Rogozin, Yuri Wolf, and Eugene Koonin. “Selection
in the Evolution of Gene Duplications .” Genome Biology. BioMed Central,
2002. https://doi.org/10.1186/gb-2002-3-2-research0008.
ieee: F. Kondrashov, I. Rogozin, Y. Wolf, and E. Koonin, “Selection in the evolution
of gene duplications ,” Genome Biology, vol. 3, no. 2. BioMed Central,
2002.
ista: Kondrashov F, Rogozin I, Wolf Y, Koonin E. 2002. Selection in the evolution
of gene duplications . Genome Biology. 3(2).
mla: Kondrashov, Fyodor, et al. “Selection in the Evolution of Gene Duplications
.” Genome Biology, vol. 3, no. 2, BioMed Central, 2002, doi:10.1186/gb-2002-3-2-research0008.
short: F. Kondrashov, I. Rogozin, Y. Wolf, E. Koonin, Genome Biology 3 (2002).
date_created: 2018-12-11T11:48:57Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-07-26T11:48:27Z
day: '01'
doi: 10.1186/gb-2002-3-2-research0008
extern: '1'
external_id:
pmid:
- '11864370'
intvolume: ' 3'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC65685/
month: '01'
oa: 1
oa_version: Published Version
pmid: 1
publication: Genome Biology
publication_identifier:
issn:
- 1465-6906
publication_status: published
publisher: BioMed Central
publist_id: '6781'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Selection in the evolution of gene duplications '
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 3
year: '2002'
...
---
_id: '885'
abstract:
- lang: eng
text: We study fitness landscape in the space of protein sequences by relating sets
of human pathogenic missense mutations in 32 proteins to amino acid substitutions
that occurred in the course of evolution of these proteins. On average, ≈10% of
deviations of a nonhuman protein from its human ortholog are compensated pathogenic
deviations (CPDs), i.e., are caused by an amino acid substitution that, at this
site, would be pathogenic to humans. Normal functioning of a CPD-containing protein
must be caused by other, compensatory deviations of the nonhuman species from
humans. Together, a CPD and the corresponding compensatory deviation form a Dobzhansky-Muller
incompatibility that can be visualized as the corner on a fitness ridge. Thus,
proteins evolve along fitness ridges which contain only ≈10 steps between sucessive
corners. The fraction of CPDs among all deviations of a protein from its human
ortholog does not increase with the evolutionary distance between the proteins,
indicating that subtitutions that carry evolving proteins around these corners
occur in rapid succession, driven by positive selection. Data on fitness of interspecies
hybrids suggest that the compensatory change that makes a CPD fit usually occurs
within the same protein. Data on protein structures and on cooccurrence of amino
acids at different sites of multiple orthologous proteins often make it possible
to provisionally identify the substitution that compensates a partiCUlar CPD.
article_processing_charge: No
article_type: original
author:
- first_name: Alexey
full_name: Kondrashov, Alexey
last_name: Kondrashov
- first_name: Shamil
full_name: Sunyaev, Shamil
last_name: Sunyaev
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
citation:
ama: Kondrashov A, Sunyaev S, Kondrashov F. Dobzhansky-Muller incompatibilities
in protein evolution. PNAS. 2002;99(23):14878-14883. doi:10.1073/pnas.232565499
apa: Kondrashov, A., Sunyaev, S., & Kondrashov, F. (2002). Dobzhansky-Muller
incompatibilities in protein evolution. PNAS. National Academy of Sciences.
https://doi.org/10.1073/pnas.232565499
chicago: Kondrashov, Alexey, Shamil Sunyaev, and Fyodor Kondrashov. “Dobzhansky-Muller
Incompatibilities in Protein Evolution.” PNAS. National Academy of Sciences,
2002. https://doi.org/10.1073/pnas.232565499.
ieee: A. Kondrashov, S. Sunyaev, and F. Kondrashov, “Dobzhansky-Muller incompatibilities
in protein evolution,” PNAS, vol. 99, no. 23. National Academy of Sciences,
pp. 14878–14883, 2002.
ista: Kondrashov A, Sunyaev S, Kondrashov F. 2002. Dobzhansky-Muller incompatibilities
in protein evolution. PNAS. 99(23), 14878–14883.
mla: Kondrashov, Alexey, et al. “Dobzhansky-Muller Incompatibilities in Protein
Evolution.” PNAS, vol. 99, no. 23, National Academy of Sciences, 2002,
pp. 14878–83, doi:10.1073/pnas.232565499.
short: A. Kondrashov, S. Sunyaev, F. Kondrashov, PNAS 99 (2002) 14878–14883.
date_created: 2018-12-11T11:49:01Z
date_published: 2002-11-12T00:00:00Z
date_updated: 2023-07-26T09:48:37Z
day: '12'
doi: 10.1073/pnas.232565499
extern: '1'
external_id:
pmid:
- '12403824'
intvolume: ' 99'
issue: '23'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC137512/
month: '11'
oa: 1
oa_version: Published Version
page: 14878 - 14883
pmid: 1
publication: PNAS
publication_identifier:
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
publist_id: '6763'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Dobzhansky-Muller incompatibilities in protein evolution
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 99
year: '2002'
...
---
_id: '897'
abstract:
- lang: eng
text: "Transcription is a slow and expensive process: in eukaryotes, approximately
20 nucleotides can be transcribed per second at the expense of at least two ATP
molecules per nucleotide. Thus, at least for highly expressed genes, transcription
of long introns, which are particularly common in mammals, is costly. Using data
on the expression of genes that encode proteins in Caenorhabditis elegans and
Homo sapiens, we show that introns in highly expressed genes are substantially
shorter than those in genes that are expressed at low levels. This difference
is greater in humans, such that introns are, on average, 14 times shorter in highly
expressed genes than in genes with low expression, whereas in C. Elegans the difference
in intron length is only twofold. In contrast, the density of introns in a gene
does not strongly depend on the level of gene expression. Thus, natural selection
appears to favor short introns in highly expressed genes to minimize the cost
of transcription and other molecular processes, such as splicing.\r\n"
acknowledgement: We are grateful to A. Kondrashov, I. Rogozin and A. Feldman for reading
the manuscript and P. Bouman, J. Cherry, J. Blumensteil and T. Kim for discussion.
article_processing_charge: No
article_type: original
author:
- first_name: Cristian
full_name: Castillo Davis, Cristian
last_name: Castillo Davis
- first_name: Sergei
full_name: Mekhedov, Sergei
last_name: Mekhedov
- first_name: Daniel
full_name: Hartl, Daniel
last_name: Hartl
- first_name: Eugene
full_name: Koonin, Eugene
last_name: Koonin
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
citation:
ama: Castillo Davis C, Mekhedov S, Hartl D, Koonin E, Kondrashov F. Selection for
short introns in highly expressed genes. Nature Genetics. 2002;31(4):415-418.
doi:10.1038/ng940
apa: Castillo Davis, C., Mekhedov, S., Hartl, D., Koonin, E., & Kondrashov,
F. (2002). Selection for short introns in highly expressed genes. Nature Genetics.
Nature Publishing Group. https://doi.org/10.1038/ng940
chicago: Castillo Davis, Cristian, Sergei Mekhedov, Daniel Hartl, Eugene Koonin,
and Fyodor Kondrashov. “Selection for Short Introns in Highly Expressed Genes.”
Nature Genetics. Nature Publishing Group, 2002. https://doi.org/10.1038/ng940.
ieee: C. Castillo Davis, S. Mekhedov, D. Hartl, E. Koonin, and F. Kondrashov, “Selection
for short introns in highly expressed genes,” Nature Genetics, vol. 31,
no. 4. Nature Publishing Group, pp. 415–418, 2002.
ista: Castillo Davis C, Mekhedov S, Hartl D, Koonin E, Kondrashov F. 2002. Selection
for short introns in highly expressed genes. Nature Genetics. 31(4), 415–418.
mla: Castillo Davis, Cristian, et al. “Selection for Short Introns in Highly Expressed
Genes.” Nature Genetics, vol. 31, no. 4, Nature Publishing Group, 2002,
pp. 415–18, doi:10.1038/ng940.
short: C. Castillo Davis, S. Mekhedov, D. Hartl, E. Koonin, F. Kondrashov, Nature
Genetics 31 (2002) 415–418.
date_created: 2018-12-11T11:49:05Z
date_published: 2002-08-01T00:00:00Z
date_updated: 2023-07-26T09:45:30Z
day: '01'
doi: 10.1038/ng940
extern: '1'
external_id:
pmid:
- '12134150'
intvolume: ' 31'
issue: '4'
language:
- iso: eng
month: '08'
oa_version: None
page: 415 - 418
pmid: 1
publication: Nature Genetics
publication_status: published
publisher: Nature Publishing Group
publist_id: '6751'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Selection for short introns in highly expressed genes
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 31
year: '2002'
...
---
_id: '1737'
abstract:
- lang: eng
text: A new solvent-free composite polymer electrolyte consisting of high-molecular
mass polyethylene oxide (PEO) filled with titanium oxide and containing LiI and
I2 was developed. The introduction of the inorganic filler (TiO2 Degussa P25)
into the polymer matrix produces dramatic morphological changes to the host polymer
structure. Upon addition of the inorganic oxide, the surface roughness increases,
with respect to the original polymer and in parallel, the fractal dimension decreases.
Both the thermograms and the atomic force microscope (AFM) pictures confirm the
amorphicity of the composite electrolyte. The polymer sub-units are held together
in a parallel orientation, forming straight long chains of about 500 nm in width,
along which TiO2 spherical particles of about 20-25 nm in diameter are distributed.
The polymer chains separated by the titania particles are arranged in a three-dimensional,
mechanically stable network, that creates free space and voids into which the
iodide/triodide anions can easily migrate. All solid-state dye-sensitized solar
cells fabricated using this composite electrolyte present high efficiencies (typical
maximum incident photon to current efficiency (IPCE) as high as 40% at 520 nm
and overall conversion efficiency (η) of 0.96% (Voc = 0.67 V, Jsc = 2.050 mA/cm2,
FF = 39%) under direct solar irradiation. Further improvement of the photovoltaic
performance is expected by optimization of the electrolyte parameters and of the
cell assembly.
acknowledgement: Financial support from NCSR “Demokritos” (Dimoerevna 598 project),
Empeirikeion Foundation and General Secretariat for Research and Technology of Greece
(EPET II, Greece–France and Greece–Czech Republic bilateral collaboration projects)
is also greatly acknowledged. G. Katsaros thanks the Greek State Scholarships Foundation
(IKY) for fellowship allowance
article_processing_charge: No
author:
- first_name: Georgios
full_name: Katsaros, Georgios
id: 38DB5788-F248-11E8-B48F-1D18A9856A87
last_name: Katsaros
- first_name: Thomas
full_name: Stergiopoulos, Thomas
last_name: Stergiopoulos
- first_name: Iannis
full_name: Arabatzis, Iannis
last_name: Arabatzis
- first_name: Kyriaki
full_name: Papadokostaki, Kyriaki
last_name: Papadokostaki
- first_name: Polycarpos
full_name: Falaras, Polycarpos
last_name: Falaras
citation:
ama: 'Katsaros G, Stergiopoulos T, Arabatzis I, Papadokostaki K, Falaras P. A solvent-free
composite polymer/inorganic oxide electrolyte for high efficiency solid-state
dye-sensitized solar cells. Journal of Photochemistry and Photobiology A: Chemistry.
2002;149(1-3):191-198. doi:10.1016/S1010-6030(02)00027-8'
apa: 'Katsaros, G., Stergiopoulos, T., Arabatzis, I., Papadokostaki, K., & Falaras,
P. (2002). A solvent-free composite polymer/inorganic oxide electrolyte for high
efficiency solid-state dye-sensitized solar cells. Journal of Photochemistry
and Photobiology A: Chemistry. Elsevier. https://doi.org/10.1016/S1010-6030(02)00027-8'
chicago: 'Katsaros, Georgios, Thomas Stergiopoulos, Iannis Arabatzis, Kyriaki Papadokostaki,
and Polycarpos Falaras. “A Solvent-Free Composite Polymer/Inorganic Oxide Electrolyte
for High Efficiency Solid-State Dye-Sensitized Solar Cells.” Journal of Photochemistry
and Photobiology A: Chemistry. Elsevier, 2002. https://doi.org/10.1016/S1010-6030(02)00027-8.'
ieee: 'G. Katsaros, T. Stergiopoulos, I. Arabatzis, K. Papadokostaki, and P. Falaras,
“A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency
solid-state dye-sensitized solar cells,” Journal of Photochemistry and Photobiology
A: Chemistry, vol. 149, no. 1–3. Elsevier, pp. 191–198, 2002.'
ista: 'Katsaros G, Stergiopoulos T, Arabatzis I, Papadokostaki K, Falaras P. 2002.
A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency
solid-state dye-sensitized solar cells. Journal of Photochemistry and Photobiology
A: Chemistry. 149(1–3), 191–198.'
mla: 'Katsaros, Georgios, et al. “A Solvent-Free Composite Polymer/Inorganic Oxide
Electrolyte for High Efficiency Solid-State Dye-Sensitized Solar Cells.” Journal
of Photochemistry and Photobiology A: Chemistry, vol. 149, no. 1–3, Elsevier,
2002, pp. 191–98, doi:10.1016/S1010-6030(02)00027-8.'
short: 'G. Katsaros, T. Stergiopoulos, I. Arabatzis, K. Papadokostaki, P. Falaras,
Journal of Photochemistry and Photobiology A: Chemistry 149 (2002) 191–198.'
date_created: 2018-12-11T11:53:44Z
date_published: 2002-06-28T00:00:00Z
date_updated: 2023-07-26T08:56:55Z
day: '28'
doi: 10.1016/S1010-6030(02)00027-8
extern: '1'
intvolume: ' 149'
issue: 1-3
language:
- iso: eng
month: '06'
oa_version: None
page: 191 - 198
publication: 'Journal of Photochemistry and Photobiology A: Chemistry'
publication_identifier:
issn:
- 1010-6030
publication_status: published
publisher: Elsevier
publist_id: '5387'
status: public
title: A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency
solid-state dye-sensitized solar cells
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 149
year: '2002'
...
---
_id: '1738'
abstract:
- lang: eng
text: New dyes of the type Ru(II)(bdmpp)(bpy) [where bdmpp is 2,6-bis(3,5-dimethyl-N-pyrazoyl)pyridine
and bpy is 2,2′-bipyridine-4,4′-dicarboxylic acid] are prepared and characterized
by infra-red (IR), mass (MS) and electrospray mass spectroscopy (ES-MS) as well
as 1H NMR (1D and 2D) spectroscopies. The compounds present broad and very high
intensity MLCT absorption bands in the visible and can be chemically anchored
on TiO2 films via ester-like linkage involving carboxylato groups. These complexes
have been tested with success as potential molecular antennas in dye-sensitized
solar cells. Both opaque and transparent nanocrystalline TiO2 thin film electrodes
obtained by a doctor blade technique sensitized by these complexes were incorporated
in a sandwich type regenerative photoelectrochemical solar cell containing 0.1M
LiI +0.01M I2 in propylene carbonate as well as a platinized conductive glass
counter electrode. The cell was characterized by Raman spectroscopy under anodic
and cathodic bias. Two new vibration bands were observed in the lower frequency
region. The first one at 112 cm-1 is due to tri-iodide formed on the photoactive
electrode, and the second one at 167 cm-1 is a sign of the dye/iodide interaction
and corresponds to a vibration in a chemically stable "DI" intermediate
species. Under direct sunlight illumination (solar irradiance of 60 mW/cm2) by
using a composite polymer solid state electrolyte, the cell ITO/TiO2/[Ru(II)(bdmpp)(bpy)(NCS)](PF6)/electrolyte/Pt-ITO
produced a continuous photocurrent as high as 4.29mA/cm2, and gave IPCE values
about half of the corresponding values obtained by the standard N3 dye under the
same conditions. The photovoltage is about 600 mV and the overall energy conversion
cell's efficiency is as high as 1.72%.
author:
- first_name: Polycarpos
full_name: Falaras, Polycarpos
last_name: Falaras
- first_name: Katerina
full_name: Chryssou, Katerina
last_name: Chryssou
- first_name: Thomas
full_name: Stergiopoulos, Thomas
last_name: Stergiopoulos
- first_name: Ioannis
full_name: Arabatzis, Ioannis M
last_name: Arabatzis
- first_name: Georgios
full_name: Georgios Katsaros
id: 38DB5788-F248-11E8-B48F-1D18A9856A87
last_name: Katsaros
- first_name: Vincent
full_name: Catalano, Vincent J
last_name: Catalano
- first_name: Raif
full_name: Kurtaran, Raif
last_name: Kurtaran
- first_name: Anne
full_name: Hugot-Le Goff, Anne
last_name: Hugot Le Goff
- first_name: Marie
full_name: Bernard, Marie C
last_name: Bernard
citation:
ama: 'Falaras P, Chryssou K, Stergiopoulos T, et al. Dye-sensitization of titanium
dioxide thin films by Ru(II)-bpp-bpy complexes. In: Vol 4801. SPIE; 2002:125-135.
doi:10.1117/12.452446'
apa: Falaras, P., Chryssou, K., Stergiopoulos, T., Arabatzis, I., Katsaros, G.,
Catalano, V., … Bernard, M. (2002). Dye-sensitization of titanium dioxide thin
films by Ru(II)-bpp-bpy complexes (Vol. 4801, pp. 125–135). Presented at the Organic
Photovoltaics, SPIE. https://doi.org/10.1117/12.452446
chicago: Falaras, Polycarpos, Katerina Chryssou, Thomas Stergiopoulos, Ioannis Arabatzis,
Georgios Katsaros, Vincent Catalano, Raif Kurtaran, Anne Hugot Le Goff, and Marie
Bernard. “Dye-Sensitization of Titanium Dioxide Thin Films by Ru(II)-Bpp-Bpy Complexes,”
4801:125–35. SPIE, 2002. https://doi.org/10.1117/12.452446.
ieee: P. Falaras et al., “Dye-sensitization of titanium dioxide thin films
by Ru(II)-bpp-bpy complexes,” presented at the Organic Photovoltaics, 2002, vol.
4801, pp. 125–135.
ista: Falaras P, Chryssou K, Stergiopoulos T, Arabatzis I, Katsaros G, Catalano
V, Kurtaran R, Hugot Le Goff A, Bernard M. 2002. Dye-sensitization of titanium
dioxide thin films by Ru(II)-bpp-bpy complexes. Organic Photovoltaics vol. 4801,
125–135.
mla: Falaras, Polycarpos, et al. Dye-Sensitization of Titanium Dioxide Thin Films
by Ru(II)-Bpp-Bpy Complexes. Vol. 4801, SPIE, 2002, pp. 125–35, doi:10.1117/12.452446.
short: P. Falaras, K. Chryssou, T. Stergiopoulos, I. Arabatzis, G. Katsaros, V.
Catalano, R. Kurtaran, A. Hugot Le Goff, M. Bernard, in:, SPIE, 2002, pp. 125–135.
conference:
name: Organic Photovoltaics
date_created: 2018-12-11T11:53:45Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2021-01-12T06:52:53Z
day: '01'
doi: 10.1117/12.452446
extern: 1
intvolume: ' 4801'
month: '01'
page: 125 - 135
publication_status: published
publisher: SPIE
publist_id: '5385'
quality_controlled: 0
status: public
title: Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes
type: conference
volume: 4801
year: '2002'
...
---
_id: '1739'
abstract:
- lang: eng
text: Poly(ethylene oxide)/titania polymer electrolyte based photoelectrochemical
cells have been fabricated with Ru(dcbpy)2(NCS)2 complex as the sensitizer and
nanoporous TiO2 films as photoanodes. The introduction of the titania filler into
the poly(ethylene oxide) matrix reduces the crystallinity of the polymer and enhances
the mobility of the 1-/13 - redox couple, resulting in outstanding overall conversion
efficiency (4.2% under direct sunlight illumination) of the corresponding dye-sensitized
nanocrystalline TiO2 solar cell, one of the best efficiencies reported to date
for a solid-state device.
acknowledgement: 'Financial support from NCSR “Demokritos” and GSRT-Greece is greatly
acknowledged. '
author:
- first_name: Thomas
full_name: Stergiopoulos, Thomas
last_name: Stergiopoulos
- first_name: Iannis
full_name: Arabatzis, Iannis M
last_name: Arabatzis
- first_name: Georgios
full_name: Georgios Katsaros
id: 38DB5788-F248-11E8-B48F-1D18A9856A87
last_name: Katsaros
- first_name: Polycarpos
full_name: Falaras, Polycarpos
last_name: Falaras
citation:
ama: Stergiopoulos T, Arabatzis I, Katsaros G, Falaras P. Binary Polyethylene Oxide/Titania
Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical
Cells. Nano Letters. 2002;2(11):1259-1261. doi:10.1021/nl025798u
apa: Stergiopoulos, T., Arabatzis, I., Katsaros, G., & Falaras, P. (2002). Binary
Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient
Nanocrystalline TiO2 Photoelectrochemical Cells. Nano Letters. American
Chemical Society. https://doi.org/10.1021/nl025798u
chicago: Stergiopoulos, Thomas, Iannis Arabatzis, Georgios Katsaros, and Polycarpos
Falaras. “Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for
Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells.” Nano Letters.
American Chemical Society, 2002. https://doi.org/10.1021/nl025798u.
ieee: T. Stergiopoulos, I. Arabatzis, G. Katsaros, and P. Falaras, “Binary Polyethylene
Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline
TiO2 Photoelectrochemical Cells,” Nano Letters, vol. 2, no. 11. American
Chemical Society, pp. 1259–1261, 2002.
ista: Stergiopoulos T, Arabatzis I, Katsaros G, Falaras P. 2002. Binary Polyethylene
Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline
TiO2 Photoelectrochemical Cells. Nano Letters. 2(11), 1259–1261.
mla: Stergiopoulos, Thomas, et al. “Binary Polyethylene Oxide/Titania Solid-State
Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical
Cells.” Nano Letters, vol. 2, no. 11, American Chemical Society, 2002,
pp. 1259–61, doi:10.1021/nl025798u.
short: T. Stergiopoulos, I. Arabatzis, G. Katsaros, P. Falaras, Nano Letters 2 (2002)
1259–1261.
date_created: 2018-12-11T11:53:45Z
date_published: 2002-11-01T00:00:00Z
date_updated: 2021-01-12T06:52:53Z
day: '01'
doi: 10.1021/nl025798u
extern: 1
intvolume: ' 2'
issue: '11'
month: '11'
page: 1259 - 1261
publication: Nano Letters
publication_status: published
publisher: American Chemical Society
publist_id: '5386'
quality_controlled: 0
status: public
title: Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly
Efficient Nanocrystalline TiO2 Photoelectrochemical Cells
type: journal_article
volume: 2
year: '2002'
...
---
_id: '204'
abstract:
- lang: eng
text: Let k⩾5 be an integer, and let x⩾1 be an arbitrary real number. We derive
a bound[Formula presented] for the number of positive integers less than or equal
to x which can be represented as a sum of two non-negative coprime kth powers,
in essentially more than one way.
article_processing_charge: No
article_type: original
author:
- first_name: Timothy D
full_name: Browning, Timothy D
id: 35827D50-F248-11E8-B48F-1D18A9856A87
last_name: Browning
orcid: 0000-0002-8314-0177
citation:
ama: Browning TD. Equal Sums of Two kth Powers. Journal of Number Theory.
2002;96(2):293-318. doi:10.1006/jnth.2002.2800
apa: Browning, T. D. (2002). Equal Sums of Two kth Powers. Journal of Number
Theory. Academic Press. https://doi.org/10.1006/jnth.2002.2800
chicago: Browning, Timothy D. “Equal Sums of Two Kth Powers.” Journal of Number
Theory. Academic Press, 2002. https://doi.org/10.1006/jnth.2002.2800.
ieee: T. D. Browning, “Equal Sums of Two kth Powers,” Journal of Number Theory,
vol. 96, no. 2. Academic Press, pp. 293–318, 2002.
ista: Browning TD. 2002. Equal Sums of Two kth Powers. Journal of Number Theory.
96(2), 293–318.
mla: Browning, Timothy D. “Equal Sums of Two Kth Powers.” Journal of Number Theory,
vol. 96, no. 2, Academic Press, 2002, pp. 293–318, doi:10.1006/jnth.2002.2800.
short: T.D. Browning, Journal of Number Theory 96 (2002) 293–318.
date_created: 2018-12-11T11:45:11Z
date_published: 2002-10-02T00:00:00Z
date_updated: 2023-07-26T12:15:14Z
day: '02'
doi: 10.1006/jnth.2002.2800
extern: '1'
intvolume: ' 96'
issue: '2'
language:
- iso: eng
month: '10'
oa_version: Published Version
page: 293 - 318
publication: Journal of Number Theory
publication_identifier:
issn:
- 0022-314X
publication_status: published
publisher: Academic Press
publist_id: '7708'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Equal Sums of Two kth Powers
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
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 96
year: '2002'
...