---
_id: '1731'
abstract:
- lang: eng
text: 'We consider two-player zero-sum games on graphs. These games can be classified
on the basis of the information of the players and on the mode of interaction
between them. On the basis of information the classification is as follows: (a)
partial-observation (both players have partial view of the game); (b) one-sided
complete-observation (one player has complete observation); and (c) complete-observation
(both players have complete view of the game). On the basis of mode of interaction
we have the following classification: (a) concurrent (both players interact simultaneously);
and (b) turn-based (both players interact in turn). The two sources of randomness
in these games are randomness in transition function and randomness in strategies.
In general, randomized strategies are more powerful than deterministic strategies,
and randomness in transitions gives more general classes of games. In this work
we present a complete characterization for the classes of games where randomness
is not helpful in: (a) the transition function probabilistic transition can be
simulated by deterministic transition); and (b) strategies (pure strategies are
as powerful as randomized strategies). As consequence of our characterization
we obtain new undecidability results for these games. '
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Hugo
full_name: Gimbert, Hugo
last_name: Gimbert
- 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, Doyen L, Gimbert H, Henzinger TA. Randomness for free. Information
and Computation. 2015;245(12):3-16. doi:10.1016/j.ic.2015.06.003
apa: Chatterjee, K., Doyen, L., Gimbert, H., & Henzinger, T. A. (2015). Randomness
for free. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.06.003
chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger.
“Randomness for Free.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.06.003.
ieee: K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for
free,” Information and Computation, vol. 245, no. 12. Elsevier, pp. 3–16,
2015.
ista: Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free.
Information and Computation. 245(12), 3–16.
mla: Chatterjee, Krishnendu, et al. “Randomness for Free.” Information and Computation,
vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:10.1016/j.ic.2015.06.003.
short: K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation
245 (2015) 3–16.
corr_author: '1'
date_created: 2018-12-11T11:53:42Z
date_published: 2015-12-01T00:00:00Z
date_updated: 2025-09-23T10:32:00Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2015.06.003
ec_funded: 1
external_id:
arxiv:
- '1006.0673'
isi:
- '000368899100002'
intvolume: ' 245'
isi: 1
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1006.0673
month: '12'
oa: 1
oa_version: Preprint
page: 3 - 16
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '5395'
quality_controlled: '1'
related_material:
record:
- id: '3856'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Randomness for free
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 245
year: '2015'
...
---
OA_place: publisher
OA_type: free access
_id: '3249'
abstract:
- lang: eng
text: Boolean notions of correctness are formalized by preorders on systems. Quantitative
measures of correctness can be formalized by real-valued distance functions between
systems, where the distance between implementation and specification provides
a measure of "fit" or "desirability". We extend the simulation
preorder to the quantitative setting by making each player of a simulation game
pay a certain price for her choices. We use the resulting games with quantitative
objectives to define three different simulation distances. The correctness distance
measures how much the specification must be changed in order to be satisfied by
the implementation. The coverage distance measures how much the implementation
restricts the degrees of freedom offered by the specification. The robustness
distance measures how much a system can deviate from the implementation description
without violating the specification. We consider these distances for safety as
well as liveness specifications. The distances can be computed in polynomial time
for safety specifications, and for liveness specifications given by weak fairness
constraints. We show that the distance functions satisfy the triangle inequality,
that the distance between two systems does not increase under parallel composition
with a third system, and that the distance between two systems can be bounded
from above and below by distances between abstractions of the two systems. These
properties suggest that our simulation distances provide an appropriate basis
for a quantitative theory of discrete systems. We also demonstrate how the robustness
distance can be used to measure how many transmission errors are tolerated by
error correcting codes.
acknowledgement: This work was partially supported by the ERC Advanced Grant QUAREM,
the FWF NFN Grant S11402-N23 (RiSE), the European Union project COMBEST and the
European Network of Excellence Artist Design.
article_processing_charge: No
article_type: original
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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
citation:
ama: Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. Theoretical
Computer Science. 2012;413(1):21-35. doi:10.1016/j.tcs.2011.08.002
apa: Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2012). Simulation distances.
Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2011.08.002
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances.”
Theoretical Computer Science. Elsevier, 2012. https://doi.org/10.1016/j.tcs.2011.08.002.
ieee: P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” Theoretical
Computer Science, vol. 413, no. 1. Elsevier, pp. 21–35, 2012.
ista: Cerny P, Henzinger TA, Radhakrishna A. 2012. Simulation distances. Theoretical
Computer Science. 413(1), 21–35.
mla: Cerny, Pavol, et al. “Simulation Distances.” Theoretical Computer Science,
vol. 413, no. 1, Elsevier, 2012, pp. 21–35, doi:10.1016/j.tcs.2011.08.002.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 413
(2012) 21–35.
corr_author: '1'
date_created: 2018-12-11T12:02:15Z
date_published: 2012-01-06T00:00:00Z
date_updated: 2025-09-30T07:46:06Z
day: '06'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2011.08.002
ec_funded: 1
external_id:
isi:
- '000298529200003'
intvolume: ' 413'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.tcs.2011.08.002
month: '01'
oa: 1
oa_version: Published Version
page: 21 - 35
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '3408'
pubrep_id: '42'
quality_controlled: '1'
related_material:
record:
- id: '5389'
relation: earlier_version
status: public
- id: '4393'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Simulation distances
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 413
year: '2012'
...
---
_id: '3316'
abstract:
- lang: eng
text: In addition to being correct, a system should be robust, that is, it should
behave reasonably even after receiving unexpected inputs. In this paper, we summarize
two formal notions of robustness that we have introduced previously for reactive
systems. One of the notions is based on assigning costs for failures on a user-provided
notion of incorrect transitions in a specification. Here, we define a system to
be robust if a finite number of incorrect inputs does not lead to an infinite
number of incorrect outputs. We also give a more refined notion of robustness
that aims to minimize the ratio of output failures to input failures. The second
notion is aimed at liveness. In contrast to the previous notion, it has no concept
of recovery from an error. Instead, it compares the ratio of the number of liveness
constraints that the system violates to the number of liveness constraints that
the environment violates.
article_processing_charge: No
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Karin
full_name: Greimel, Karin
last_name: Greimel
- 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
citation:
ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered
robustness. In: 6th IEEE International Symposium on Industrial and Embedded
Systems. IEEE; 2011:176-185. doi:10.1109/SIES.2011.5953660'
apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann,
B. (2011). Specification-centered robustness. In 6th IEEE International Symposium
on Industrial and Embedded Systems (pp. 176–185). Vasteras, Sweden: IEEE.
https://doi.org/10.1109/SIES.2011.5953660'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger,
and Barbara Jobstmann. “Specification-Centered Robustness.” In 6th IEEE International
Symposium on Industrial and Embedded Systems, 176–85. IEEE, 2011. https://doi.org/10.1109/SIES.2011.5953660.
ieee: R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered
robustness,” in 6th IEEE International Symposium on Industrial and Embedded
Systems, Vasteras, Sweden, 2011, pp. 176–185.
ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered
robustness. 6th IEEE International Symposium on Industrial and Embedded Systems.
SIES: International Symposium on Industrial Embedded Systems, 176–185.'
mla: Bloem, Roderick, et al. “Specification-Centered Robustness.” 6th IEEE International
Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–85, doi:10.1109/SIES.2011.5953660.
short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th
IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp.
176–185.
conference:
end_date: 2011-06-17
location: Vasteras, Sweden
name: 'SIES: International Symposium on Industrial Embedded Systems'
start_date: 2011-06-15
date_created: 2018-12-11T12:02:38Z
date_published: 2011-07-14T00:00:00Z
date_updated: 2025-07-10T11:52:29Z
day: '14'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/SIES.2011.5953660
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse
month: '07'
oa: 1
oa_version: Published Version
page: 176 - 185
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _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: 6th IEEE International Symposium on Industrial and Embedded Systems
publication_status: published
publisher: IEEE
publist_id: '3323'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Specification-centered robustness
type: conference
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 (TOPLAS).
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 (TOPLAS). 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 (TOPLAS). 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
(TOPLAS), 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 (TOPLAS). 33(4),
14.
mla: Tripakis, Stavros, et al. “A Theory of Synchronous Relational Interfaces.”
ACM Transactions on Programming Languages and Systems (TOPLAS), 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 (TOPLAS) 33 (2011).
date_created: 2018-12-11T12:02:51Z
date_published: 2011-07-01T00:00:00Z
date_updated: 2025-09-30T09:05:52Z
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 (TOPLAS)
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 33
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: 2025-09-30T09:27:30Z
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: '3359'
abstract:
- lang: eng
text: "Motivated by improvements in constraint-solving technology and by the increase
of routinely available computational power, partial-program synthesis is emerging
as an effective approach for increasing programmer productivity. The goal of the
approach is to allow the programmer to specify a part of her intent imperatively
(that is, give a partial program) and a part of her intent declaratively, by specifying
which conditions need to be achieved or maintained. The task of the synthesizer
is to construct a program that satisfies the specification. As an example, consider
a partial program where threads access shared data without using any synchronization
mechanism, and a declarative specification that excludes data races and deadlocks.
The task of the synthesizer is then to place locks into the program code in order
for the program to meet the specification.\r\n\r\nIn this paper, we argue that
quantitative objectives are needed in partial-program synthesis in order to produce
higher-quality programs, while enabling simpler specifications. Returning to the
example, the synthesizer could construct a naive solution that uses one global
lock for shared data. This can be prevented either by constraining the solution
space further (which is error-prone and partly defeats the point of synthesis),
or by optimizing a quantitative objective that models performance. Other quantitative
notions useful in synthesis include fault tolerance, robustness, resource (memory,
power) consumption, and information flow."
acknowledgement: This work was partially supported by the ERC Advanced Grant QUAREM,
the FWF NFN Grant S11402-N23 (RiSE), and the EU NOE Grant ArtistDesign.
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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: 'Cerny P, Henzinger TA. From boolean to quantitative synthesis. In: ACM; 2011:149-154.
doi:10.1145/2038642.2038666'
apa: 'Cerny, P., & Henzinger, T. A. (2011). From boolean to quantitative synthesis
(pp. 149–154). Presented at the EMSOFT: Embedded Software , Taipei; Taiwan: ACM.
https://doi.org/10.1145/2038642.2038666'
chicago: Cerny, Pavol, and Thomas A Henzinger. “From Boolean to Quantitative Synthesis,”
149–54. ACM, 2011. https://doi.org/10.1145/2038642.2038666.
ieee: 'P. Cerny and T. A. Henzinger, “From boolean to quantitative synthesis,” presented
at the EMSOFT: Embedded Software , Taipei; Taiwan, 2011, pp. 149–154.'
ista: 'Cerny P, Henzinger TA. 2011. From boolean to quantitative synthesis. EMSOFT:
Embedded Software , 149–154.'
mla: Cerny, Pavol, and Thomas A. Henzinger. From Boolean to Quantitative Synthesis.
ACM, 2011, pp. 149–54, doi:10.1145/2038642.2038666.
short: P. Cerny, T.A. Henzinger, in:, ACM, 2011, pp. 149–154.
conference:
end_date: 2011-10-14
location: Taipei; Taiwan
name: 'EMSOFT: Embedded Software '
start_date: 2011-10-09
corr_author: '1'
date_created: 2018-12-11T12:02:53Z
date_published: 2011-10-09T00:00:00Z
date_updated: 2024-10-21T06:03:04Z
day: '09'
department:
- _id: ToHe
doi: 10.1145/2038642.2038666
ec_funded: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 149 - 154
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: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: ACM
publist_id: '3256'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From boolean to quantitative synthesis
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3360'
abstract:
- lang: eng
text: 'A discounted-sum automaton (NDA) is a nondeterministic finite automaton with
edge weights, which values a run by the discounted sum of visited edge weights.
More precisely, the weight in the i-th position of the run is divided by lambda^i,
where the discount factor lambda is a fixed rational number greater than 1. Discounted
summation is a common and useful measuring scheme, especially for infinite sequences,
which reflects the assumption that earlier weights are more important than later
weights. Determinizing automata is often essential, for example, in formal verification,
where there are polynomial algorithms for comparing two deterministic NDAs, while
the equivalence problem for NDAs is not known to be decidable. Unfortunately,
however, discounted-sum automata are, in general, not determinizable: it is currently
known that for every rational discount factor 1 < lambda < 2, there is an
NDA with lambda (denoted lambda-NDA) that cannot be determinized. We provide positive
news, showing that every NDA with an integral factor is determinizable. We also
complete the picture by proving that the integers characterize exactly the discount
factors that guarantee determinizability: we show that for every non-integral
rational factor lambda, there is a nondeterminizable lambda-NDA. Finally, we prove
that the class of NDAs with integral discount factors enjoys closure under the
algebraic operations min, max, addition, and subtraction, which is not the case
for general NDAs nor for deterministic NDAs. This shows that for integral discount
factors, the class of NDAs forms an attractive specification formalism in quantitative
formal verification. All our results hold equally for automata over finite words
and for automata over infinite words. '
alternative_title:
- LIPIcs
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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: 'Boker U, Henzinger TA. Determinizing discounted-sum automata. In: Vol 12.
Springer; 2011:82-96. doi:10.4230/LIPIcs.CSL.2011.82'
apa: 'Boker, U., & Henzinger, T. A. (2011). Determinizing discounted-sum automata
(Vol. 12, pp. 82–96). Presented at the CSL: Computer Science Logic, Bergen, Norway:
Springer. https://doi.org/10.4230/LIPIcs.CSL.2011.82'
chicago: Boker, Udi, and Thomas A Henzinger. “Determinizing Discounted-Sum Automata,”
12:82–96. Springer, 2011. https://doi.org/10.4230/LIPIcs.CSL.2011.82.
ieee: 'U. Boker and T. A. Henzinger, “Determinizing discounted-sum automata,” presented
at the CSL: Computer Science Logic, Bergen, Norway, 2011, vol. 12, pp. 82–96.'
ista: 'Boker U, Henzinger TA. 2011. Determinizing discounted-sum automata. CSL:
Computer Science Logic, LIPIcs, vol. 12, 82–96.'
mla: Boker, Udi, and Thomas A. Henzinger. Determinizing Discounted-Sum Automata.
Vol. 12, Springer, 2011, pp. 82–96, doi:10.4230/LIPIcs.CSL.2011.82.
short: U. Boker, T.A. Henzinger, in:, Springer, 2011, pp. 82–96.
conference:
end_date: 2011-09-15
location: Bergen, Norway
name: 'CSL: Computer Science Logic'
start_date: 2011-09-12
date_created: 2018-12-11T12:02:53Z
date_published: 2011-08-31T00:00:00Z
date_updated: 2021-01-12T07:42:56Z
day: '31'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CSL.2011.82
ec_funded: 1
file:
- access_level: open_access
checksum: 250603c6be8ccad4fbd4d7b24221f0ee
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:17Z
date_updated: 2020-07-14T12:46:10Z
file_id: '4803'
file_name: IST-2012-82-v1+1_Determinizing_discounted-sum_automata.pdf
file_size: 504270
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 12'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 82 - 96
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
publication_status: published
publisher: Springer
publist_id: '3255'
pubrep_id: '82'
quality_controlled: '1'
scopus_import: 1
status: public
title: Determinizing discounted-sum automata
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12
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: '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: '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: 2025-09-30T09:27:29Z
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: '2038'
relation: later_version
status: public
- id: '3356'
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: '3853'
abstract:
- lang: eng
text: 'Quantitative languages are an extension of boolean languages that assign
to each word a real number. Mean-payoff automata are finite automata with numerical
weights on transitions that assign to each infinite path the long-run average
of the transition weights. When the mode of branching of the automaton is deterministic,
nondeterministic, or alternating, the corresponding class of quantitative languages
is not robust as it is not closed under the pointwise operations of max, min,
sum, and numerical complement. Nondeterministic and alternating mean-payoff automata
are not decidable either, as the quantitative generalization of the problems of
universality and language inclusion is undecidable. We introduce a new class of
quantitative languages, defined by mean-payoff automaton expressions, which is
robust and decidable: it is closed under the four pointwise operations, and we
show that all decision problems are decidable for this class. Mean-payoff automaton
expressions subsume deterministic meanpayoff automata, and we show that they have
expressive power incomparable to nondeterministic and alternating mean-payoff
automata. We also present for the first time an algorithm to compute distance
between two quantitative languages, and in our case the quantitative languages
are given as mean-payoff automaton expressions.'
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- 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: Philippe
full_name: Rannou, Philippe
last_name: Rannou
citation:
ama: 'Chatterjee K, Doyen L, Edelsbrunner H, Henzinger TA, Rannou P. Mean-payoff
automaton expressions. In: Vol 6269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2010:269-283. doi:10.1007/978-3-642-15375-4_19'
apa: 'Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T. A., & Rannou,
P. (2010). Mean-payoff automaton expressions (Vol. 6269, pp. 269–283). Presented
at the CONCUR: Concurrency Theory, Paris, France: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.1007/978-3-642-15375-4_19'
chicago: Chatterjee, Krishnendu, Laurent Doyen, Herbert Edelsbrunner, Thomas A Henzinger,
and Philippe Rannou. “Mean-Payoff Automaton Expressions,” 6269:269–83. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_19.
ieee: 'K. Chatterjee, L. Doyen, H. Edelsbrunner, T. A. Henzinger, and P. Rannou,
“Mean-payoff automaton expressions,” presented at the CONCUR: Concurrency Theory,
Paris, France, 2010, vol. 6269, pp. 269–283.'
ista: 'Chatterjee K, Doyen L, Edelsbrunner H, Henzinger TA, Rannou P. 2010. Mean-payoff
automaton expressions. CONCUR: Concurrency Theory, LNCS, vol. 6269, 269–283.'
mla: Chatterjee, Krishnendu, et al. Mean-Payoff Automaton Expressions. Vol.
6269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 269–83, doi:10.1007/978-3-642-15375-4_19.
short: K. Chatterjee, L. Doyen, H. Edelsbrunner, T.A. Henzinger, P. Rannou, in:,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 269–283.
conference:
end_date: 2010-09-03
location: Paris, France
name: 'CONCUR: Concurrency Theory'
start_date: 2010-08-31
corr_author: '1'
date_created: 2018-12-11T12:05:31Z
date_published: 2010-11-18T00:00:00Z
date_updated: 2024-10-09T20:54:08Z
day: '18'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: HeEd
- _id: ToHe
doi: 10.1007/978-3-642-15375-4_19
ec_funded: 1
file:
- access_level: open_access
checksum: 4f753ae99d076553fb8733e2c8b390e2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:41Z
date_updated: 2020-07-14T12:46:17Z
file_id: '5163'
file_name: IST-2012-62-v1+1_Mean-payoff_automaton_expressions.pdf
file_size: 233260
relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: ' 6269'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 269 - 283
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: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '2328'
pubrep_id: '62'
quality_controlled: '1'
scopus_import: 1
status: public
title: Mean-payoff automaton expressions
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6269
year: '2010'
...
---
_id: '3855'
abstract:
- lang: eng
text: 'We study observation-based strategies for partially-observable Markov decision
processes (POMDPs) with parity objectives. An observation-based strategy relies
on partial information about the history of a play, namely, on the past sequence
of observations. We consider qualitative analysis problems: given a POMDP with
a parity objective, decide whether there exists an observation-based strategy
to achieve the objective with probability 1 (almost-sure winning), or with positive
probability (positive winning). Our main results are twofold. First, we present
a complete picture of the computational complexity of the qualitative analysis
problem for POMDPs with parity objectives and its subclasses: safety, reachability,
Büchi, and coBüchi objectives. We establish several upper and lower bounds that
were not known in the literature. Second, we give optimal bounds (matching upper
and lower bounds) for the memory required by pure and randomized observation-based
strategies for each class of 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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- 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, Doyen L, Henzinger TA. Qualitative analysis of partially-observable
Markov Decision Processes. In: Vol 6281. Springer; 2010:258-269. doi:10.1007/978-3-642-15155-2_24'
apa: 'Chatterjee, K., Doyen, L., & Henzinger, T. A. (2010). Qualitative analysis
of partially-observable Markov Decision Processes (Vol. 6281, pp. 258–269). Presented
at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic:
Springer. https://doi.org/10.1007/978-3-642-15155-2_24'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Qualitative
Analysis of Partially-Observable Markov Decision Processes,” 6281:258–69. Springer,
2010. https://doi.org/10.1007/978-3-642-15155-2_24.
ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “Qualitative analysis of partially-observable
Markov Decision Processes,” presented at the MFCS: Mathematical Foundations of
Computer Science, Brno, Czech Republic, 2010, vol. 6281, pp. 258–269.'
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2010. Qualitative analysis of partially-observable
Markov Decision Processes. MFCS: Mathematical Foundations of Computer Science,
LNCS, vol. 6281, 258–269.'
mla: Chatterjee, Krishnendu, et al. Qualitative Analysis of Partially-Observable
Markov Decision Processes. Vol. 6281, Springer, 2010, pp. 258–69, doi:10.1007/978-3-642-15155-2_24.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2010, pp. 258–269.
conference:
end_date: 2010-08-27
location: Brno, Czech Republic
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2010-08-23
corr_author: '1'
date_created: 2018-12-11T12:05:32Z
date_published: 2010-08-01T00:00:00Z
date_updated: 2024-10-09T21:08:23Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15155-2_24
ec_funded: 1
file:
- access_level: open_access
checksum: b6c82ec82f194e5b0ab7c1c3800e4580
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:51Z
date_updated: 2020-07-14T12:46:17Z
file_id: '5038'
file_name: IST-2012-61-v1+1_Qualitative_analysis_of_partially-observable_Markov_Decision_Processes.pdf
file_size: 173948
relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: ' 6281'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 258 - 269
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: '2326'
pubrep_id: '61'
quality_controlled: '1'
related_material:
record:
- id: '5395'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Qualitative analysis of partially-observable Markov Decision Processes
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6281
year: '2010'
...
---
_id: '3856'
abstract:
- lang: eng
text: 'We consider two-player zero-sum games on graphs. These games can be classified
on the basis of the information of the players and on the mode of interaction
between them. On the basis of information the classification is as follows: (a)
partial-observation (both players have partial view of the game); (b) one-sided
complete-observation (one player has complete observation); and (c) complete-observation
(both players have complete view of the game). On the basis of mode of interaction
we have the following classification: (a) concurrent (players interact simultaneously);
and (b) turn-based (players interact in turn). The two sources of randomness in
these games are randomness in transition function and randomness in strategies.
In general, randomized strategies are more powerful than deterministic strategies,
and randomness in transitions gives more general classes of games. We present
a complete characterization for the classes of games where randomness is not helpful
in: (a) the transition function (probabilistic transition can be simulated by
deterministic transition); and (b) strategies (pure strategies are as powerful
as randomized strategies). As consequence of our characterization we obtain new
undecidability results for these games. '
acknowledgement: This research was supported by the European Union project COMBEST
and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Hugo
full_name: Gimbert, Hugo
last_name: Gimbert
- 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, Doyen L, Gimbert H, Henzinger TA. Randomness for free. In: Vol
6281. Springer; 2010:246-257. doi:10.1007/978-3-642-15155-2_23'
apa: 'Chatterjee, K., Doyen, L., Gimbert, H., & Henzinger, T. A. (2010). Randomness
for free (Vol. 6281, pp. 246–257). Presented at the MFCS: Mathematical Foundations
of Computer Science, Brno, Czech Republic: Springer. https://doi.org/10.1007/978-3-642-15155-2_23'
chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger.
“Randomness for Free,” 6281:246–57. Springer, 2010. https://doi.org/10.1007/978-3-642-15155-2_23.
ieee: 'K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for
free,” presented at the MFCS: Mathematical Foundations of Computer Science, Brno,
Czech Republic, 2010, vol. 6281, pp. 246–257.'
ista: 'Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2010. Randomness for free.
MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6281, 246–257.'
mla: Chatterjee, Krishnendu, et al. Randomness for Free. Vol. 6281, Springer,
2010, pp. 246–57, doi:10.1007/978-3-642-15155-2_23.
short: K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, in:, Springer, 2010,
pp. 246–257.
conference:
end_date: 2010-08-27
location: Brno, Czech Republic
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2010-08-23
corr_author: '1'
date_created: 2018-12-11T12:05:32Z
date_published: 2010-09-06T00:00:00Z
date_updated: 2025-09-23T10:32:00Z
day: '06'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15155-2_23
ec_funded: 1
external_id:
arxiv:
- '1006.0673'
intvolume: ' 6281'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1006.0673
month: '09'
oa: 1
oa_version: Preprint
page: 246 - 257
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: '2325'
pubrep_id: '60'
quality_controlled: '1'
related_material:
record:
- id: '1731'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Randomness for free
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6281
year: '2010'
...
---
_id: '3857'
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 an almost complete characterization
of the decidability and undecidability frontier of the quantitative and qualitative
decision problems for probabilistic automata on infinite words.
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
citation:
ama: 'Chatterjee K, Henzinger TA. Probabilistic Automata on infinite words: decidability
and undecidability results. In: Vol 6252. Springer; 2010:1-16. doi:10.1007/978-3-642-15643-4_1'
apa: 'Chatterjee, K., & Henzinger, T. A. (2010). Probabilistic Automata on infinite
words: decidability and undecidability results (Vol. 6252, pp. 1–16). Presented
at the ATVA: Automated Technology for Verification and Analysis, Singapore, Singapore:
Springer. https://doi.org/10.1007/978-3-642-15643-4_1'
chicago: 'Chatterjee, Krishnendu, and Thomas A Henzinger. “Probabilistic Automata
on Infinite Words: Decidability and Undecidability Results,” 6252:1–16. Springer,
2010. https://doi.org/10.1007/978-3-642-15643-4_1.'
ieee: 'K. Chatterjee and T. A. Henzinger, “Probabilistic Automata on infinite words:
decidability and undecidability results,” presented at the ATVA: Automated Technology
for Verification and Analysis, Singapore, Singapore, 2010, vol. 6252, pp. 1–16.'
ista: 'Chatterjee K, Henzinger TA. 2010. Probabilistic Automata on infinite words:
decidability and undecidability results. ATVA: Automated Technology for Verification
and Analysis, LNCS, vol. 6252, 1–16.'
mla: 'Chatterjee, Krishnendu, and Thomas A. Henzinger. Probabilistic Automata
on Infinite Words: Decidability and Undecidability Results. Vol. 6252, Springer,
2010, pp. 1–16, doi:10.1007/978-3-642-15643-4_1.'
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2010, pp. 1–16.
conference:
end_date: 2010-09-24
location: Singapore, Singapore
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2010-09-21
corr_author: '1'
date_created: 2018-12-11T12:05:33Z
date_published: 2010-10-12T00:00:00Z
date_updated: 2024-10-09T21:08:23Z
day: '12'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15643-4_1
ec_funded: 1
intvolume: ' 6252'
language:
- iso: eng
month: '10'
oa_version: None
page: 1 - 16
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: '2324'
pubrep_id: '28'
quality_controlled: '1'
related_material:
record:
- id: '5392'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: 'Probabilistic Automata on infinite words: decidability and undecidability
results'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6252
year: '2010'
...
---
_id: '3866'
abstract:
- lang: eng
text: Systems ought to behave reasonably even in circumstances that are not anticipated
in their specifications. We propose a definition of robustness for liveness specifications
which prescribes, for any number of environment assumptions that are violated,
a minimal number of system guarantees that must still be fulfilled. This notion
of robustness can be formulated and realized using a Generalized Reactivity formula.
We present an algorithm for synthesizing robust systems from such formulas. For
the important special case of Generalized Reactivity formulas of rank 1, our algorithm
improves the complexity of [PPS06] for large specifications with a small number
of assumptions and guarantees.
alternative_title:
- LNCS
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Karin
full_name: Greimel, Karin
last_name: Greimel
- 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
citation:
ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Robustness in
the presence of liveness. In: Touili T, Cook B, Jackson P, eds. Vol 6174. Springer;
2010:410-424. doi:10.1007/978-3-642-14295-6_36'
apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann,
B. (2010). Robustness in the presence of liveness. In T. Touili, B. Cook, &
P. Jackson (Eds.) (Vol. 6174, pp. 410–424). Presented at the CAV: Computer Aided
Verification, Edinburgh, UK: Springer. https://doi.org/10.1007/978-3-642-14295-6_36'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger,
and Barbara Jobstmann. “Robustness in the Presence of Liveness.” edited by Tayssir
Touili, Byron Cook, and Paul Jackson, 6174:410–24. Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_36.
ieee: 'R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Robustness
in the presence of liveness,” presented at the CAV: Computer Aided Verification,
Edinburgh, UK, 2010, vol. 6174, pp. 410–424.'
ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2010. Robustness
in the presence of liveness. CAV: Computer Aided Verification, LNCS, vol. 6174,
410–424.'
mla: Bloem, Roderick, et al. Robustness in the Presence of Liveness. Edited
by Tayssir Touili et al., vol. 6174, Springer, 2010, pp. 410–24, doi:10.1007/978-3-642-14295-6_36.
short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, T.
Touili, B. Cook, P. Jackson (Eds.), Springer, 2010, pp. 410–424.
conference:
end_date: 2010-07-19
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
date_created: 2018-12-11T12:05:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2021-01-12T07:52:47Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_36
ec_funded: 1
editor:
- first_name: Tayssir
full_name: Touili, Tayssir
last_name: Touili
- first_name: Byron
full_name: Cook, Byron
last_name: Cook
- first_name: Paul
full_name: Jackson, Paul
last_name: Jackson
file:
- access_level: open_access
checksum: 9d204611c8d7855bed8134f8708a0010
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:52Z
date_updated: 2020-07-14T12:46:19Z
file_id: '5243'
file_name: IST-2012-54-v1+1_Robustness_in_the_presence_of_liveness.pdf
file_size: 213083
relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 410 - 424
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: '2310'
pubrep_id: '54'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robustness in the presence of liveness
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '3867'
abstract:
- lang: eng
text: Weighted automata are nondeterministic automata with numerical weights on
transitions. They can define quantitative languages L that assign to each word
w a real number L(w). In the case of infinite words, the value of a run is naturally
computed as the maximum, limsup, liminf, limit-average, or discounted-sum of the
transition weights. The value of a word w is the supremum of the values of the
runs over w. We study expressiveness and closure questions about these quantitative
languages. We first show that the set of words with value greater than a threshold
can be omega-regular for deterministic limit-average and discounted-sum automata,
while this set is always omega-regular when the threshold is isolated (i.e., some
neighborhood around the threshold contains no word). In the latter case, we prove
that the omega-regular language is robust against small perturbations of the transition
weights. We next consider automata with transition weights 0 or 1 and show that
they are as expressive as general weighted automata in the limit-average case,
but not in the discounted-sum case. Third, for quantitative languages L-1 and
L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1 - L-1, which
generalize the boolean operations on languages, as well as the sum L-1 + L-2.
We establish the closure properties of all classes of quantitative languages with
respect to these four operations.
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- 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, Doyen L, Henzinger TA. Expressiveness and closure properties
for quantitative languages. Logical Methods in Computer Science. 2010;6(3):1-23.
doi:10.2168/LMCS-6(3:10)2010
apa: Chatterjee, K., Doyen, L., & Henzinger, T. A. (2010). Expressiveness and
closure properties for quantitative languages. Logical Methods in Computer
Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-6(3:10)2010
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness
and Closure Properties for Quantitative Languages.” Logical Methods in Computer
Science. International Federation of Computational Logic, 2010. https://doi.org/10.2168/LMCS-6(3:10)2010.
ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure
properties for quantitative languages,” Logical Methods in Computer Science,
vol. 6, no. 3. International Federation of Computational Logic, pp. 1–23, 2010.
ista: Chatterjee K, Doyen L, Henzinger TA. 2010. Expressiveness and closure properties
for quantitative languages. Logical Methods in Computer Science. 6(3), 1–23.
mla: Chatterjee, Krishnendu, et al. “Expressiveness and Closure Properties for Quantitative
Languages.” Logical Methods in Computer Science, vol. 6, no. 3, International
Federation of Computational Logic, 2010, pp. 1–23, doi:10.2168/LMCS-6(3:10)2010.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, Logical Methods in Computer Science
6 (2010) 1–23.
corr_author: '1'
date_created: 2018-12-11T12:05:36Z
date_published: 2010-08-30T00:00:00Z
date_updated: 2025-09-30T09:31:00Z
day: '30'
ddc:
- '000'
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.2168/LMCS-6(3:10)2010
ec_funded: 1
external_id:
isi:
- '000282653500010'
file:
- access_level: open_access
checksum: 0243da726476817f2ea33b48b78be696
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:54Z
date_updated: 2020-07-14T12:46:19Z
file_id: '5312'
file_name: IST-2012-55-v1+1_Expressiveness_Closure_Properties_Quantitative_Languages.pdf
file_size: 216598
relation: main_file
- access_level: open_access
checksum: 5e512b8503a9cb263de26331c4ee9cf2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:55Z
date_updated: 2020-07-14T12:46:19Z
file_id: '5313'
file_name: IST-2016-55-v2+1_1007.4018.pdf
file_size: 302416
relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: ' 6'
isi: 1
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: 1 - 23
project:
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _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 of Computational Logic
publist_id: '2311'
pubrep_id: '504'
quality_controlled: '1'
related_material:
record:
- id: '4540'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Expressiveness and closure properties for quantitative languages
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
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: '4388'
abstract:
- lang: eng
text: GIST is a tool that (a) solves the qualitative analysis problem of turn-based
probabilistic games with ω-regular objectives; and (b) synthesizes reasonable
environment assumptions for synthesis of unrealizable specifications. Our tool
provides the first and efficient implementations of several reduction-based techniques
to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic
games for synthesizing environment assumptions for unrealizable specifications.
alternative_title:
- LNCS
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: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. GIST: A solver for
probabilistic games. In: Vol 6174. Springer; 2010:665-669. doi:10.1007/978-3-642-14295-6_57'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Radhakrishna, A. (2010).
GIST: A solver for probabilistic games (Vol. 6174, pp. 665–669). Presented at
the CAV: Computer Aided Verification, Edinburgh, UK: Springer. https://doi.org/10.1007/978-3-642-14295-6_57'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun
Radhakrishna. “GIST: A Solver for Probabilistic Games,” 6174:665–69. Springer,
2010. https://doi.org/10.1007/978-3-642-14295-6_57.'
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, “GIST:
A solver for probabilistic games,” presented at the CAV: Computer Aided Verification,
Edinburgh, UK, 2010, vol. 6174, pp. 665–669.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2010. GIST: A solver
for probabilistic games. CAV: Computer Aided Verification, LNCS, vol. 6174, 665–669.'
mla: 'Chatterjee, Krishnendu, et al. GIST: A Solver for Probabilistic Games.
Vol. 6174, Springer, 2010, pp. 665–69, doi:10.1007/978-3-642-14295-6_57.'
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, in:, Springer,
2010, pp. 665–669.
conference:
end_date: 2010-07-17
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
corr_author: '1'
date_created: 2018-12-11T12:08:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2024-10-09T20:54:00Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_57
ec_funded: 1
external_id:
arxiv:
- '1004.2367'
file:
- access_level: open_access
checksum: 0b2ef8c4037ffccc6902d93081af24f7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:33Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5221'
file_name: IST-2012-43-v1+1_GIST-_A_solver_for_probabilistic_games.pdf
file_size: 293605
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 665 - 669
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: '1068'
pubrep_id: '43'
quality_controlled: '1'
related_material:
record:
- id: '5393'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: 'GIST: A solver for probabilistic games'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '4392'
abstract:
- lang: eng
text: 'While a boolean notion of correctness is given by a preorder on systems and
properties, a quantitative notion of correctness is defined by a distance function
on systems and properties, where the distance between a system and a property
provides a measure of “fit” or “desirability.” In this article, we explore several
ways how the simulation preorder can be generalized to a distance function. This
is done by equipping the classical simulation game between a system and a property
with quantitative objectives. In particular, for systems that satisfy a property,
a quantitative simulation game can measure the “robustness” of the satisfaction,
that is, how much the system can deviate from its nominal behavior while still
satisfying the property. For systems that violate a property, a quantitative simulation
game can measure the “seriousness” of the violation, that is, how much the property
has to be modified so that it is satisfied by the system. These distances can
be computed in polynomial time, since the computation reduces to the value problem
in limit average games with constant weights. Finally, we demonstrate how the
robustness distance can be used to measure how many transmission errors are tolerated
by error correcting codes. '
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Quantitative Simulation Games. In:
Manna Z, Peled D, eds. Time For Verification: Essays in Memory of Amir Pnueli.
Vol 6200. Essays in Memory of Amir Pnueli. Springer; 2010:42-60. doi:10.1007/978-3-642-13754-9_3'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Quantitative Simulation
Games. In Z. Manna & D. Peled (Eds.), Time For Verification: Essays in
Memory of Amir Pnueli (Vol. 6200, pp. 42–60). Springer. https://doi.org/10.1007/978-3-642-13754-9_3'
chicago: 'Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative
Simulation Games.” In Time For Verification: Essays in Memory of Amir Pnueli,
edited by Zohar Manna and Doron Peled, 6200:42–60. Essays in Memory of Amir Pnueli.
Springer, 2010. https://doi.org/10.1007/978-3-642-13754-9_3.'
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative Simulation
Games,” in Time For Verification: Essays in Memory of Amir Pnueli, vol.
6200, Z. Manna and D. Peled, Eds. Springer, 2010, pp. 42–60.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010.Quantitative Simulation Games.
In: Time For Verification: Essays in Memory of Amir Pnueli. LNCS, vol. 6200, 42–60.'
mla: 'Cerny, Pavol, et al. “Quantitative Simulation Games.” Time For Verification:
Essays in Memory of Amir Pnueli, edited by Zohar Manna and Doron Peled, vol.
6200, Springer, 2010, pp. 42–60, doi:10.1007/978-3-642-13754-9_3.'
short: 'P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Z. Manna, D. Peled (Eds.),
Time For Verification: Essays in Memory of Amir Pnueli, Springer, 2010, pp. 42–60.'
corr_author: '1'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-07-29T00:00:00Z
date_updated: 2024-10-09T20:53:58Z
day: '29'
department:
- _id: ToHe
doi: 10.1007/978-3-642-13754-9_3
ec_funded: 1
editor:
- first_name: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Doron
full_name: Peled, Doron
last_name: Peled
intvolume: ' 6200'
language:
- iso: eng
month: '07'
oa_version: None
page: 42 - 60
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: 'Time For Verification: Essays in Memory of Amir Pnueli'
publication_status: published
publisher: Springer
publist_id: '1064'
quality_controlled: '1'
scopus_import: 1
series_title: Essays in Memory of Amir Pnueli
status: public
title: Quantitative Simulation Games
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6200
year: '2010'
...
---
_id: '4393'
abstract:
- lang: eng
text: Boolean notions of correctness are formalized by preorders on systems. Quantitative
measures of correctness can be formalized by real-valued distance functions between
systems, where the distance between implementation and specification provides
a measure of “fit” or “desirability.” We extend the simulation preorder to the
quantitative setting, by making each player of a simulation game pay a certain
price for her choices. We use the resulting games with quantitative objectives
to define three different simulation distances. The correctness distance measures
how much the specification must be changed in order to be satisfied by the implementation.
The coverage distance measures how much the implementation restricts the degrees
of freedom offered by the specification. The robustness distance measures how
much a system can deviate from the implementation description without violating
the specification. We consider these distances for safety as well as liveness
specifications. The distances can be computed in polynomial time for safety specifications,
and for liveness specifications given by weak fairness constraints. We show that
the distance functions satisfy the triangle inequality, that the distance between
two systems does not increase under parallel composition with a third system,
and that the distance between two systems can be bounded from above and below
by distances between abstractions of the two systems. These properties suggest
that our simulation distances provide an appropriate basis for a quantitative
theory of discrete systems. We also demonstrate how the robustness distance can
be used to measure how many transmission errors are tolerated by error correcting
codes.
acknowledgement: This work was partially supported by the European Union project COMBEST
and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. In: Vol 6269.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:235-268. doi:10.1007/978-3-642-15375-4_18'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Simulation distances
(Vol. 6269, pp. 235–268). Presented at the CONCUR: Concurrency Theory, Paris,
France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-15375-4_18'
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances,”
6269:235–68. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_18.
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” presented
at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 235–268.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010. Simulation distances. CONCUR:
Concurrency Theory, LNCS, vol. 6269, 235–268.'
mla: Cerny, Pavol, et al. Simulation Distances. Vol. 6269, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2010, pp. 235–68, doi:10.1007/978-3-642-15375-4_18.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2010, pp. 235–268.
conference:
end_date: 2010-09-03
location: Paris, France
name: 'CONCUR: Concurrency Theory'
start_date: 2010-08-31
corr_author: '1'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-11-01T00:00:00Z
date_updated: 2025-09-30T07:46:05Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15375-4_18
ec_funded: 1
file:
- access_level: open_access
checksum: ea567903676ba8afe0507ee11313dce5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:12Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5130'
file_name: IST-2012-42-v1+1_Simulation_distances.pdf
file_size: 198913
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6269'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 235 - 268
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: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '1065'
pubrep_id: '42'
quality_controlled: '1'
related_material:
record:
- id: '5389'
relation: earlier_version
status: public
- id: '3249'
relation: later_version
status: public
scopus_import: 1
status: public
title: Simulation distances
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6269
year: '2010'
...