---
_id: '3362'
abstract:
- lang: eng
text: State-transition systems communicating by shared variables have been the underlying
model of choice for applications of model checking. Such formalisms, however,
have difficulty with modeling process creation or death and communication reconfigurability.
Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling
formalism that supports dynamic reconfiguration and creation/death of processes.
The resulting formalism supports two types of variables, data variables and reference
variables. Reference variables enable changing the connectivity between processes
and referring to instances of processes. We show how this new formalism supports
parallel composition and refinement through trace containment. DRM provide a natural
language for modeling (and ultimately reasoning about) biological systems and
multiple threads communicating through shared variables.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- 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: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
- first_name: Anmol
full_name: Singh, Anmol
last_name: Singh
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. Dynamic
reactive modules. In: Vol 6901. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2011:404-418. doi:10.1007/978-3-642-23217-6_27'
apa: 'Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., &
Vardi, M. (2011). Dynamic reactive modules (Vol. 6901, pp. 404–418). Presented
at the CONCUR: Concurrency Theory, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.1007/978-3-642-23217-6_27'
chicago: Fisher, Jasmin, Thomas A Henzinger, Dejan Nickovic, Nir Piterman, Anmol
Singh, and Moshe Vardi. “Dynamic Reactive Modules,” 6901:404–18. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2011. https://doi.org/10.1007/978-3-642-23217-6_27.
ieee: 'J. Fisher, T. A. Henzinger, D. Nickovic, N. Piterman, A. Singh, and M. Vardi,
“Dynamic reactive modules,” presented at the CONCUR: Concurrency Theory, Aachen,
Germany, 2011, vol. 6901, pp. 404–418.'
ista: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. 2011. Dynamic
reactive modules. CONCUR: Concurrency Theory, LNCS, vol. 6901, 404–418.'
mla: Fisher, Jasmin, et al. Dynamic Reactive Modules. Vol. 6901, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:10.1007/978-3-642-23217-6_27.
short: J. Fisher, T.A. Henzinger, D. Nickovic, N. Piterman, A. Singh, M. Vardi,
in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–418.
conference:
end_date: 2011-09-09
location: Aachen, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2011-09-06
date_created: 2018-12-11T12:02:54Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-23217-6_27
ec_funded: 1
file:
- access_level: open_access
checksum: 6bf2453d8e52e979ddb58d17325bad26
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:17:48Z
date_updated: 2020-07-14T12:46:10Z
file_id: '7870'
file_name: 2011_CONCUR_Fisher.pdf
file_size: 337125
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6901'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 404 - 418
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '3253'
quality_controlled: '1'
scopus_import: 1
status: public
title: Dynamic reactive modules
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6901
year: '2011'
...
---
_id: '3363'
abstract:
- lang: eng
text: We consider probabilistic automata on infinite words with acceptance defined
by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider
quantitative and qualitative decision problems. We present extensions and adaptations
of proofs for probabilistic finite automata and present a complete characterization
of the decidability and undecidability frontier of the quantitative and qualitative
decision problems for probabilistic automata on infinite words.
article_number: '1104.0127'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Mathieu
full_name: Tracol, Mathieu
id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
last_name: Tracol
citation:
ama: Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic
automata on infinite words. doi:10.48550/arXiv.1104.0127
apa: Chatterjee, K., Henzinger, T. A., & Tracol, M. (n.d.). The decidability
frontier for probabilistic automata on infinite words. ArXiv. https://doi.org/10.48550/arXiv.1104.0127
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability
Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d. https://doi.org/10.48550/arXiv.1104.0127.
ieee: K. Chatterjee, T. A. Henzinger, and M. Tracol, “The decidability frontier
for probabilistic automata on infinite words.” ArXiv.
ista: Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic
automata on infinite words. 1104.0127.
mla: Chatterjee, Krishnendu, et al. The Decidability Frontier for Probabilistic
Automata on Infinite Words. 1104.0127, ArXiv, doi:10.48550/arXiv.1104.0127.
short: K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.).
corr_author: '1'
date_created: 2018-12-11T12:02:54Z
date_published: 2011-04-01T00:00:00Z
date_updated: 2025-06-26T09:19:59Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/arXiv.1104.0127
ec_funded: 1
external_id:
arxiv:
- '1104.0127'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1104.0127
month: '04'
oa: 1
oa_version: Preprint
page: '19'
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: submitted
publisher: ArXiv
publist_id: '3251'
status: public
title: The decidability frontier for probabilistic automata on infinite words
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3364'
abstract:
- lang: eng
text: Molecular noise, which arises from the randomness of the discrete events in
the cell, significantly influences fundamental biological processes. Discrete-state
continuous-time stochastic models (CTMC) can be used to describe such effects,
but the calculation of the probabilities of certain events is computationally
expensive. We present a comparison of two analysis approaches for CTMC. On one
hand, we estimate the probabilities of interest using repeated Gillespie simulation
and determine the statistical accuracy that we obtain. On the other hand, we apply
a numerical reachability analysis that approximates the probability distributions
of the system at several time instances. We use examples of cellular processes
to demonstrate the superiority of the reachability analysis if accurate results
are required.
article_processing_charge: No
author:
- first_name: Frédéric
full_name: Didier, Frédéric
last_name: Didier
- 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: Maria
full_name: Mateescu, Maria
last_name: Mateescu
- first_name: Verena
full_name: Wolf, Verena
last_name: Wolf
citation:
ama: Didier F, Henzinger TA, Mateescu M, Wolf V. Approximation of event probabilities
in noisy cellular processes. Theoretical Computer Science. 2011;412(21):2128-2141.
doi:10.1016/j.tcs.2010.10.022
apa: Didier, F., Henzinger, T. A., Mateescu, M., & Wolf, V. (2011). Approximation
of event probabilities in noisy cellular processes. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2010.10.022
chicago: Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf.
“Approximation of Event Probabilities in Noisy Cellular Processes.” Theoretical
Computer Science. Elsevier, 2011. https://doi.org/10.1016/j.tcs.2010.10.022.
ieee: F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Approximation of event
probabilities in noisy cellular processes,” Theoretical Computer Science,
vol. 412, no. 21. Elsevier, pp. 2128–2141, 2011.
ista: Didier F, Henzinger TA, Mateescu M, Wolf V. 2011. Approximation of event probabilities
in noisy cellular processes. Theoretical Computer Science. 412(21), 2128–2141.
mla: Didier, Frédéric, et al. “Approximation of Event Probabilities in Noisy Cellular
Processes.” Theoretical Computer Science, vol. 412, no. 21, Elsevier, 2011,
pp. 2128–41, doi:10.1016/j.tcs.2010.10.022.
short: F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, Theoretical Computer Science
412 (2011) 2128–2141.
date_created: 2018-12-11T12:02:55Z
date_published: 2011-05-06T00:00:00Z
date_updated: 2025-09-30T09:03:30Z
day: '06'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2010.10.022
external_id:
isi:
- '000290078000005'
file:
- access_level: open_access
checksum: e5503e25ce020d753e06b3431e16841e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:09Z
date_updated: 2020-07-14T12:46:10Z
file_id: '4862'
file_name: IST-2012-79-v1+1_Approximation_of_event_probabilities_in_noisy_cellular_processes.pdf
file_size: 230503
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 412'
isi: 1
issue: '21'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 2128 - 2141
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '3249'
pubrep_id: '79'
quality_controlled: '1'
related_material:
record:
- id: '4535'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Approximation of event probabilities in noisy cellular processes
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 412
year: '2011'
...
---
_id: '3365'
abstract:
- lang: eng
text: We present the tool Quasy, a quantitative synthesis tool. Quasy takes qualitative
and quantitative specifications and automatically constructs a system that satisfies
the qualitative specification and optimizes the quantitative specification, if
such a system exists. The user can choose between a system that satisfies and
optimizes the specifications (a) under all possible environment behaviors or (b)
under the most-likely environment behaviors given as a probability distribution
on the possible input sequences. Quasy solves these two quantitative synthesis
problems by reduction to instances of 2-player games and Markov Decision Processes
(MDPs) with quantitative winning objectives. Quasy can also be seen as a game
solver for quantitative games. Most notable, it can solve lexicographic mean-payoff
games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with
mean-payoff parity objectives.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. QUASY: quantitative synthesis
tool. In: Vol 6605. Springer; 2011:267-271. doi:10.1007/978-3-642-19835-9_24'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Singh, R. (2011). QUASY:
quantitative synthesis tool (Vol. 6605, pp. 267–271). Presented at the TACAS:
Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken,
Germany: Springer. https://doi.org/10.1007/978-3-642-19835-9_24'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
Singh. “QUASY: Quantitative Synthesis Tool,” 6605:267–71. Springer, 2011. https://doi.org/10.1007/978-3-642-19835-9_24.'
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “QUASY: quantitative
synthesis tool,” presented at the TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, Saarbrucken, Germany, 2011, vol. 6605, pp. 267–271.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2011. QUASY: quantitative
synthesis tool. TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, LNCS, vol. 6605, 267–271.'
mla: 'Chatterjee, Krishnendu, et al. QUASY: Quantitative Synthesis Tool.
Vol. 6605, Springer, 2011, pp. 267–71, doi:10.1007/978-3-642-19835-9_24.'
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2011,
pp. 267–271.
conference:
end_date: 2011-04-03
location: Saarbrucken, Germany
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2011-03-26
date_created: 2018-12-11T12:02:55Z
date_published: 2011-09-29T00:00:00Z
date_updated: 2021-01-12T07:42:58Z
day: '29'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-19835-9_24
file:
- access_level: open_access
checksum: 762e52eb296f6dbfbf2a75d98b8ebaee
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:37Z
date_updated: 2020-07-14T12:46:10Z
file_id: '5022'
file_name: IST-2012-77-v1+1_QUASY-_quantitative_synthesis_tool.pdf
file_size: 475661
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6605'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 267 - 271
publication_status: published
publisher: Springer
publist_id: '3248'
pubrep_id: '77'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'QUASY: quantitative synthesis tool'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6605
year: '2011'
...
---
_id: '3366'
abstract:
- lang: eng
text: 'We present an algorithmic method for the quantitative, performance-aware
synthesis of concurrent programs. The input consists of a nondeterministic partial
program and of a parametric performance model. The nondeterminism allows the programmer
to omit which (if any) synchronization construct is used at a particular program
location. The performance model, specified as a weighted automaton, can capture
system architectures by assigning different costs to actions such as locking,
context switching, and memory and cache accesses. The quantitative synthesis problem
is to automatically resolve the nondeterminism of the partial program so that
both correctness is guaranteed and performance is optimal. As is standard for
shared memory concurrency, correctness is formalized "specification free",
in particular as race freedom or deadlock freedom. For worst-case (average-case)
performance, we show that the problem can be reduced to 2-player graph games (with
probabilistic transitions) with quantitative objectives. While we show, using
game-theoretic methods, that the synthesis problem is Nexp-complete, we present
an algorithmic method and an implementation that works efficiently for concurrent
programs and performance models of practical interest. We have implemented a prototype
tool and used it to synthesize finite-state concurrent programs that exhibit different
programming patterns, for several performance models representing different architectures. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: 'Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. Quantitative
synthesis for concurrent programs. In: Gopalakrishnan G, Qadeer S, eds. Vol 6806.
Springer; 2011:243-259. doi:10.1007/978-3-642-22110-1_20'
apa: 'Cerny, P., Chatterjee, K., Henzinger, T. A., Radhakrishna, A., & Singh,
R. (2011). Quantitative synthesis for concurrent programs. In G. Gopalakrishnan
& S. Qadeer (Eds.) (Vol. 6806, pp. 243–259). Presented at the CAV: Computer
Aided Verification, Snowbird, USA: Springer. https://doi.org/10.1007/978-3-642-22110-1_20'
chicago: Cerny, Pavol, Krishnendu Chatterjee, Thomas A Henzinger, Arjun Radhakrishna,
and Rohit Singh. “Quantitative Synthesis for Concurrent Programs.” edited by Ganesh
Gopalakrishnan and Shaz Qadeer, 6806:243–59. Springer, 2011. https://doi.org/10.1007/978-3-642-22110-1_20.
ieee: 'P. Cerny, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh,
“Quantitative synthesis for concurrent programs,” presented at the CAV: Computer
Aided Verification, Snowbird, USA, 2011, vol. 6806, pp. 243–259.'
ista: 'Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. 2011. Quantitative
synthesis for concurrent programs. CAV: Computer Aided Verification, LNCS, vol.
6806, 243–259.'
mla: Cerny, Pavol, et al. Quantitative Synthesis for Concurrent Programs.
Edited by Ganesh Gopalakrishnan and Shaz Qadeer, vol. 6806, Springer, 2011, pp.
243–59, doi:10.1007/978-3-642-22110-1_20.
short: P. Cerny, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, R. Singh, in:,
G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 243–259.
conference:
end_date: 2011-07-20
location: Snowbird, USA
name: 'CAV: Computer Aided Verification'
start_date: 2011-07-14
corr_author: '1'
date_created: 2018-12-11T12:02:55Z
date_published: 2011-04-21T00:00:00Z
date_updated: 2024-10-21T06:03:04Z
day: '21'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-642-22110-1_20
ec_funded: 1
editor:
- first_name: Ganesh
full_name: Gopalakrishnan, Ganesh
last_name: Gopalakrishnan
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
file:
- access_level: open_access
checksum: c033689355f45742dc7c99b5af13ce7a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:51Z
date_updated: 2020-07-14T12:46:10Z
file_id: '5174'
file_name: IST-2012-76-v1+1_Quantitative_synthesis_for_concurrent_programs.pdf
file_size: 508946
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6806'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 243 - 259
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '3247'
pubrep_id: '76'
quality_controlled: '1'
related_material:
record:
- id: '5388'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Quantitative synthesis for concurrent programs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6806
year: '2011'
...
---
_id: '3381'
abstract:
- lang: eng
text: In this survey, we compare several languages for specifying Markovian population
models such as queuing networks and chemical reaction networks. All these languages
— matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic
process algebras, and guarded command models — describe continuous-time Markov
chains, but they differ according to important properties, such as compositionality,
expressiveness and succinctness, executability, and ease of use. Moreover, they
provide different support for checking the well-formedness of a model and for
analyzing a model.
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: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Verena
full_name: Wolf, Verena
last_name: Wolf
citation:
ama: 'Henzinger TA, Jobstmann B, Wolf V. Formalisms for specifying Markovian population
models. IJFCS: International Journal of Foundations of Computer Science.
2011;22(4):823-841. doi:10.1142/S0129054111008441'
apa: 'Henzinger, T. A., Jobstmann, B., & Wolf, V. (2011). Formalisms for specifying
Markovian population models. IJFCS: International Journal of Foundations of
Computer Science. World Scientific Publishing. https://doi.org/10.1142/S0129054111008441'
chicago: 'Henzinger, Thomas A, Barbara Jobstmann, and Verena Wolf. “Formalisms for
Specifying Markovian Population Models.” IJFCS: International Journal of Foundations
of Computer Science. World Scientific Publishing, 2011. https://doi.org/10.1142/S0129054111008441.'
ieee: 'T. A. Henzinger, B. Jobstmann, and V. Wolf, “Formalisms for specifying Markovian
population models,” IJFCS: International Journal of Foundations of Computer
Science, vol. 22, no. 4. World Scientific Publishing, pp. 823–841, 2011.'
ista: 'Henzinger TA, Jobstmann B, Wolf V. 2011. Formalisms for specifying Markovian
population models. IJFCS: International Journal of Foundations of Computer Science.
22(4), 823–841.'
mla: 'Henzinger, Thomas A., et al. “Formalisms for Specifying Markovian Population
Models.” IJFCS: International Journal of Foundations of Computer Science,
vol. 22, no. 4, World Scientific Publishing, 2011, pp. 823–41, doi:10.1142/S0129054111008441.'
short: 'T.A. Henzinger, B. Jobstmann, V. Wolf, IJFCS: International Journal of Foundations
of Computer Science 22 (2011) 823–841.'
date_created: 2018-12-11T12:03:00Z
date_published: 2011-06-01T00:00:00Z
date_updated: 2025-09-30T08:49:01Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1142/S0129054111008441
external_id:
isi:
- '000291552600005'
file:
- access_level: open_access
checksum: df88431872586c773fbcfea37d7b36a2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:45Z
date_updated: 2020-07-14T12:46:11Z
file_id: '4707'
file_name: IST-2016-628-v1+1_journals-ijfcs-HenzingerJW11.pdf
file_size: 222840
relation: main_file
file_date_updated: 2020-07-14T12:46:11Z
has_accepted_license: '1'
intvolume: ' 22'
isi: 1
issue: '4'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 823 - 841
publication: 'IJFCS: International Journal of Foundations of Computer Science'
publication_status: published
publisher: World Scientific Publishing
publist_id: '3226'
pubrep_id: '628'
quality_controlled: '1'
related_material:
record:
- id: '3841'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Formalisms for specifying Markovian population models
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 22
year: '2011'
...
---
_id: '3315'
abstract:
- lang: eng
text: We consider two-player games played in real time on game structures with clocks
where the objectives of players are described using parity conditions. The games
are concurrent in that at each turn, both players independently propose a time
delay and an action, and the action with the shorter delay is chosen. To prevent
a player from winning by blocking time, we restrict each player to play strategies
that ensure that the player cannot be responsible for causing a zeno run. First,
we present an efficient reduction of these games to turn-based (i.e., not concurrent)
finite-state (i.e., untimed) parity games. Our reduction improves the best known
complexity for solving timed parity games. Moreover, the rich class of algorithms
for classical parity games can now be applied to timed parity games. The states
of the resulting game are based on clock regions of the original game, and the
state space of the finite game is linear in the size of the region graph. Second,
we consider two restricted classes of strategies for the player that represents
the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust
winning strategies. Using a limit-robust winning strategy, the controller cannot
choose an exact real-valued time delay but must allow for some nonzero jitter
in each of its actions. If there is a given lower bound on the jitter, then the
strategy is bounded-robust winning. We show that exact strategies are more powerful
than limit-robust strategies, which are more powerful than bounded-robust winning
strategies for any bound. For both kinds of robust strategies, we present efficient
reductions to standard timed automaton games. These reductions provide algorithms
for the synthesis of robust real-time controllers.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: 'Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness.
Logical Methods in Computer Science. 2011;7(4). doi:10.2168/LMCS-7(4:8)2011'
apa: 'Chatterjee, K., Henzinger, T. A., & Prabhu, V. (2011). Timed parity games:
Complexity and robustness. Logical Methods in Computer Science. International
Federation for Computational Logic. https://doi.org/10.2168/LMCS-7(4:8)2011'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed
Parity Games: Complexity and Robustness.” Logical Methods in Computer Science.
International Federation for Computational Logic, 2011. https://doi.org/10.2168/LMCS-7(4:8)2011.'
ieee: 'K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity
and robustness,” Logical Methods in Computer Science, vol. 7, no. 4. International
Federation for Computational Logic, 2011.'
ista: 'Chatterjee K, Henzinger TA, Prabhu V. 2011. Timed parity games: Complexity
and robustness. Logical Methods in Computer Science. 7(4).'
mla: 'Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.”
Logical Methods in Computer Science, vol. 7, no. 4, International Federation
for Computational Logic, 2011, doi:10.2168/LMCS-7(4:8)2011.'
short: K. Chatterjee, T.A. Henzinger, V. Prabhu, Logical Methods in Computer Science
7 (2011).
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T12:02:37Z
date_published: 2011-12-14T00:00:00Z
date_updated: 2026-07-06T13:25:39Z
day: '14'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.2168/LMCS-7(4:8)2011
ec_funded: 1
file:
- access_level: open_access
checksum: 3480e1594bbef25ff7462fa93a8a814e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:42Z
date_updated: 2020-07-14T12:46:07Z
file_id: '5231'
file_name: IST-2016-86-v2+1_1011.0688_3_.pdf
file_size: 588863
relation: main_file
file_date_updated: 2020-07-14T12:46:07Z
has_accepted_license: '1'
intvolume: ' 7'
issue: '4'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation for Computational Logic
publist_id: '3324'
pubrep_id: '506'
quality_controlled: '1'
related_material:
record:
- id: '3876'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'Timed parity games: Complexity and robustness'
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2011'
...
---
_id: '3302'
abstract:
- lang: eng
text: Cloud computing aims to give users virtually unlimited pay-per-use computing
resources without the burden of managing the underlying infrastructure. We present
a new job execution environment Flextic that exploits scal- able static scheduling
techniques to provide the user with a flexible pricing model, such as a tradeoff
between dif- ferent degrees of execution speed and execution price, and at the
same time, reduce scheduling overhead for the cloud provider. We have evaluated
a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various
data parallel jobs from machine learning, im- age processing, and gene sequencing
that we considered, Flextic has low scheduling overhead and reduces job du- ration
by up to 15% compared to Hadoop, a dynamic cloud scheduler.
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: Anmol
full_name: Singh, Anmol
id: 72A86902-E99F-11E9-9F62-915534D1B916
last_name: Singh
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds.
In: 3rd USENIX Workshop on Hot Topics in Cloud Computing. Usenix Association;
2011:1-6.'
apa: 'Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011).
Static scheduling in clouds. In 3rd USENIX Workshop on Hot Topics in Cloud
Computing (pp. 1–6). Portland, OR, United States: Usenix Association.'
chicago: Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey.
“Static Scheduling in Clouds.” In 3rd USENIX Workshop on Hot Topics in Cloud
Computing, 1–6. Usenix Association, 2011.
ieee: T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling
in clouds,” in 3rd USENIX Workshop on Hot Topics in Cloud Computing, Portland,
OR, United States, 2011, pp. 1–6.
ista: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling
in clouds. 3rd USENIX Workshop on Hot Topics in Cloud Computing. HotCloud: Workshop
on Hot Topics in Cloud Computing, 1–6.'
mla: Henzinger, Thomas A., et al. “Static Scheduling in Clouds.” 3rd USENIX Workshop
on Hot Topics in Cloud Computing, Usenix Association, 2011, pp. 1–6.
short: T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, 3rd USENIX
Workshop on Hot Topics in Cloud Computing, Usenix Association, 2011, pp. 1–6.
conference:
end_date: 2011-06-15
location: Portland, OR, United States
name: 'HotCloud: Workshop on Hot Topics in Cloud Computing'
start_date: 2011-06-14
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T12:02:33Z
date_published: 2011-06-14T00:00:00Z
date_updated: 2026-07-07T06:07:16Z
day: '14'
ddc:
- '000'
- '005'
department:
- _id: ToHe
file:
- access_level: open_access
checksum: 21a461ac004bb535c83320fe79b30375
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:14Z
date_updated: 2020-07-14T12:46:06Z
file_id: '5333'
file_name: IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf
file_size: 232770
relation: main_file
file_date_updated: 2020-07-14T12:46:06Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 1 - 6
publication: 3rd USENIX Workshop on Hot Topics in Cloud Computing
publication_status: published
publisher: Usenix Association
publist_id: '3338'
pubrep_id: '90'
quality_controlled: '1'
status: public
title: Static scheduling in clouds
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3356'
abstract:
- lang: eng
text: There is recently a significant effort to add quantitative objectives to formal
verification and synthesis. We introduce and investigate the extension of temporal
logics with quantitative atomic assertions, aiming for a general and flexible
framework for quantitative-oriented specifications. In the heart of quantitative
objectives lies the accumulation of values along a computation. It is either the
accumulated summation, as with the energy objectives, or the accumulated average,
as with the mean-payoff objectives. We investigate the extension of temporal logics
with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is
a numeric variable of the system, c is a constant rational number, and Sum(v)
and Avg(v) denote the accumulated sum and average of the values of v from the
beginning of the computation up to the current point of time. We also allow the
path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring
to the average value along an entire computation. We study the border of decidability
for extensions of various temporal logics. In particular, we show that extending
the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by
prefix-accumulation assertions and extending LTL with path-accumulation assertions,
result in temporal logics whose model-checking problem is decidable. The extended
logics allow to significantly extend the currently known energy and mean-payoff
objectives. Moreover, the prefix-accumulation assertions may be refined with "controlled-accumulation",
allowing, for example, to specify constraints on the average waiting time between
a request and a grant. On the negative side, we show that the fragment we point
to is, in a sense, the maximal logic whose extension with prefix-accumulation
assertions permits a decidable model-checking procedure. Extending a temporal
logic that has the EG or EU modalities, and in particular CTL and LTL, makes the
problem undecidable.
article_number: '5970226'
article_processing_charge: No
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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
citation:
ama: 'Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications
with accumulative values. In: IEEE; 2011. doi:10.1109/LICS.2011.33'
apa: 'Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2011). Temporal
specifications with accumulative values. Presented at the LICS: Logic in Computer
Science, Toronto, Canada: IEEE. https://doi.org/10.1109/LICS.2011.33'
chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman.
“Temporal Specifications with Accumulative Values.” IEEE, 2011. https://doi.org/10.1109/LICS.2011.33.
ieee: 'U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications
with accumulative values,” presented at the LICS: Logic in Computer Science, Toronto,
Canada, 2011.'
ista: 'Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications
with accumulative values. LICS: Logic in Computer Science, 5970226.'
mla: Boker, Udi, et al. Temporal Specifications with Accumulative Values.
5970226, IEEE, 2011, doi:10.1109/LICS.2011.33.
short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, in:, IEEE, 2011.
conference:
end_date: 2011-06-24
location: Toronto, Canada
name: 'LICS: Logic in Computer Science'
start_date: 2011-06-21
date_created: 2018-12-11T12:02:52Z
date_published: 2011-06-21T00:00:00Z
date_updated: 2026-07-07T14:01:43Z
day: '21'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1109/LICS.2011.33
ec_funded: 1
external_id:
isi:
- '000297350400007'
file:
- access_level: open_access
checksum: 792128f5455f0f40f1105f0398e05fa9
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:42Z
date_updated: 2020-07-14T12:46:09Z
file_id: '4960'
file_name: IST-2012-83-v1+1_Temporal_specifications_with_accumulative_values.pdf
file_size: 225426
relation: main_file
file_date_updated: 2020-07-14T12:46:09Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: IEEE
publist_id: '3259'
pubrep_id: '83'
related_material:
record:
- id: '5385'
relation: earlier_version
status: public
- id: '2038'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Temporal specifications with accumulative values
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2011'
...
---
_id: '5385'
abstract:
- lang: eng
text: There is recently a significant effort to add quantitative objectives to formal
verification and synthesis. We introduce and investigate the extension of temporal
logics with quantitative atomic assertions, aiming for a general and flexible
framework for quantitative-oriented specifications. In the heart of quantitative
objectives lies the accumulation of values along a computation. It is either the
accumulated summation, as with the energy objectives, or the accumulated average,
as with the mean-payoff objectives. We investigate the extension of temporal logics
with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is
a numeric variable of the system, c is a constant rational number, and Sum(v)
and Avg(v) denote the accumulated sum and average of the values of v from the
beginning of the computation up to the current point of time. We also allow the
path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring
to the average value along an entire computation. We study the border of decidability
for extensions of various temporal logics. In particular, we show that extending
the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by
prefix-accumulation assertions and extending LTL with path-accumulation assertions,
result in temporal logics whose model-checking problem is decidable. The extended
logics allow to significantly extend the currently known energy and mean-payoff
objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”,
allowing, for example, to specify constraints on the average waiting time between
a request and a grant. On the negative side, we show that the fragment we point
to is, in a sense, the maximal logic whose extension with prefix-accumulation
assertions permits a decidable model-checking procedure. Extending a temporal
logic that has the EG or EU modalities, and in particular CTL and LTL, makes the
problem undecidable.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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
citation:
ama: Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal Specifications
with Accumulative Values. IST Austria; 2011. doi:10.15479/AT:IST-2011-0003
apa: Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2011). Temporal
specifications with accumulative values. IST Austria. https://doi.org/10.15479/AT:IST-2011-0003
chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman.
Temporal Specifications with Accumulative Values. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0003.
ieee: U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, Temporal specifications
with accumulative values. IST Austria, 2011.
ista: Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications
with accumulative values, IST Austria, 14p.
mla: Boker, Udi, et al. Temporal Specifications with Accumulative Values.
IST Austria, 2011, doi:10.15479/AT:IST-2011-0003.
short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications
with Accumulative Values, IST Austria, 2011.
date_created: 2018-12-12T11:39:02Z
date_published: 2011-04-04T00:00:00Z
date_updated: 2026-07-07T14:01:43Z
day: '04'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.15479/AT:IST-2011-0003
ec_funded: 1
file:
- access_level: open_access
checksum: 8491d0d48c4911620ecd5350b413c11e
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:00Z
date_updated: 2020-07-14T12:46:41Z
file_id: '5461'
file_name: IST-2011-0003_IST-2011-0003.pdf
file_size: 366281
relation: main_file
file_date_updated: 2020-07-14T12:46:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '14'
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '21'
related_material:
record:
- id: '3356'
relation: later_version
status: public
- id: '2038'
relation: later_version
status: public
status: public
title: Temporal specifications with accumulative values
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3353'
abstract:
- lang: eng
text: 'Compositional theories are crucial when designing large and complex systems
from smaller components. In this work we propose such a theory for synchronous
concurrent systems. Our approach follows so-called interface theories, which use
game-theoretic interpretations of composition and refinement. These are appropriate
for systems with distinct inputs and outputs, and explicit conditions on inputs
that must be enforced during composition. Our interfaces model systems that execute
in an infinite sequence of synchronous rounds. At each round, a contract must
be satisfied. The contract is simply a relation specifying the set of valid input/output
pairs. Interfaces can be composed by parallel, serial or feedback composition.
A refinement relation between interfaces is defined, and shown to have two main
properties: (1) it is preserved by composition, and (2) it is equivalent to substitutability,
namely, the ability to replace an interface by another one in any context. Shared
refinement and abstraction operators, corresponding to greatest lower and least
upper bounds with respect to refinement, are also defined. Input-complete interfaces,
that impose no restrictions on inputs, and deterministic interfaces, that produce
a unique output for any legal input, are discussed as special cases, and an interesting
duality between the two classes is exposed. A number of illustrative examples
are provided, as well as algorithms to compute compositions, check refinement,
and so on, for finite-state interfaces.'
article_number: '14'
article_processing_charge: No
author:
- first_name: Stavros
full_name: Tripakis, Stavros
last_name: Tripakis
- first_name: Ben
full_name: Lickly, Ben
last_name: Lickly
- 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: Edward
full_name: Lee, Edward
last_name: Lee
citation:
ama: Tripakis S, Lickly B, Henzinger TA, Lee E. A theory of synchronous relational
interfaces. ACM Transactions on Programming Languages and Systems. 2011;33(4).
doi:10.1145/1985342.1985345
apa: Tripakis, S., Lickly, B., Henzinger, T. A., & Lee, E. (2011). A theory
of synchronous relational interfaces. ACM Transactions on Programming Languages
and Systems. ACM. https://doi.org/10.1145/1985342.1985345
chicago: Tripakis, Stavros, Ben Lickly, Thomas A Henzinger, and Edward Lee. “A Theory
of Synchronous Relational Interfaces.” ACM Transactions on Programming Languages
and Systems. ACM, 2011. https://doi.org/10.1145/1985342.1985345.
ieee: S. Tripakis, B. Lickly, T. A. Henzinger, and E. Lee, “A theory of synchronous
relational interfaces,” ACM Transactions on Programming Languages and Systems,
vol. 33, no. 4. ACM, 2011.
ista: Tripakis S, Lickly B, Henzinger TA, Lee E. 2011. A theory of synchronous relational
interfaces. ACM Transactions on Programming Languages and Systems. 33(4), 14.
mla: Tripakis, Stavros, et al. “A Theory of Synchronous Relational Interfaces.”
ACM Transactions on Programming Languages and Systems, vol. 33, no. 4,
14, ACM, 2011, doi:10.1145/1985342.1985345.
short: S. Tripakis, B. Lickly, T.A. Henzinger, E. Lee, ACM Transactions on Programming
Languages and Systems 33 (2011).
das_tickbox: '1'
date_created: 2018-12-11T12:02:51Z
date_published: 2011-07-01T00:00:00Z
date_updated: 2026-07-07T14:03:34Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1145/1985342.1985345
ec_funded: 1
external_id:
isi:
- '000292766400003'
file:
- access_level: open_access
checksum: 5d44a8aa81e33210649beae507602138
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:45Z
date_updated: 2020-07-14T12:46:09Z
file_id: '5235'
file_name: IST-2012-85-v1+1_A_theory_of_synchronous_relational_interfaces.pdf
file_size: 775662
relation: main_file
file_date_updated: 2020-07-14T12:46:09Z
has_accepted_license: '1'
intvolume: ' 33'
isi: 1
issue: '4'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication: ACM Transactions on Programming Languages and Systems
publication_status: published
publisher: ACM
publist_id: '3263'
pubrep_id: '85'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A theory of synchronous relational interfaces
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 33
year: '2011'
...
---
_id: '3354'
abstract:
- lang: eng
text: 'We consider two-player games played on a finite state space for an infinite
number of rounds. The games are concurrent: in each round, the two players (player
1 and player 2) choose their moves independently and simultaneously; the current
state and the two moves determine the successor state. We consider ω-regular winning
conditions specified as parity objectives. Both players are allowed to use randomization
when choosing their moves. We study the computation of the limit-winning set of
states, consisting of the states where the sup-inf value of the game for player
1 is 1: in other words, a state is limit-winning if player 1 can ensure a probability
of winning arbitrarily close to 1. We show that the limit-winning set can be computed
in O(n2d+2) time, where n is the size of the game structure and 2d is the number
of priorities (or colors). The membership problem of whether a state belongs to
the limit-winning set can be decided in NP ∩ coNP. While this complexity is the
same as for the simpler class of turn-based parity games, where in each state
only one of the two players has a choice of moves, our algorithms are considerably
more involved than those for turn-based games. This is because concurrent games
do not satisfy two of the most fundamental properties of turn-based parity games.
First, in concurrent games limit-winning strategies require randomization; and
second, they require infinite memory.'
article_number: '28'
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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
citation:
ama: Chatterjee K, De Alfaro L, Henzinger TA. Qualitative concurrent parity games.
ACM Transactions on Computational Logic. 2011;12(4). doi:10.1145/1970398.1970404
apa: Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2011). Qualitative concurrent
parity games. ACM Transactions on Computational Logic. ACM. https://doi.org/10.1145/1970398.1970404
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Qualitative
Concurrent Parity Games.” ACM Transactions on Computational Logic. ACM,
2011. https://doi.org/10.1145/1970398.1970404.
ieee: K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Qualitative concurrent
parity games,” ACM Transactions on Computational Logic, vol. 12, no. 4.
ACM, 2011.
ista: Chatterjee K, De Alfaro L, Henzinger TA. 2011. Qualitative concurrent parity
games. ACM Transactions on Computational Logic. 12(4), 28.
mla: Chatterjee, Krishnendu, et al. “Qualitative Concurrent Parity Games.” ACM
Transactions on Computational Logic, vol. 12, no. 4, 28, ACM, 2011, doi:10.1145/1970398.1970404.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, ACM Transactions on Computational
Logic 12 (2011).
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T12:02:51Z
date_published: 2011-07-04T00:00:00Z
date_updated: 2026-07-07T14:02:38Z
day: '04'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/1970398.1970404
external_id:
isi:
- '000296202300006'
intvolume: ' 12'
isi: 1
issue: '4'
language:
- iso: eng
month: '07'
oa_version: None
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '3262'
quality_controlled: '1'
related_material:
record:
- id: '2054'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Qualitative concurrent parity games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12
year: '2011'
...
---
_id: '10908'
abstract:
- lang: eng
text: We present ABC, a software tool for automatically computing symbolic upper
bounds on the number of iterations of nested program loops. The system combines
static analysis of programs with symbolic summation techniques to derive loop
invariant relations between program variables. Iteration bounds are obtained from
the inferred invariants, by replacing variables with bounds on their greatest
values. We have successfully applied ABC to a large number of examples. The derived
symbolic bounds express non-trivial polynomial relations over loop variables.
We also report on results to automatically infer symbolic expressions over harmonic
numbers as upper bounds on loop iteration counts.
acknowledgement: This work was supported in part by the Swiss NSF. The fourth author
is supported by an FWF Hertha Firnberg Research grant (T425-N23).
article_processing_charge: No
author:
- first_name: Régis
full_name: Blanc, Régis
last_name: Blanc
- 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: Thibaud
full_name: Hottelier, Thibaud
last_name: Hottelier
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
citation:
ama: 'Blanc R, Henzinger TA, Hottelier T, Kovács L. ABC: Algebraic Bound Computation
for loops. In: Clarke EM, Voronkov A, eds. Logic for Programming, Artificial
Intelligence, and Reasoning. Vol 6355. LNCS. Berlin, Heidelberg: Springer
Nature; 2010:103-118. doi:10.1007/978-3-642-17511-4_7'
apa: 'Blanc, R., Henzinger, T. A., Hottelier, T., & Kovács, L. (2010). ABC:
Algebraic Bound Computation for loops. In E. M. Clarke & A. Voronkov (Eds.),
Logic for Programming, Artificial Intelligence, and Reasoning (Vol. 6355,
pp. 103–118). Berlin, Heidelberg: Springer Nature. https://doi.org/10.1007/978-3-642-17511-4_7'
chicago: 'Blanc, Régis, Thomas A Henzinger, Thibaud Hottelier, and Laura Kovács.
“ABC: Algebraic Bound Computation for Loops.” In Logic for Programming, Artificial
Intelligence, and Reasoning, edited by Edmund M Clarke and Andrei Voronkov,
6355:103–18. LNCS. Berlin, Heidelberg: Springer Nature, 2010. https://doi.org/10.1007/978-3-642-17511-4_7.'
ieee: 'R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, “ABC: Algebraic Bound
Computation for loops,” in Logic for Programming, Artificial Intelligence,
and Reasoning, Dakar, Senegal, 2010, vol. 6355, pp. 103–118.'
ista: 'Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound
Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning.
LPAR: Logic for Programming, Artificial Intelligence and ReasoningLNCS vol. 6355,
103–118.'
mla: 'Blanc, Régis, et al. “ABC: Algebraic Bound Computation for Loops.” Logic
for Programming, Artificial Intelligence, and Reasoning, edited by Edmund
M Clarke and Andrei Voronkov, vol. 6355, Springer Nature, 2010, pp. 103–18, doi:10.1007/978-3-642-17511-4_7.'
short: R. Blanc, T.A. Henzinger, T. Hottelier, L. Kovács, in:, E.M. Clarke, A. Voronkov
(Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer
Nature, Berlin, Heidelberg, 2010, pp. 103–118.
conference:
end_date: 2010-05-01
location: Dakar, Senegal
name: 'LPAR: Logic for Programming, Artificial Intelligence and Reasoning'
start_date: 2010-04-25
corr_author: '1'
date_created: 2022-03-21T08:14:35Z
date_published: 2010-05-01T00:00:00Z
date_updated: 2025-09-30T09:51:13Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-17511-4_7
editor:
- first_name: Edmund M
full_name: Clarke, Edmund M
last_name: Clarke
- first_name: Andrei
full_name: Voronkov, Andrei
last_name: Voronkov
external_id:
isi:
- '000309668000007'
intvolume: ' 6355'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://infoscience.epfl.ch/record/186096
month: '05'
oa: 1
oa_version: Submitted Version
page: 103-118
place: Berlin, Heidelberg
publication: Logic for Programming, Artificial Intelligence, and Reasoning
publication_identifier:
eisbn:
- '9783642175114'
eissn:
- 1611-3349
isbn:
- '9783642175107'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'ABC: Algebraic Bound Computation for loops'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6355
year: '2010'
...
---
_id: '4361'
abstract:
- lang: eng
text: Depth-bounded processes form the most expressive known fragment of the π-calculus
for which interesting verification problems are still decidable. In this paper
we develop an adequate domain of limits for the well-structured transition systems
that are induced by depth-bounded processes. An immediate consequence of our result
is that there exists a forward algorithm that decides the covering problem for
this class. Unlike backward algorithms, the forward algorithm terminates even
if the depth of the process is not known a priori. More importantly, our result
suggests a whole spectrum of forward algorithms that enable the effective verification
of a large class of mobile systems.
alternative_title:
- LNCS
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Wies T, Zufferey D, Henzinger TA. Forward analysis of depth-bounded processes.
In: Ong L, ed. Vol 6014. Springer; 2010:94-108. doi:10.1007/978-3-642-12032-9_8'
apa: 'Wies, T., Zufferey, D., & Henzinger, T. A. (2010). Forward analysis of
depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at
the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos,
Cyprus: Springer. https://doi.org/10.1007/978-3-642-12032-9_8'
chicago: Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis
of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010.
https://doi.org/10.1007/978-3-642-12032-9_8.
ieee: 'T. Wies, D. Zufferey, and T. A. Henzinger, “Forward analysis of depth-bounded
processes,” presented at the FoSSaCS: Foundations of Software Science and Computation
Structures, Paphos, Cyprus, 2010, vol. 6014, pp. 94–108.'
ista: 'Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded
processes. FoSSaCS: Foundations of Software Science and Computation Structures,
LNCS, vol. 6014, 94–108.'
mla: Wies, Thomas, et al. Forward Analysis of Depth-Bounded Processes. Edited
by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:10.1007/978-3-642-12032-9_8.
short: T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010,
pp. 94–108.
conference:
end_date: 2010-03-28
location: Paphos, Cyprus
name: 'FoSSaCS: Foundations of Software Science and Computation Structures'
start_date: 2010-03-20
corr_author: '1'
date_created: 2018-12-11T12:08:27Z
date_published: 2010-03-01T00:00:00Z
date_updated: 2026-04-09T14:35:23Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-12032-9_8
editor:
- first_name: Luke
full_name: Ong, Luke
last_name: Ong
file:
- access_level: open_access
checksum: 3e610de84937d821316362658239134a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:17Z
date_updated: 2020-07-14T12:46:27Z
file_id: '4677'
file_name: IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf
file_size: 240766
relation: main_file
file_date_updated: 2020-07-14T12:46:27Z
has_accepted_license: '1'
intvolume: ' 6014'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 94 - 108
publication_status: published
publisher: Springer
publist_id: '1099'
pubrep_id: '50'
quality_controlled: '1'
related_material:
record:
- id: '1405'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Forward analysis of depth-bounded processes
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6014
year: '2010'
...
---
_id: '4362'
abstract:
- lang: eng
text: Software transactional memories (STMs) promise simple and efficient concurrent
programming. Several correctness properties have been proposed for STMs. Based
on a bounded conflict graph algorithm for verifying correctness of STMs, we develop
TRACER, a tool for runtime verification of STM implementations. The novelty of
TRACER lies in the way it combines coarse and precise runtime analyses to guarantee
sound and complete verification in an efficient manner. We implement TRACER in
the TL2 STM implementation. We evaluate the performance of TRACER on STAMP benchmarks.
While a precise runtime verification technique based on conflict graphs results
in an average slowdown of 60x, the two-level approach of TRACER performs complete
verification with an average slowdown of around 25x across different benchmarks.
alternative_title:
- LNCS
author:
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Singh V. Runtime verification for software transactional memories. In: Sokolsky
O, Rosu G, Tilmann N, et al., eds. Vol 6418. Springer; 2010:421-435. doi:10.1007/978-3-642-16612-9_32'
apa: 'Singh, V. (2010). Runtime verification for software transactional memories.
In O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner,
… G. Pace (Eds.) (Vol. 6418, pp. 421–435). Presented at the RV: International
Conference on Runtime Verification, St. Julians, Malta: Springer. https://doi.org/10.1007/978-3-642-16612-9_32'
chicago: Singh, Vasu. “Runtime Verification for Software Transactional Memories.”
edited by Oleg Sokolsky, Grigore Rosu, Nikolai Tilmann, Howard Barringer, Ylies
Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, and Gordon Pace, 6418:421–35.
Springer, 2010. https://doi.org/10.1007/978-3-642-16612-9_32.
ieee: 'V. Singh, “Runtime verification for software transactional memories,” presented
at the RV: International Conference on Runtime Verification, St. Julians, Malta,
2010, vol. 6418, pp. 421–435.'
ista: 'Singh V. 2010. Runtime verification for software transactional memories.
RV: International Conference on Runtime Verification, LNCS, vol. 6418, 421–435.'
mla: Singh, Vasu. Runtime Verification for Software Transactional Memories.
Edited by Oleg Sokolsky et al., vol. 6418, Springer, 2010, pp. 421–35, doi:10.1007/978-3-642-16612-9_32.
short: V. Singh, in:, O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone,
B. Finkbeiner, K. Havelund, I. Lee, G. Pace (Eds.), Springer, 2010, pp. 421–435.
conference:
end_date: 2010-11-04
location: St. Julians, Malta
name: 'RV: International Conference on Runtime Verification'
start_date: 2010-11-01
corr_author: '1'
date_created: 2018-12-11T12:08:28Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2024-10-09T20:54:01Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-16612-9_32
editor:
- first_name: Oleg
full_name: Sokolsky, Oleg
last_name: Sokolsky
- first_name: Grigore
full_name: Rosu, Grigore
last_name: Rosu
- first_name: Nikolai
full_name: Tilmann, Nikolai
last_name: Tilmann
- first_name: Howard
full_name: Barringer, Howard
last_name: Barringer
- first_name: Ylies
full_name: Falcone, Ylies
last_name: Falcone
- first_name: Bernd
full_name: Finkbeiner, Bernd
last_name: Finkbeiner
- first_name: Klaus
full_name: Havelund, Klaus
last_name: Havelund
- first_name: Insup
full_name: Lee, Insup
last_name: Lee
- first_name: Gordon
full_name: Pace, Gordon
last_name: Pace
intvolume: ' 6418'
language:
- iso: eng
month: '01'
oa_version: None
page: 421 - 435
publication_status: published
publisher: Springer
publist_id: '1096'
quality_controlled: '1'
scopus_import: 1
status: public
title: Runtime verification for software transactional memories
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6418
year: '2010'
...
---
_id: '4369'
abstract:
- lang: eng
text: In this paper we propose a novel technique for constructing timed automata
from properties expressed in the logic mtl, under bounded-variability assumptions.
We handle full mtl and include all future operators. Our construction is based
on separation of the continuous time monitoring of the input sequence and discrete
predictions regarding the future. The separation of the continuous from the discrete
allows us to determinize our automata in an exponential construction that does
not increase the number of clocks. This leads to a doubly exponential construction
from mtl to deterministic timed automata, compared with triply exponential using
existing approaches. We offer an alternative to the existing approach to linear
real-time model checking, which has never been implemented. It further offers
a unified framework for model checking, runtime monitoring, and synthesis, in
an approach that can reuse tools, implementations, and insights from the discrete
setting.
alternative_title:
- LNCS
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Nickovic D, Piterman N. From MTL to deterministic timed automata. In: Henzinger
TA, Chatterjee K, eds. Vol 6246. Springer; 2010:152-167. doi:10.1007/978-3-642-15297-9_13'
apa: 'Nickovic, D., & Piterman, N. (2010). From MTL to deterministic timed automata.
In T. A. Henzinger & K. Chatterjee (Eds.) (Vol. 6246, pp. 152–167). Presented
at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg,
Austria: Springer. https://doi.org/10.1007/978-3-642-15297-9_13'
chicago: Nickovic, Dejan, and Nir Piterman. “From MTL to Deterministic Timed Automata.”
edited by Thomas A. Henzinger and Krishnendu Chatterjee, 6246:152–67. Springer,
2010. https://doi.org/10.1007/978-3-642-15297-9_13.
ieee: 'D. Nickovic and N. Piterman, “From MTL to deterministic timed automata,”
presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg,
Austria, 2010, vol. 6246, pp. 152–167.'
ista: 'Nickovic D, Piterman N. 2010. From MTL to deterministic timed automata. FORMATS:
Formal Modeling and Analysis of Timed Systems, LNCS, vol. 6246, 152–167.'
mla: Nickovic, Dejan, and Nir Piterman. From MTL to Deterministic Timed Automata.
Edited by Thomas A. Henzinger and Krishnendu Chatterjee, vol. 6246, Springer,
2010, pp. 152–67, doi:10.1007/978-3-642-15297-9_13.
short: D. Nickovic, N. Piterman, in:, T.A. Henzinger, K. Chatterjee (Eds.), Springer,
2010, pp. 152–167.
conference:
end_date: 2010-09-10
location: Klosterneuburg, Austria
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2010-09-08
corr_author: '1'
date_created: 2018-12-11T12:08:30Z
date_published: 2010-09-08T00:00:00Z
date_updated: 2024-10-09T20:54:01Z
day: '08'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15297-9_13
ec_funded: 1
editor:
- first_name: Thomas A.
full_name: Henzinger, Thomas A.
last_name: Henzinger
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
last_name: Chatterjee
file:
- access_level: open_access
checksum: b0ca5f5fbe8a3d20ccbc6f51a344a459
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:43Z
date_updated: 2020-07-14T12:46:27Z
file_id: '5028'
file_name: IST-2012-49-v1+1_From_MTL_to_deterministic_timed_automata.pdf
file_size: 249789
relation: main_file
file_date_updated: 2020-07-14T12:46:27Z
has_accepted_license: '1'
intvolume: ' 6246'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 152 - 167
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '1090'
pubrep_id: '49'
quality_controlled: '1'
scopus_import: 1
status: public
title: From MTL to deterministic timed automata
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6246
year: '2010'
...
---
_id: '4378'
abstract:
- lang: eng
text: 'Techniques such as verification condition generation, predicate abstraction,
and expressive type systems reduce software verification to proving formulas in
expressive logics. Programs and their specifications often make use of data structures
such as sets, multisets, algebraic data types, or graphs. Consequently, formulas
generated from verification also involve such data structures. To automate the
proofs of such formulas we propose a logic (a “calculus”) of such data structures.
We build the calculus by starting from decidable logics of individual data structures,
and connecting them through functions and sets, in ways that go beyond the frameworks
such as Nelson-Oppen. The result are new decidable logics that can simultaneously
specify properties of different kinds of data structures and overcome the limitations
of the individual logics. Several of our decidable logics include abstraction
functions that map a data structure into its more abstract view (a tree into a
multiset, a multiset into a set), into a numerical quantity (the size or the height),
or into the truth value of a candidate data structure invariant (sortedness, or
the heap property). For algebraic data types, we identify an asymptotic many-to-one
condition on the abstraction function that guarantees the existence of a decision
procedure. In addition to the combination based on abstraction functions, we can
combine multiple data structure theories if they all reduce to the same data structure
logic. As an instance of this approach, we describe a decidable logic whose formulas
are propositional combinations of formulas in: weak monadic second-order logic
of two successors, two-variable logic with counting, multiset algebra with Presburger
arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the
logic of algebraic data types with the set content function. The subformulas in
this combination can share common variables that refer to sets of objects along
with the common set algebra operations. Such sound and complete combination is
possible because the relations on sets definable in the component logics are all
expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic
and its new extensions play an important role in our decidability results. In
several cases, when we combine logics that belong to NP, we can prove the satisfiability
for the combined logic is still in NP.'
alternative_title:
- LNCS
author:
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Philippe
full_name: Suter, Philippe
last_name: Suter
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Kuncak V, Piskac R, Suter P, Wies T. Building a calculus of data structures.
In: Barthe G, Hermenegildo M, eds. Vol 5944. Springer; 2010:26-44. doi:10.1007/978-3-642-11319-2_6'
apa: 'Kuncak, V., Piskac, R., Suter, P., & Wies, T. (2010). Building a calculus
of data structures. In G. Barthe & M. Hermenegildo (Eds.) (Vol. 5944, pp.
26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
Madrid, Spain: Springer. https://doi.org/10.1007/978-3-642-11319-2_6'
chicago: Kuncak, Viktor, Ruzica Piskac, Philippe Suter, and Thomas Wies. “Building
a Calculus of Data Structures.” edited by Gilles Barthe and Manuel Hermenegildo,
5944:26–44. Springer, 2010. https://doi.org/10.1007/978-3-642-11319-2_6.
ieee: 'V. Kuncak, R. Piskac, P. Suter, and T. Wies, “Building a calculus of data
structures,” presented at the VMCAI: Verification, Model Checking and Abstract
Interpretation, Madrid, Spain, 2010, vol. 5944, pp. 26–44.'
ista: 'Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944,
26–44.'
mla: Kuncak, Viktor, et al. Building a Calculus of Data Structures. Edited
by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44,
doi:10.1007/978-3-642-11319-2_6.
short: V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo
(Eds.), Springer, 2010, pp. 26–44.
conference:
end_date: 2010-01-19
location: Madrid, Spain
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2010-01-17
date_created: 2018-12-11T12:08:33Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:31Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-11319-2_6
editor:
- first_name: Gilles
full_name: Barthe, Gilles
last_name: Barthe
- first_name: Manuel
full_name: Hermenegildo, Manuel
last_name: Hermenegildo
intvolume: ' 5944'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://infoscience.epfl.ch/record/161290/
month: '01'
oa: 1
oa_version: Submitted Version
page: 26 - 44
publication_status: published
publisher: Springer
publist_id: '1081'
quality_controlled: '1'
scopus_import: 1
status: public
title: Building a calculus of data structures
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 5944
year: '2010'
...
---
_id: '4380'
abstract:
- lang: eng
text: Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing
resources, while leaving the burden of managing the computing infrastructure to
the cloud provider. We present a new programming and pricing model that gives
the cloud user the flexibility of trading execution speed and price on a per-job
basis. We discuss the scheduling and resource management challenges for the cloud
provider that arise in the implementation of this model. We argue that techniques
from real-time and embedded software can be useful in this context.
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: Anmol
full_name: Tomar, Anmol
id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87
last_name: Tomar
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud
resources. In: ACM; 2010:1-8. doi:10.1145/1879021.1879022'
apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010).
A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded
Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022'
chicago: Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey.
“A Marketplace for Cloud Resources,” 1–8. ACM, 2010. https://doi.org/10.1145/1879021.1879022.
ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace
for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA,
2010, pp. 1–8.'
ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for
cloud resources. EMSOFT: Embedded Software , 1–8.'
mla: Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM,
2010, pp. 1–8, doi:10.1145/1879021.1879022.
short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010,
pp. 1–8.
conference:
end_date: 2010-10-29
location: Arizona, USA
name: 'EMSOFT: Embedded Software '
start_date: 2010-10-24
corr_author: '1'
date_created: 2018-12-11T12:08:33Z
date_published: 2010-10-24T00:00:00Z
date_updated: 2024-10-09T20:54:01Z
day: '24'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/1879021.1879022
file:
- access_level: open_access
checksum: 7680dd24016810710f7c977bc94f85e9
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:42Z
date_updated: 2020-07-14T12:46:28Z
file_id: '4767'
file_name: IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf
file_size: 222626
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 1 - 8
publication_status: published
publisher: ACM
publist_id: '1078'
pubrep_id: '48'
quality_controlled: '1'
scopus_import: 1
status: public
title: A marketplace for cloud resources
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4381'
abstract:
- lang: eng
text: Cloud computing aims to give users virtually unlimited pay-per-use computing
resources without the burden of managing the underlying infrastructure. We claim
that, in order to realize the full potential of cloud computing, the user must
be presented with a pricing model that offers flexibility at the requirements
level, such as a choice between different degrees of execution speed and the cloud
provider must be presented with a programming model that offers flexibility at
the execution level, such as a choice between different scheduling policies. In
such a flexible framework, with each job, the user purchases a virtual computer
with the desired speed and cost characteristics, and the cloud provider can optimize
the utilization of resources across a stream of jobs from different users. We
designed a flexible framework to test our hypothesis, which is called FlexPRICE
(Flexible Provisioning of Resources in a Cloud Environment) and works as follows.
A user presents a job to the cloud. The cloud finds different schedules to execute
the job and presents a set of quotes to the user in terms of price and duration
for the execution. The user then chooses a particular quote and the cloud is obliged
to execute the job according to the chosen quote. FlexPRICE thus hides the complexity
of the actual scheduling decisions from the user, but still provides enough flexibility
to meet the users actual demands. We implemented FlexPRICE in a simulator called
PRICES that allows us to experiment with our framework. We observe that FlexPRICE
provides a wide range of execution options-from fast and expensive to slow and
cheap-- for the whole spectrum of data-intensive and computation-intensive jobs.
We also observe that the set of quotes computed by FlexPRICE do not vary as the
number of simultaneous jobs increases.
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: Anmol
full_name: Tomar, Anmol
id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87
last_name: Tomar
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning
of resources in a cloud environment. In: IEEE; 2010:83-90. doi:10.1109/CLOUD.2010.71'
apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010).
FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90).
Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71'
chicago: 'Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien
Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,”
83–90. IEEE, 2010. https://doi.org/10.1109/CLOUD.2010.71.'
ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE:
Flexible provisioning of resources in a cloud environment,” presented at the CLOUD:
Cloud Computing, Miami, USA, 2010, pp. 83–90.'
ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible
provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.'
mla: 'Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources
in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.'
short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010,
pp. 83–90.
conference:
end_date: 2010-07-10
location: Miami, USA
name: 'CLOUD: Cloud Computing'
start_date: 2010-07-05
corr_author: '1'
date_created: 2018-12-11T12:08:33Z
date_published: 2010-08-26T00:00:00Z
date_updated: 2024-10-09T20:54:00Z
day: '26'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1109/CLOUD.2010.71
file:
- access_level: open_access
checksum: 98e534675339a8e2beca08890d048145
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:03Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5188'
file_name: IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf
file_size: 467436
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 83 - 90
publication_status: published
publisher: IEEE
publist_id: '1077'
pubrep_id: '47'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'FlexPRICE: Flexible provisioning of resources in a cloud environment'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4382'
abstract:
- lang: eng
text: 'Transactional memory (TM) has shown potential to simplify the task of writing
concurrent programs. Inspired by classical work on databases, formal definitions
of the semantics of TM executions have been proposed. Many of these definitions
assumed that accesses to shared data are solely performed through transactions.
In practice, due to legacy code and concurrency libraries, transactions in a TM
have to share data with non-transactional operations. The semantics of such interaction,
while widely discussed by practitioners, lacks a clear formal specification. Those
interactions can vary, sometimes in subtle ways, between TM implementations and
underlying memory models. We propose a correctness condition for TMs, parametrized
opacity, to formally capture the now folklore notion of strong atomicity by stipulating
the two following intuitive requirements: first, every transaction appears as
if it is executed instantaneously with respect to other transactions and non-transactional
operations, and second, non-transactional operations conform to the given underlying
memory model. We investigate the inherent cost of implementing parametrized opacity.
We first prove that parametrized opacity requires either instrumenting non-transactional
operations (for most memory models) or writing to memory by transactions using
potentially expensive read-modify-write instructions (such as compare-and-swap).
Then, we show that for a class of practical relaxed memory models, parametrized
opacity can indeed be implemented with constant-time instrumentation of non-transactional
writes and no instrumentation of non-transactional reads. We show that, in practice,
parametrizing the notion of correctness allows developing more efficient TM implementations.'
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- 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: Michal
full_name: Kapalka, Michal
last_name: Kapalka
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. Transactions in the jungle.
In: ACM; 2010:263-272. doi:10.1145/1810479.1810529'
apa: 'Guerraoui, R., Henzinger, T. A., Kapalka, M., & Singh, V. (2010). Transactions
in the jungle (pp. 263–272). Presented at the SPAA: ACM Symposium on Parallel
Algorithms and Architectures, Santorini, Greece: ACM. https://doi.org/10.1145/1810479.1810529'
chicago: Guerraoui, Rachid, Thomas A Henzinger, Michal Kapalka, and Vasu Singh.
“Transactions in the Jungle,” 263–72. ACM, 2010. https://doi.org/10.1145/1810479.1810529.
ieee: 'R. Guerraoui, T. A. Henzinger, M. Kapalka, and V. Singh, “Transactions in
the jungle,” presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures,
Santorini, Greece, 2010, pp. 263–272.'
ista: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. 2010. Transactions in the
jungle. SPAA: ACM Symposium on Parallel Algorithms and Architectures, 263–272.'
mla: Guerraoui, Rachid, et al. Transactions in the Jungle. ACM, 2010, pp.
263–72, doi:10.1145/1810479.1810529.
short: R. Guerraoui, T.A. Henzinger, M. Kapalka, V. Singh, in:, ACM, 2010, pp. 263–272.
conference:
end_date: 2010-06-15
location: Santorini, Greece
name: 'SPAA: ACM Symposium on Parallel Algorithms and Architectures'
start_date: 2010-06-13
date_created: 2018-12-11T12:08:34Z
date_published: 2010-06-13T00:00:00Z
date_updated: 2024-10-21T06:03:05Z
day: '13'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/1810479.1810529
file:
- access_level: open_access
checksum: f2ad6c00a6304da34bf21bcdcfd36c4b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:28Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5080'
file_name: IST-2012-46-v1+1_Transactions_in_the_jungle.pdf
file_size: 246409
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 263 - 272
publication_status: published
publisher: ACM
publist_id: '1076'
pubrep_id: '46'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Transactions in the jungle
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...