---
_id: '10906'
abstract:
- lang: eng
text: HSF(C) is a tool that automates verification of safety and liveness properties
for C programs. This paper describes the verification approach taken by HSF(C)
and provides instructions on how to install and use the tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergey
full_name: Grebenshchikov, Sergey
last_name: Grebenshchikov
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Nuno P.
full_name: Lopes, Nuno P.
last_name: Lopes
- first_name: Corneliu
full_name: Popeea, Corneliu
last_name: Popeea
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
citation:
ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software
verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms
for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg:
Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46'
apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko,
A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &
B. König (Eds.), Tools and Algorithms for the Construction and Analysis of
Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46'
chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea,
and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In
Tools and Algorithms for the Construction and Analysis of Systems, edited
by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer,
2012. https://doi.org/10.1007/978-3-642-28756-5_46.'
ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko,
“HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms
for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol.
7214, pp. 549–551.'
ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C):
A software verifier based on Horn clauses. Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.'
mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn
Clauses.” Tools and Algorithms for the Construction and Analysis of Systems,
edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51,
doi:10.1007/978-3-642-28756-5_46.'
short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:,
C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis
of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.
conference:
end_date: 2012-04-01
location: Tallinn, Estonia
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2012-03-24
corr_author: '1'
date_created: 2022-03-21T08:03:30Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2026-06-18T10:45:24Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-28756-5_46
editor:
- first_name: Cormac
full_name: Flanagan, Cormac
last_name: Flanagan
- first_name: Barbara
full_name: König, Barbara
last_name: König
intvolume: ' 7214'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/978-3-642-28756-5_46
month: '04'
oa: 1
oa_version: Published Version
page: 549-551
place: Berlin, Heidelberg
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783642287565'
eissn:
- 1611-3349
isbn:
- '9783642287558'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'HSF(C): A software verifier based on Horn clauses'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7214
year: '2012'
...
---
_id: '2302'
abstract:
- lang: eng
text: 'We introduce propagation models (PMs), a formalism able to express several
kinds of equations that describe the behavior of biochemical reaction networks.
Furthermore, we introduce the propagation abstract data type (PADT), which separates
concerns regarding different numerical algorithms for the transient analysis of
biochemical reaction networks from concerns regarding their implementation, thus
allowing for portable and efficient solutions. The state of a propagation abstract
data type is given by a vector that assigns mass values to a set of nodes, and
its (next) operator propagates mass values through this set of nodes. We propose
an approximate implementation of the (next) operator, based on threshold abstraction,
which propagates only "significant" mass values and thus achieves a
compromise between efficiency and accuracy. Finally, we give three use cases for
propagation models: the chemical master equation (CME), the reaction rate equation
(RRE), and a hybrid method that combines these two equations. These three applications
use propagation models in order to propagate probabilities and/or expected values
and variances of the model''s variables.'
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: Maria
full_name: Mateescu, Maria
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
citation:
ama: Henzinger TA, Mateescu M. The propagation approach for computing biochemical
reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics.
2012;10(2):310-322. doi:10.1109/TCBB.2012.91
apa: Henzinger, T. A., & Mateescu, M. (2012). The propagation approach for computing
biochemical reaction networks. IEEE ACM Transactions on Computational Biology
and Bioinformatics. IEEE. https://doi.org/10.1109/TCBB.2012.91
chicago: Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for
Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational
Biology and Bioinformatics. IEEE, 2012. https://doi.org/10.1109/TCBB.2012.91.
ieee: T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical
reaction networks,” IEEE ACM Transactions on Computational Biology and Bioinformatics,
vol. 10, no. 2. IEEE, pp. 310–322, 2012.
ista: Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical
reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics.
10(2), 310–322.
mla: Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing
Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology
and Bioinformatics, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:10.1109/TCBB.2012.91.
short: T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology
and Bioinformatics 10 (2012) 310–322.
corr_author: '1'
date_created: 2018-12-11T11:56:52Z
date_published: 2012-07-03T00:00:00Z
date_updated: 2025-09-29T14:17:43Z
day: '03'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1109/TCBB.2012.91
ec_funded: 1
external_id:
isi:
- '000323504100006'
pmid:
- '22778152'
intvolume: ' 10'
isi: 1
issue: '2'
language:
- iso: eng
month: '07'
oa_version: None
page: 310 - 322
pmid: 1
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: IEEE ACM Transactions on Computational Biology and Bioinformatics
publication_status: published
publisher: IEEE
publist_id: '4625'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The propagation approach for computing biochemical reaction networks
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 10
year: '2012'
...
---
_id: '2848'
abstract:
- lang: eng
text: We study evolutionary game theory in a setting where individuals learn from
each other. We extend the traditional approach by assuming that a population contains
individuals with different learning abilities. In particular, we explore the situation
where individuals have different search spaces, when attempting to learn the strategies
of others. The search space of an individual specifies the set of strategies learnable
by that individual. The search space is genetically given and does not change
under social evolutionary dynamics. We introduce a general framework and study
a specific example in the context of direct reciprocity. For this example, we
obtain the counter intuitive result that cooperation can only evolve for intermediate
benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection.
Our paper is a step toward making a connection between computational learning
theory and evolutionary game dynamics.
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: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations
with different learners. Journal of Theoretical Biology. 2012;301:161-173.
doi:10.1016/j.jtbi.2012.02.021
apa: Chatterjee, K., Zufferey, D., & Nowak, M. (2012). Evolutionary game dynamics
in populations with different learners. Journal of Theoretical Biology.
Elsevier. https://doi.org/10.1016/j.jtbi.2012.02.021
chicago: Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary
Game Dynamics in Populations with Different Learners.” Journal of Theoretical
Biology. Elsevier, 2012. https://doi.org/10.1016/j.jtbi.2012.02.021.
ieee: K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations
with different learners,” Journal of Theoretical Biology, vol. 301. Elsevier,
pp. 161–173, 2012.
ista: Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations
with different learners. Journal of Theoretical Biology. 301, 161–173.
mla: Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with
Different Learners.” Journal of Theoretical Biology, vol. 301, Elsevier,
2012, pp. 161–73, doi:10.1016/j.jtbi.2012.02.021.
short: K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301
(2012) 161–173.
corr_author: '1'
date_created: 2018-12-11T11:59:55Z
date_published: 2012-05-21T00:00:00Z
date_updated: 2025-09-30T08:20:22Z
day: '21'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jtbi.2012.02.021
ec_funded: 1
external_id:
isi:
- '000303079500016'
pmid:
- '22394652'
intvolume: ' 301'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/
month: '05'
oa: 1
oa_version: Submitted Version
page: 161 - 173
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '3946'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Evolutionary game dynamics in populations with different learners
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 301
year: '2012'
...
---
OA_type: closed access
_id: '2888'
abstract:
- lang: eng
text: Formal verification aims to improve the quality of hardware and software by
detecting errors before they do harm. At the basis of formal verification lies
the logical notion of correctness, which purports to capture whether or not a
circuit or program behaves as desired. We suggest that the boolean partition into
correct and incorrect systems falls short of the practical need to assess the
behavior of hardware and software in a more nuanced fashion against multiple criteria.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. Quantitative reactive models. In: 15th International Conference
on Model Driven Engineering Languages and Systems. Vol 7590. Springer; 2012:1-2.
doi:10.1007/978-3-642-33666-9_1'
apa: 'Henzinger, T. A. (2012). Quantitative reactive models. In 15th International
Conference on Model Driven Engineering Languages and Systems (Vol. 7590, pp.
1–2). Innsbruck, Austria: Springer. https://doi.org/10.1007/978-3-642-33666-9_1'
chicago: Henzinger, Thomas A. “Quantitative Reactive Models.” In 15th International
Conference on Model Driven Engineering Languages and Systems, 7590:1–2. Springer,
2012. https://doi.org/10.1007/978-3-642-33666-9_1.
ieee: T. A. Henzinger, “Quantitative reactive models,” in 15th International
Conference on Model Driven Engineering Languages and Systems, Innsbruck, Austria,
2012, vol. 7590, pp. 1–2.
ista: 'Henzinger TA. 2012. Quantitative reactive models. 15th International Conference
on Model Driven Engineering Languages and Systems. MODELS: Model-driven Engineering
Languages and Systems, LNCS, vol. 7590, 1–2.'
mla: Henzinger, Thomas A. “Quantitative Reactive Models.” 15th International
Conference on Model Driven Engineering Languages and Systems, vol. 7590, Springer,
2012, pp. 1–2, doi:10.1007/978-3-642-33666-9_1.
short: T.A. Henzinger, in:, 15th International Conference on Model Driven Engineering
Languages and Systems, Springer, 2012, pp. 1–2.
conference:
end_date: 2012-10-05
location: Innsbruck, Austria
name: 'MODELS: Model-driven Engineering Languages and Systems'
start_date: 2012-09-30
corr_author: '1'
date_created: 2018-12-11T12:00:09Z
date_published: 2012-09-01T00:00:00Z
date_updated: 2025-05-20T07:30:56Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33666-9_1
ec_funded: 1
intvolume: ' 7590'
language:
- iso: eng
month: '09'
oa_version: None
page: 1 - 2
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
publication: 15th International Conference on Model Driven Engineering Languages and
Systems
publication_identifier:
eisbn:
- '9783642336669'
eissn:
- 1611-3349
publication_status: published
publisher: Springer
publist_id: '3870'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative reactive models
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7590
year: '2012'
...
---
_id: '2890'
abstract:
- lang: eng
text: 'Systems are often specified using multiple requirements on their behavior.
In practice, these requirements can be contradictory. The classical approach to
specification, verification, and synthesis demands more detailed specifications
that resolve any contradictions in the requirements. These detailed specifications
are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative
frameworks allow the formalization of the intuitive idea that what is desired
is an implementation that comes "closest" to satisfying the mutually
incompatible requirements, according to a measure of fit that can be defined by
the requirements engineer. One flexible framework for quantifying how "well"
an implementation satisfies a specification is offered by simulation distances
that are parameterized by an error model. We introduce this framework, study its
properties, and provide an algorithmic solution for the following quantitative
synthesis question: given two (or more) behavioral requirements specified by possibly
incompatible finite-state machines, and an error model, find the finite-state
implementation that minimizes the maximal simulation distance to the given requirements.
Furthermore, we generalize the framework to handle infinite alphabets (for example,
realvalued domains). We also demonstrate how quantitative specifications based
on simulation distances might lead to smaller and easier to modify specifications.
Finally, we illustrate our approach using case studies on error correcting codes
and scheduler synthesis.'
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Sivakanth
full_name: Gopi, Sivakanth
last_name: Gopi
- 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: Nishant
full_name: Totla, Nishant
last_name: Totla
citation:
ama: 'Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. Synthesis from incompatible
specifications. In: Proceedings of the Tenth ACM International Conference on
Embedded Software. ACM; 2012:53-62. doi:10.1145/2380356.2380371'
apa: 'Cerny, P., Gopi, S., Henzinger, T. A., Radhakrishna, A., & Totla, N. (2012).
Synthesis from incompatible specifications. In Proceedings of the tenth ACM
international conference on Embedded software (pp. 53–62). Tampere, Finland:
ACM. https://doi.org/10.1145/2380356.2380371'
chicago: Cerny, Pavol, Sivakanth Gopi, Thomas A Henzinger, Arjun Radhakrishna, and
Nishant Totla. “Synthesis from Incompatible Specifications.” In Proceedings
of the Tenth ACM International Conference on Embedded Software, 53–62. ACM,
2012. https://doi.org/10.1145/2380356.2380371.
ieee: P. Cerny, S. Gopi, T. A. Henzinger, A. Radhakrishna, and N. Totla, “Synthesis
from incompatible specifications,” in Proceedings of the tenth ACM international
conference on Embedded software, Tampere, Finland, 2012, pp. 53–62.
ista: 'Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. 2012. Synthesis from
incompatible specifications. Proceedings of the tenth ACM international conference
on Embedded software. EMSOFT: Embedded Software , 53–62.'
mla: Cerny, Pavol, et al. “Synthesis from Incompatible Specifications.” Proceedings
of the Tenth ACM International Conference on Embedded Software, ACM, 2012,
pp. 53–62, doi:10.1145/2380356.2380371.
short: P. Cerny, S. Gopi, T.A. Henzinger, A. Radhakrishna, N. Totla, in:, Proceedings
of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp.
53–62.
conference:
end_date: 2012-10-12
location: Tampere, Finland
name: 'EMSOFT: Embedded Software '
start_date: 2012-10-07
date_created: 2018-12-11T12:00:10Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2021-01-12T07:00:30Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2380356.2380371
ec_funded: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 53 - 62
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
publication: Proceedings of the tenth ACM international conference on Embedded software
publication_status: published
publisher: ACM
publist_id: '3868'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synthesis from incompatible specifications
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '2891'
abstract:
- lang: eng
text: "Quantitative automata are nondeterministic finite automata with edge weights.
They value a\r\nrun by some function from the sequence of visited weights to the
reals, and value a word by its\r\nminimal/maximal run. They generalize boolean
automata, and have gained much attention in\r\nrecent years. Unfortunately, important
automaton classes, such as sum, discounted-sum, and\r\nlimit-average automata,
cannot be determinized. Yet, the quantitative setting provides the potential\r\nof
approximate determinization. We define approximate determinization with respect
to\r\na distance function, and investigate this potential.\r\nWe show that sum
automata cannot be determinized approximately with respect to any\r\ndistance
function. However, restricting to nonnegative weights allows for approximate determinization\r\nwith
respect to some distance functions.\r\nDiscounted-sum automata allow for approximate
determinization, as the influence of a word’s\r\nsuffix is decaying. However,
the naive approach, of unfolding the automaton computations up\r\nto a sufficient
level, is shown to be doubly exponential in the discount factor. We provide an\r\nalternative
construction that is singly exponential in the discount factor, in the precision,
and\r\nin the number of states. We prove matching lower bounds, showing exponential
dependency on\r\neach of these three parameters.\r\nAverage and limit-average
automata are shown to prohibit approximate determinization with\r\nrespect to
any distance function, and this is the case even for two weights, 0 and 1."
acknowledgement: We thank Laurent Doyen for great ideas and valuable help in analyzing
discounted-sum automata.
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. Approximate determinization of quantitative automata.
In: Leibniz International Proceedings in Informatics. Vol 18. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2012:362-373. doi:10.4230/LIPIcs.FSTTCS.2012.362'
apa: 'Boker, U., & Henzinger, T. A. (2012). Approximate determinization of quantitative
automata. In Leibniz International Proceedings in Informatics (Vol. 18,
pp. 362–373). Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.FSTTCS.2012.362'
chicago: Boker, Udi, and Thomas A Henzinger. “Approximate Determinization of Quantitative
Automata.” In Leibniz International Proceedings in Informatics, 18:362–73.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. https://doi.org/10.4230/LIPIcs.FSTTCS.2012.362.
ieee: U. Boker and T. A. Henzinger, “Approximate determinization of quantitative
automata,” in Leibniz International Proceedings in Informatics, Hyderabad,
India, 2012, vol. 18, pp. 362–373.
ista: 'Boker U, Henzinger TA. 2012. Approximate determinization of quantitative
automata. Leibniz International Proceedings in Informatics. FSTTCS: Foundations
of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 362–373.'
mla: Boker, Udi, and Thomas A. Henzinger. “Approximate Determinization of Quantitative
Automata.” Leibniz International Proceedings in Informatics, vol. 18, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 362–73, doi:10.4230/LIPIcs.FSTTCS.2012.362.
short: U. Boker, T.A. Henzinger, in:, Leibniz International Proceedings in Informatics,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 362–373.
conference:
end_date: 2012-12-17
location: Hyderabad, India
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2012-12-15
corr_author: '1'
date_created: 2018-12-11T12:00:10Z
date_published: 2012-12-01T00:00:00Z
date_updated: 2024-10-09T20:54:57Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.FSTTCS.2012.362
ec_funded: 1
file:
- access_level: open_access
checksum: 88da18d3e2cb2e5011d7d10ce38a3864
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:37Z
date_updated: 2020-07-14T12:45:52Z
file_id: '4826'
file_name: IST-2017-805-v1+1_34.pdf
file_size: 559069
relation: main_file
file_date_updated: 2020-07-14T12:45:52Z
has_accepted_license: '1'
intvolume: ' 18'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '12'
oa: 1
oa_version: Published Version
page: 362 - 373
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Leibniz International Proceedings in Informatics
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '3867'
pubrep_id: '805'
quality_controlled: '1'
scopus_import: 1
status: public
title: Approximate determinization of quantitative 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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2012'
...
---
_id: '2916'
abstract:
- lang: eng
text: The classical (boolean) notion of refinement for behavioral interfaces of
system components is the alternating refinement preorder. In this paper, we define
a quantitative measure for interfaces, called interface simulation distance. It
makes the alternating refinement preorder quantitative by, intu- itively, tolerating
errors (while counting them) in the alternating simulation game. We show that
the interface simulation distance satisfies the triangle inequality, that the
distance between two interfaces does not increase under parallel composition with
a third interface, and that the distance between two interfaces can be bounded
from above and below by distances between abstractions of the two interfaces.
We illustrate the framework, and the properties of the distances under composition
of interfaces, with two case studies.
arxiv: 1
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- 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, Chmelik M, Henzinger TA, Radhakrishna A. Interface Simulation Distances.
In: Electronic Proceedings in Theoretical Computer Science. Vol 96. EPTCS;
2012:29-42. doi:10.4204/EPTCS.96.3'
apa: 'Cerny, P., Chmelik, M., Henzinger, T. A., & Radhakrishna, A. (2012). Interface
Simulation Distances. In Electronic Proceedings in Theoretical Computer Science
(Vol. 96, pp. 29–42). Napoli, Italy: EPTCS. https://doi.org/10.4204/EPTCS.96.3'
chicago: Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna.
“Interface Simulation Distances.” In Electronic Proceedings in Theoretical
Computer Science, 96:29–42. EPTCS, 2012. https://doi.org/10.4204/EPTCS.96.3.
ieee: P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface Simulation
Distances,” in Electronic Proceedings in Theoretical Computer Science,
Napoli, Italy, 2012, vol. 96, pp. 29–42.
ista: 'Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2012. Interface Simulation
Distances. Electronic Proceedings in Theoretical Computer Science. GandALF: Games,
Automata, Logic, and Formal Verification vol. 96, 29–42.'
mla: Cerny, Pavol, et al. “Interface Simulation Distances.” Electronic Proceedings
in Theoretical Computer Science, vol. 96, EPTCS, 2012, pp. 29–42, doi:10.4204/EPTCS.96.3.
short: P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, in:, Electronic Proceedings
in Theoretical Computer Science, EPTCS, 2012, pp. 29–42.
conference:
end_date: 2012-09-08
location: Napoli, Italy
name: 'GandALF: Games, Automata, Logic, and Formal Verification'
start_date: 2012-09-06
date_created: 2018-12-11T12:00:19Z
date_published: 2012-10-07T00:00:00Z
date_updated: 2025-09-29T13:14:24Z
day: '07'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4204/EPTCS.96.3
ec_funded: 1
external_id:
arxiv:
- '1210.2450'
intvolume: ' 96'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1210.2450
month: '10'
oa: 1
oa_version: Submitted Version
page: 29 - 42
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: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _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
publication: Electronic Proceedings in Theoretical Computer Science
publication_status: published
publisher: EPTCS
publist_id: '3827'
quality_controlled: '1'
related_material:
record:
- id: '1733'
relation: later_version
status: public
scopus_import: 1
status: public
title: Interface Simulation Distances
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 96
year: '2012'
...
---
_id: '2936'
abstract:
- lang: eng
text: The notion of delays arises naturally in many computational models, such as,
in the design of circuits, control systems, and dataflow languages. In this work,
we introduce automata with delay blocks (ADBs), extending finite state automata
with variable time delay blocks, for deferring individual transition output symbols,
in a discrete-time setting. We show that the ADB languages strictly subsume the
regular languages, and are incomparable in expressive power to the context-free
languages. We show that ADBs are closed under union, concatenation and Kleene
star, and under intersection with regular languages, but not closed under complementation
and intersection with other ADB languages. We show that the emptiness and the
membership problems are decidable in polynomial time for ADBs, whereas the universality
problem is undecidable. Finally we consider the linear-time model checking problem,
i.e., whether the language of an ADB is contained in a regular language, and show
that the model checking problem is PSPACE-complete. Copyright 2012 ACM.
acknowledgement: 'This work has been financially supported in part by the European
Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract
# 270180 (NOPTILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008
(Modeling and control of Networked vehicle systems in persistent autonomous operations);
by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic
Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start
grant (279307: Graph Games); Microsoft faculty fellows award; ERC Advanced grant
QUAREM; and FWF Grant No S11403-N23 (RiSE).'
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: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: 'Chatterjee K, Henzinger TA, Prabhu V. Finite automata with time delay blocks.
In: Roceedings of the Tenth ACM International Conference on Embedded Software.
ACM; 2012:43-52. doi:10.1145/2380356.2380370'
apa: 'Chatterjee, K., Henzinger, T. A., & Prabhu, V. (2012). Finite automata
with time delay blocks. In roceedings of the tenth ACM international conference
on Embedded software (pp. 43–52). Tampere, Finland: ACM. https://doi.org/10.1145/2380356.2380370'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Finite
Automata with Time Delay Blocks.” In Roceedings of the Tenth ACM International
Conference on Embedded Software, 43–52. ACM, 2012. https://doi.org/10.1145/2380356.2380370.
ieee: K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Finite automata with time
delay blocks,” in roceedings of the tenth ACM international conference on Embedded
software, Tampere, Finland, 2012, pp. 43–52.
ista: 'Chatterjee K, Henzinger TA, Prabhu V. 2012. Finite automata with time delay
blocks. roceedings of the tenth ACM international conference on Embedded software.
EMSOFT: Embedded Software , 43–52.'
mla: Chatterjee, Krishnendu, et al. “Finite Automata with Time Delay Blocks.” Roceedings
of the Tenth ACM International Conference on Embedded Software, ACM, 2012,
pp. 43–52, doi:10.1145/2380356.2380370.
short: K. Chatterjee, T.A. Henzinger, V. Prabhu, in:, Roceedings of the Tenth ACM
International Conference on Embedded Software, ACM, 2012, pp. 43–52.
conference:
end_date: 2012-10-12
location: Tampere, Finland
name: 'EMSOFT: Embedded Software '
start_date: 2012-10-07
date_created: 2018-12-11T12:00:26Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2025-06-11T08:08:30Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2380356.2380370
ec_funded: 1
external_id:
arxiv:
- '1207.7019'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1207.7019
month: '10'
oa: 1
oa_version: Preprint
page: 43 - 52
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _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: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: roceedings of the tenth ACM international conference on Embedded software
publication_status: published
publisher: ACM
publist_id: '3799'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Finite automata with time delay blocks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '1384'
abstract:
- lang: eng
text: 'Software model checking, as an undecidable problem, has three possible outcomes:
(1) the program satisfies the specification, (2) the program does not satisfy
the specification, and (3) the model checker fails. The third outcome usually
manifests itself in a space-out, time-out, or one component of the verification
tool giving up; in all of these failing cases, significant computation is performed
by the verification tool before the failure, but no result is reported. We propose
to reformulate the model-checking problem as follows, in order to have the verification
tool report a summary of the performed work even in case of failure: given a program
and a specification, the model checker returns a condition Ψ - usually a state
predicate - such that the program satisfies the specification under the condition
Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied.
In our experiments, we investigated as one major application of conditional model
checking the sequential combination of model checkers with information passing.
We give the condition that one model checker produces, as input to a second conditional
model checker, such that the verification problem for the second is restricted
to the part of the state space that is not covered by the condition, i.e., the
second model checker works on the problems that the first model checker could
not solve. Our experiments demonstrate that repeated application of conditional
model checkers, passing information from one model checker to the next, can significantly
improve the verification results and performance, i.e., we can now verify programs
that we could not verify before.'
acknowledgement: This research was supported by the Canadian NSERC grant RGPIN 341819-07, the ERC Advanced Grant
QUAREM, and the Austrian Science Fund NFN RiSE.
article_number: '57'
article_processing_charge: No
arxiv: 1
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- 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: Mehmet
full_name: Keremoglu, Mehmet
last_name: Keremoglu
- first_name: Philipp
full_name: Wendler, Philipp
last_name: Wendler
citation:
ama: 'Beyer D, Henzinger TA, Keremoglu M, Wendler P. Conditional model checking:
A technique to pass information between verifiers. In: Proceedings of the ACM
SIGSOFT 20th International Symposium on the Foundations of Software Engineering.
ACM; 2012. doi:10.1145/2393596.2393664'
apa: 'Beyer, D., Henzinger, T. A., Keremoglu, M., & Wendler, P. (2012). Conditional
model checking: A technique to pass information between verifiers. In Proceedings
of the ACM SIGSOFT 20th International Symposium on the Foundations of Software
Engineering. Cary, NC, USA: ACM. https://doi.org/10.1145/2393596.2393664'
chicago: 'Beyer, Dirk, Thomas A Henzinger, Mehmet Keremoglu, and Philipp Wendler.
“Conditional Model Checking: A Technique to Pass Information between Verifiers.”
In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations
of Software Engineering. ACM, 2012. https://doi.org/10.1145/2393596.2393664.'
ieee: 'D. Beyer, T. A. Henzinger, M. Keremoglu, and P. Wendler, “Conditional model
checking: A technique to pass information between verifiers,” in Proceedings
of the ACM SIGSOFT 20th International Symposium on the Foundations of Software
Engineering, Cary, NC, USA, 2012.'
ista: 'Beyer D, Henzinger TA, Keremoglu M, Wendler P. 2012. Conditional model checking:
A technique to pass information between verifiers. Proceedings of the ACM SIGSOFT
20th International Symposium on the Foundations of Software Engineering. FSE:
Foundations of Software Engineering, 57.'
mla: 'Beyer, Dirk, et al. “Conditional Model Checking: A Technique to Pass Information
between Verifiers.” Proceedings of the ACM SIGSOFT 20th International Symposium
on the Foundations of Software Engineering, 57, ACM, 2012, doi:10.1145/2393596.2393664.'
short: D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the
ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering,
ACM, 2012.
conference:
end_date: 2012-11-16
location: Cary, NC, USA
name: 'FSE: Foundations of Software Engineering'
start_date: 2012-11-11
date_created: 2018-12-11T11:51:42Z
date_published: 2012-11-01T00:00:00Z
date_updated: 2025-06-11T08:07:37Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2393596.2393664
ec_funded: 1
external_id:
arxiv:
- '1109.6926'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1109.6926
month: '11'
oa: 1
oa_version: Preprint
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
publication: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations
of Software Engineering
publication_status: published
publisher: ACM
publist_id: '5826'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Conditional model checking: A technique to pass information between verifiers'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
OA_place: repository
_id: '5745'
abstract:
- lang: eng
text: Unsatisfiability proofs find many applications in verification. Today, many
SAT solvers are capable of producing resolution proofs of unsatisfiability. For
efficiency smaller proofs are preferred over bigger ones. The solvers apply proof
reduction methods to remove redundant parts of the proofs while and after generating
the proofs. One method of reducing resolution proofs is redundant resolution reduction,
i.e., removing repeated pivots in the paths of resolution proofs (aka Pivot recycle).
The known single pass algorithm only tries to remove redundancies in the parts
of the proof that are trees. In this paper, we present three modifications to
improve the algorithm such that the redundancies can be found in the parts of
the proofs that are DAGs. The first modified algorithm covers greater number of
redundancies as compared to the known algorithm without incurring any additional
cost. The second modified algorithm covers even greater number of the redundancies
but it may have longer run times. Our third modified algorithm is parametrized
and can trade off between run times and the coverage of the redundancies. We have
implemented our algorithms in OpenSMT and applied them on unsatisfiability proofs
of 198 examples from plain MUS track of SAT11 competition. The first and second
algorithm additionally remove 0.89% and 10.57% of clauses respectively as compared
to the original algorithm. For certain value of the parameter, the third algorithm
removes almost as many clauses as the second algorithm but is significantly faster.
acknowledgement: "This work was supported by the ERC Advanced Investigator grant on
Quantitative\r\nReactive Modeling (QUAREM)."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
citation:
ama: 'Gupta A. Improved single pass algorithms for resolution proof reduction. In:
10th International Symposium on Automated Technology for Verification and Analysis.
Vol 7561. Springer Nature; 2012:107-121. doi:10.1007/978-3-642-33386-6_10'
apa: 'Gupta, A. (2012). Improved single pass algorithms for resolution proof reduction.
In 10th International Symposium on Automated Technology for Verification and
Analysis (Vol. 7561, pp. 107–121). Thiruvananthapuram, Kerala, India: Springer
Nature. https://doi.org/10.1007/978-3-642-33386-6_10'
chicago: Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof
Reduction.” In 10th International Symposium on Automated Technology for Verification
and Analysis, 7561:107–21. Springer Nature, 2012. https://doi.org/10.1007/978-3-642-33386-6_10.
ieee: A. Gupta, “Improved single pass algorithms for resolution proof reduction,”
in 10th International Symposium on Automated Technology for Verification and
Analysis, Thiruvananthapuram, Kerala, India, 2012, vol. 7561, pp. 107–121.
ista: 'Gupta A. 2012. Improved single pass algorithms for resolution proof reduction.
10th International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 107–121.'
mla: Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.”
10th International Symposium on Automated Technology for Verification and Analysis,
vol. 7561, Springer Nature, 2012, pp. 107–21, doi:10.1007/978-3-642-33386-6_10.
short: A. Gupta, in:, 10th International Symposium on Automated Technology for Verification
and Analysis, Springer Nature, 2012, pp. 107–121.
conference:
end_date: 2012-10-06
location: Thiruvananthapuram, Kerala, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2012-10-03
corr_author: '1'
date_created: 2018-12-18T13:01:46Z
date_published: 2012-09-28T00:00:00Z
date_updated: 2025-04-15T07:56:27Z
day: '28'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_10
ec_funded: 1
file:
- access_level: open_access
checksum: 68415837a315de3cc4d120f6019d752c
content_type: application/pdf
creator: dernst
date_created: 2018-12-18T13:07:35Z
date_updated: 2020-07-14T12:47:10Z
file_id: '5746'
file_name: 2012_ATVA_Gupta.pdf
file_size: 465502
relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: ' 7561'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 107-121
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: 10th International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eisbn:
- '9783642333866'
eissn:
- 1611-3349
isbn:
- '9783642333859'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
pubrep_id: '180'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Improved single pass algorithms for resolution proof reduction
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7561
year: '2012'
...
---
_id: '3128'
abstract:
- lang: eng
text: 'We consider two-player zero-sum stochastic games on graphs with ω-regular
winning conditions specified as parity objectives. These games have applications
in the design and control of reactive systems. We survey the complexity results
for the problem of deciding the winner in such games, and in classes of interest
obtained as special cases, based on the information and the power of randomization
available to the players, on the class of objectives and on the winning mode.
On the basis of information, these games can be classified as follows: (a) partial-observation
(both players have partial view of the game); (b) one-sided partial-observation
(one player has partial-observation and the other player has complete-observation);
and (c) complete-observation (both players have complete view of the game). The
one-sided partial-observation games have two important subclasses: the one-player
games, known as partial-observation Markov decision processes (POMDPs), and the
blind one-player games, known as probabilistic automata. On the basis of randomization,
(a) the players may not be allowed to use randomization (pure strategies), or
(b) they may choose a probability distribution over actions but the actual random
choice is external and not visible to the player (actions invisible), or (c) they
may use full randomization. Finally, various classes of games are obtained by
restricting the parity objective to a reachability, safety, Büchi, or coBüchi
condition. We also consider several winning modes, such as sure-winning (i.e.,
all outcomes of a strategy have to satisfy the winning condition), almost-sure
winning (i.e., winning with probability 1), limit-sure winning (i.e., winning
with probability arbitrarily close to 1), and value-threshold winning (i.e., winning
with probability at least ν, where ν is a given rational). '
acknowledgement: 'The research was supported by Austrian Science Fund (FWF) Grant
No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF
NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft
faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).'
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. A survey of partial-observation stochastic
parity games. Formal Methods in System Design. 2012;43(2):268-284. doi:10.1007/s10703-012-0164-2
apa: Chatterjee, K., Doyen, L., & Henzinger, T. A. (2012). A survey of partial-observation
stochastic parity games. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0164-2
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey
of Partial-Observation Stochastic Parity Games.” Formal Methods in System Design.
Springer, 2012. https://doi.org/10.1007/s10703-012-0164-2.
ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation
stochastic parity games,” Formal Methods in System Design, vol. 43, no.
2. Springer, pp. 268–284, 2012.
ista: Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation
stochastic parity games. Formal Methods in System Design. 43(2), 268–284.
mla: Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic
Parity Games.” Formal Methods in System Design, vol. 43, no. 2, Springer,
2012, pp. 268–84, doi:10.1007/s10703-012-0164-2.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design
43 (2012) 268–284.
corr_author: '1'
date_created: 2018-12-11T12:01:33Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2025-09-30T07:57:51Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-012-0164-2
ec_funded: 1
external_id:
isi:
- '000324114600006'
file:
- access_level: open_access
checksum: dd3d590f383bb2ac6cfda1489ac1c42a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:27Z
date_updated: 2020-07-14T12:46:00Z
file_id: '4882'
file_name: IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf
file_size: 163983
relation: main_file
file_date_updated: 2020-07-14T12:46:00Z
has_accepted_license: '1'
intvolume: ' 43'
isi: 1
issue: '2'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 268 - 284
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '3570'
pubrep_id: '303'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A survey of partial-observation stochastic parity games
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 43
year: '2012'
...
---
_id: '3136'
abstract:
- lang: eng
text: 'Continuous-time Markov chains (CTMC) with their rich theory and efficient
simulation algorithms have been successfully used in modeling stochastic processes
in diverse areas such as computer science, physics, and biology. However, systems
that comprise non-instantaneous events cannot be accurately and efficiently modeled
with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that
allows for the specification of a lower bound on the time interval between an
event''s initiation and its completion, and we propose an algorithm for the computation
of their behavior. Our algorithm effectively decomposes the computation into two
stages: a pure CTMC governs event initiations while a deterministic process guarantees
lower bounds on event completion times. Furthermore, from the nature of delayed
CTMCs, we obtain a parallelized version of our algorithm. We use our formalism
to model genetic regulatory circuits (biological systems where delayed events
are common) and report on the results of our numerical algorithm as run on a cluster.
We compare performance and accuracy of our results with results obtained by using
pure CTMCs. © 2012 Springer-Verlag.'
acknowledgement: This work was supported by the ERC Advanced Investigator grant on
Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- 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
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: 'Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. Delayed continuous time
Markov chains for genetic regulatory circuits. In: Vol 7358. Springer; 2012:294-309.
doi:10.1007/978-3-642-31424-7_24'
apa: 'Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., & Sezgin, A. (2012).
Delayed continuous time Markov chains for genetic regulatory circuits (Vol. 7358,
pp. 294–309). Presented at the CAV: Computer Aided Verification, Berkeley, CA,
USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_24'
chicago: Guet, Calin C, Ashutosh Gupta, Thomas A Henzinger, Maria Mateescu, and
Ali Sezgin. “Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,”
7358:294–309. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_24.
ieee: 'C. C. Guet, A. Gupta, T. A. Henzinger, M. Mateescu, and A. Sezgin, “Delayed
continuous time Markov chains for genetic regulatory circuits,” presented at the
CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 294–309.'
ista: 'Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. 2012. Delayed continuous
time Markov chains for genetic regulatory circuits. CAV: Computer Aided Verification,
LNCS, vol. 7358, 294–309.'
mla: Guet, Calin C., et al. Delayed Continuous Time Markov Chains for Genetic
Regulatory Circuits. Vol. 7358, Springer, 2012, pp. 294–309, doi:10.1007/978-3-642-31424-7_24.
short: C.C. Guet, A. Gupta, T.A. Henzinger, M. Mateescu, A. Sezgin, in:, Springer,
2012, pp. 294–309.
conference:
end_date: 2012-07-13
location: Berkeley, CA, USA
name: 'CAV: Computer Aided Verification'
start_date: 2012-07-07
corr_author: '1'
date_created: 2018-12-11T12:01:36Z
date_published: 2012-07-01T00:00:00Z
date_updated: 2024-10-09T20:54:47Z
day: '01'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-642-31424-7_24
ec_funded: 1
language:
- iso: eng
month: '07'
oa_version: None
page: 294 - 309
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '3561'
quality_controlled: '1'
scopus_import: 1
status: public
title: Delayed continuous time Markov chains for genetic regulatory circuits
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: '7358 '
year: '2012'
...
---
_id: '3155'
abstract:
- lang: eng
text: 'We propose synchronous interfaces, a new interface theory for discrete-time
systems. We use an application to time-triggered scheduling to drive the design
choices for our formalism; in particular, additionally to deriving useful mathematical
properties, we focus on providing a syntax which is adapted to natural high-level
system modeling. As a result, we develop an interface model that relies on a guarded-command
based language and is equipped with shared variables and explicit discrete-time
clocks. We define all standard interface operations: compatibility checking, composition,
refinement, and shared refinement. Apart from the synchronous interface model,
the contribution of this paper is the establishment of a formal relation between
interface theories and real-time scheduling, where we demonstrate a fully automatic
framework for the incremental computation of time-triggered schedules.'
acknowledgement: Research partially supported by the Danish-Chinese Center for Cyber
Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB.
alternative_title:
- LNCS
author:
- first_name: Benoît
full_name: Delahaye, Benoît
last_name: Delahaye
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- 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: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. Synchronous interface
theories and time triggered scheduling. In: Vol 7273. Springer; 2012:203-218.
doi:10.1007/978-3-642-30793-5_13'
apa: 'Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., & Nickovic,
D. (2012). Synchronous interface theories and time triggered scheduling (Vol.
7273, pp. 203–218). Presented at the FORTE: Formal Techniques for Networked and
Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed
Systems , Stockholm, Sweden: Springer. https://doi.org/10.1007/978-3-642-30793-5_13'
chicago: Delahaye, Benoît, Uli Fahrenberg, Thomas A Henzinger, Axel Legay, and Dejan
Nickovic. “Synchronous Interface Theories and Time Triggered Scheduling,” 7273:203–18.
Springer, 2012. https://doi.org/10.1007/978-3-642-30793-5_13.
ieee: 'B. Delahaye, U. Fahrenberg, T. A. Henzinger, A. Legay, and D. Nickovic, “Synchronous
interface theories and time triggered scheduling,” presented at the FORTE: Formal
Techniques for Networked and Distributed Systems & FMOODS: Formal Methods
for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273,
pp. 203–218.'
ista: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. 2012. Synchronous
interface theories and time triggered scheduling. FORTE: Formal Techniques for
Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based
Distributed Systems , LNCS, vol. 7273, 203–218.'
mla: Delahaye, Benoît, et al. Synchronous Interface Theories and Time Triggered
Scheduling. Vol. 7273, Springer, 2012, pp. 203–18, doi:10.1007/978-3-642-30793-5_13.
short: B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer,
2012, pp. 203–218.
conference:
end_date: 2012-06-16
location: Stockholm, Sweden
name: 'FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS:
Formal Methods for Open Object-Based Distributed Systems '
start_date: 2012-06-13
date_created: 2018-12-11T12:01:43Z
date_published: 2012-06-01T00:00:00Z
date_updated: 2021-01-12T07:41:26Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-30793-5_13
file:
- access_level: open_access
checksum: feae2e07f2d9a59843f8ddabf25d179f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:25Z
date_updated: 2020-07-14T12:46:01Z
file_id: '4879'
file_name: IST-2012-88-v1+1_Synchronous_interface_theories_and_time_triggered_scheduling.pdf
file_size: 493198
relation: main_file
file_date_updated: 2020-07-14T12:46:01Z
has_accepted_license: '1'
intvolume: ' 7273'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 203 - 218
publication_status: published
publisher: Springer
publist_id: '3539'
pubrep_id: '88'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synchronous interface theories and time triggered scheduling
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7273
year: '2012'
...
---
_id: '3162'
abstract:
- lang: eng
text: Given a dense-time real-valued signal and a parameterized temporal logic formula
with both magnitude and timing parameters, we compute the subset of the parameter
space that renders the formula satisfied by the trace. We provide two preliminary
implementations, one which follows the exact semantics and attempts to compute
the validity domain by quantifier elimination in linear arithmetics and one which
conducts adaptive search in the parameter space.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Eugene
full_name: Asarin, Eugene
last_name: Asarin
- first_name: Alexandre
full_name: Donzé, Alexandre
last_name: Donzé
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Asarin E, Donzé A, Maler O, Nickovic D. Parametric identification of temporal
properties. In: Vol 7186. Springer; 2012:147-160. doi:10.1007/978-3-642-29860-8_12'
apa: 'Asarin, E., Donzé, A., Maler, O., & Nickovic, D. (2012). Parametric identification
of temporal properties (Vol. 7186, pp. 147–160). Presented at the RV: Runtime
Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-642-29860-8_12'
chicago: Asarin, Eugene, Alexandre Donzé, Oded Maler, and Dejan Nickovic. “Parametric
Identification of Temporal Properties,” 7186:147–60. Springer, 2012. https://doi.org/10.1007/978-3-642-29860-8_12.
ieee: 'E. Asarin, A. Donzé, O. Maler, and D. Nickovic, “Parametric identification
of temporal properties,” presented at the RV: Runtime Verification, San Francisco,
CA, United States, 2012, vol. 7186, pp. 147–160.'
ista: 'Asarin E, Donzé A, Maler O, Nickovic D. 2012. Parametric identification of
temporal properties. RV: Runtime Verification, LNCS, vol. 7186, 147–160.'
mla: Asarin, Eugene, et al. Parametric Identification of Temporal Properties.
Vol. 7186, Springer, 2012, pp. 147–60, doi:10.1007/978-3-642-29860-8_12.
short: E. Asarin, A. Donzé, O. Maler, D. Nickovic, in:, Springer, 2012, pp. 147–160.
conference:
end_date: 2011-09-30
location: San Francisco, CA, United States
name: 'RV: Runtime Verification'
start_date: 2011-09-27
date_created: 2018-12-11T12:01:45Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2021-01-12T07:41:29Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-29860-8_12
file:
- access_level: open_access
checksum: ba4a75287008fc64b8fbf78a7476ec32
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T12:50:15Z
date_updated: 2020-07-14T12:46:01Z
file_id: '7862'
file_name: 2012_RV_Asarin.pdf
file_size: 374726
relation: main_file
file_date_updated: 2020-07-14T12:46:01Z
has_accepted_license: '1'
intvolume: ' 7186'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 147 - 160
publication_status: published
publisher: Springer
publist_id: '3525'
quality_controlled: '1'
scopus_import: 1
status: public
title: Parametric identification of temporal properties
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7186
year: '2012'
...
---
OA_place: publisher
OA_type: free access
_id: '3168'
abstract:
- lang: eng
text: The induction of a signaling pathway is characterized by transient complex
formation and mutual posttranslational modification of proteins. To faithfully
capture this combinatorial process in a mathematical model is an important challenge
in systems biology. Exploiting the limited context on which most binding and modification
events are conditioned, attempts have been made to reduce the combinatorial complexity
by quotienting the reachable set of molecular species into species aggregates
while preserving the deterministic semantics of the thermodynamic limit. Recently,
we proposed a quotienting that also preserves the stochastic semantics and that
is complete in the sense that the semantics of individual species can be recovered
from the aggregate semantics. In this paper, we prove that this quotienting yields
a sufficient condition for weak lumpability (that is to say that the quotient
system is still Markovian for a given set of initial distributions) and that it
gives rise to a backward Markov bisimulation between the original and aggregated
transition system (which means that the conditional probability of being in a
given state in the original system knowing that we are in its equivalence class
is an invariant of the system). We illustrate the framework on a case study of
the epidermal growth factor (EGF)/insulin receptor crosstalk.
acknowledgement: "We would like to thank the anonymous reviewers for their comments
on the different versions of the paper. We would also like to thank Ferdinanda Camporesi
for her careful reading and the useful insights that she gave us about the paper.\r\nJérôme
Feret’s contribution was partially supported by the AbstractCell ANR-Chair of Excellence.
Heinz Koeppl’s research is supported by the Swiss National Science Foundation, grant
no. 200020-117975/1. Tatjana Petrov’s research is supported by SystemsX.ch (the
Swiss Initiative in Systems Biology)."
article_processing_charge: No
article_type: original
author:
- first_name: Jérôme
full_name: Feret, Jérôme
last_name: Feret
- 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: Heinz
full_name: Koeppl, Heinz
last_name: Koeppl
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: Feret J, Henzinger TA, Koeppl H, Petrov T. Lumpability abstractions of rule
based systems. Theoretical Computer Science. 2012;431:137-164. doi:10.1016/j.tcs.2011.12.059
apa: Feret, J., Henzinger, T. A., Koeppl, H., & Petrov, T. (2012). Lumpability
abstractions of rule based systems. Theoretical Computer Science. Elsevier.
https://doi.org/10.1016/j.tcs.2011.12.059
chicago: Feret, Jérôme, Thomas A Henzinger, Heinz Koeppl, and Tatjana Petrov. “Lumpability
Abstractions of Rule Based Systems.” Theoretical Computer Science. Elsevier,
2012. https://doi.org/10.1016/j.tcs.2011.12.059.
ieee: J. Feret, T. A. Henzinger, H. Koeppl, and T. Petrov, “Lumpability abstractions
of rule based systems,” Theoretical Computer Science, vol. 431. Elsevier,
pp. 137–164, 2012.
ista: Feret J, Henzinger TA, Koeppl H, Petrov T. 2012. Lumpability abstractions
of rule based systems. Theoretical Computer Science. 431, 137–164.
mla: Feret, Jérôme, et al. “Lumpability Abstractions of Rule Based Systems.” Theoretical
Computer Science, vol. 431, Elsevier, 2012, pp. 137–64, doi:10.1016/j.tcs.2011.12.059.
short: J. Feret, T.A. Henzinger, H. Koeppl, T. Petrov, Theoretical Computer Science
431 (2012) 137–164.
date_created: 2018-12-11T12:01:47Z
date_published: 2012-05-04T00:00:00Z
date_updated: 2026-06-18T18:39:28Z
day: '04'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2011.12.059
external_id:
isi:
- '000303302400010'
intvolume: ' 431'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.tcs.2011.12.059
month: '05'
oa: 1
oa_version: Published Version
page: 137 - 164
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '3515'
pubrep_id: '73'
quality_controlled: '1'
related_material:
record:
- id: '3719'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Lumpability abstractions of rule based systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 431
year: '2012'
...
---
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: 2026-06-18T18:41:23Z
day: '06'
ddc:
- '000'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 413
year: '2012'
...
---
_id: '3251'
abstract:
- lang: eng
text: Many infinite state systems can be seen as well-structured transition systems
(WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also
a simulation relation. WSTS are an attractive target for formal analysis because
there exist generic algorithms that decide interesting verification problems for
this class. Among the most popular algorithms are acceleration-based forward analyses
for computing the covering set. Termination of these algorithms can only be guaranteed
for flattable WSTS. Yet, many WSTS of practical interest are not flattable and
the question whether any given WSTS is flattable is itself undecidable. We therefore
propose an analysis that computes the covering set and captures the essence of
acceleration-based algorithms, but sacrifices precision for guaranteed termination.
Our analysis is an abstract interpretation whose abstract domain builds on the
ideal completion of the well-quasi-ordered state space, and a widening operator
that mimics acceleration and controls the loss of precision of the analysis. We
present instances of our framework for various classes of WSTS. Our experience
with a prototype implementation indicates that, despite the inherent precision
loss, our analysis often computes the precise covering set of the analyzed system.
acknowledgement: This research was supported in part by the European Research Council
(ERC) Advanced Investigator Grant QUAREM and by the Austrian Science Fund (FWF)
project S11402-N23.
alternative_title:
- LNCS
author:
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- 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: 'Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition
systems. In: Vol 7148. Springer; 2012:445-460. doi:10.1007/978-3-642-27940-9_29'
apa: 'Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions
for well structured transition systems (Vol. 7148, pp. 445–460). Presented at
the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia,
PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_29'
chicago: Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions
for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_29.
ieee: 'D. Zufferey, T. Wies, and T. A. Henzinger, “Ideal abstractions for well structured
transition systems,” presented at the VMCAI: Verification, Model Checking and
Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 445–460.'
ista: 'Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured
transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation,
LNCS, vol. 7148, 445–460.'
mla: Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition
Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29.
short: D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.
conference:
end_date: 2012-01-24
location: Philadelphia, PA, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2012-01-22
date_created: 2018-12-11T12:02:16Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2026-04-09T14:35:23Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-27940-9_29
ec_funded: 1
file:
- access_level: open_access
checksum: f2f0d55efa32309ad1fe65a5fcaad90c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:35Z
date_updated: 2020-07-14T12:46:05Z
file_id: '4759'
file_name: IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf
file_size: 217104
relation: main_file
file_date_updated: 2020-07-14T12:46:05Z
has_accepted_license: '1'
intvolume: ' 7148'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 445 - 460
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
publication_status: published
publisher: Springer
publist_id: '3406'
pubrep_id: '100'
quality_controlled: '1'
related_material:
record:
- id: '1405'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Ideal abstractions for well structured transition systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7148
year: '2012'
...
---
_id: '3253'
abstract:
- lang: eng
text: We describe a framework for reasoning about programs with lists carrying integer
numerical data. We use abstract domains to describe and manipulate complex constraints
on configurations of these programs mixing constraints on the shape of the heap,
sizes of the lists, on the multisets of data stored in these lists, and on the
data at their different positions. Moreover, we provide powerful techniques for
automatic validation of Hoare-triples and invariant checking, as well as for automatic
synthesis of invariants and procedure summaries using modular inter-procedural
analysis. The approach has been implemented in a tool called Celia and experimented
successfully on a large benchmark of programs.
acknowledgement: This work was partly supported by the French National Research Agency
(ANR) project Veridyc (ANR-09-SEGI-016).
alternative_title:
- LNCS
author:
- first_name: Ahmed
full_name: Bouajjani, Ahmed
last_name: Bouajjani
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- first_name: Constantin
full_name: Enea, Constantin
last_name: Enea
- first_name: Mihaela
full_name: Sighireanu, Mihaela
last_name: Sighireanu
citation:
ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Abstract domains for automated
reasoning about list manipulating programs with infinite data. In: Vol 7148. Springer;
2012:1-22. doi:10.1007/978-3-642-27940-9_1'
apa: 'Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Abstract
domains for automated reasoning about list manipulating programs with infinite
data (Vol. 7148, pp. 1–22). Presented at the VMCAI: Verification, Model Checking
and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_1'
chicago: Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
“Abstract Domains for Automated Reasoning about List Manipulating Programs with
Infinite Data,” 7148:1–22. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_1.
ieee: 'A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Abstract domains for
automated reasoning about list manipulating programs with infinite data,” presented
at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia,
PA, USA, 2012, vol. 7148, pp. 1–22.'
ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Abstract domains for automated
reasoning about list manipulating programs with infinite data. VMCAI: Verification,
Model Checking and Abstract Interpretation, LNCS, vol. 7148, 1–22.'
mla: Bouajjani, Ahmed, et al. Abstract Domains for Automated Reasoning about
List Manipulating Programs with Infinite Data. Vol. 7148, Springer, 2012,
pp. 1–22, doi:10.1007/978-3-642-27940-9_1.
short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2012, pp.
1–22.
conference:
end_date: 2012-01-24
location: Philadelphia, PA, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2012-01-22
date_created: 2018-12-11T12:02:17Z
date_published: 2012-02-26T00:00:00Z
date_updated: 2024-10-21T06:02:58Z
day: '26'
department:
- _id: ToHe
doi: 10.1007/978-3-642-27940-9_1
intvolume: ' 7148'
language:
- iso: eng
month: '02'
oa_version: None
page: 1 - 22
publication_status: published
publisher: Springer
publist_id: '3404'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstract domains for automated reasoning about list manipulating programs with
infinite data
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7148
year: '2012'
...
---
_id: '3836'
abstract:
- lang: eng
text: Hierarchical Timing Language (HTL) is a coordination language for distributed,
hard real-time applications. HTL is a hierarchical extension of Giotto and, like
its predecessor, based on the logical execution time (LET) paradigm of real-time
programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine
(or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram
structure needs to be flattened; the flattening makes separatecompilation difficult,
and may result in E machinecode of exponential size. In this paper, we propose
a generalization of the E machine, which supports a hierarchicalprogram structure
at runtime through real-time trigger mechanisms that are arranged in a tree. We
present the generalized E machine, and a modular compiler for HTL that generates
code of linear size. The compiler may generate code for any part of a given HTL
program separately in any order.
article_processing_charge: No
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- 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: Alberto
full_name: Sangiovanni Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate
compilation of hierarchical real-time programs into linear-bounded embedded machine
code. Science of Computer Programming. 2012;77(2):96-112. doi:10.1016/j.scico.2010.06.004
apa: Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., & Sangiovanni Vincentelli,
A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded
embedded machine code. Science of Computer Programming. Elsevier. https://doi.org/10.1016/j.scico.2010.06.004
chicago: Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and
Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time
Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming.
Elsevier, 2012. https://doi.org/10.1016/j.scico.2010.06.004.
ieee: A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli,
“Separate compilation of hierarchical real-time programs into linear-bounded embedded
machine code,” Science of Computer Programming, vol. 77, no. 2. Elsevier,
pp. 96–112, 2012.
ista: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012.
Separate compilation of hierarchical real-time programs into linear-bounded embedded
machine code. Science of Computer Programming. 77(2), 96–112.
mla: Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs
into Linear-Bounded Embedded Machine Code.” Science of Computer Programming,
vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:10.1016/j.scico.2010.06.004.
short: A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli,
Science of Computer Programming 77 (2012) 96–112.
date_created: 2018-12-11T12:05:26Z
date_published: 2012-02-01T00:00:00Z
date_updated: 2025-09-30T07:33:11Z
day: '01'
department:
- _id: ToHe
doi: 10.1016/j.scico.2010.06.004
external_id:
isi:
- '000298464800003'
intvolume: ' 77'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa_version: None
page: 96 - 112
publication: Science of Computer Programming
publication_status: published
publisher: Elsevier
publist_id: '2370'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Separate compilation of hierarchical real-time programs into linear-bounded
embedded machine code
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 77
year: '2012'
...
---
_id: '3846'
abstract:
- lang: eng
text: We summarize classical and recent results about two-player games played on
graphs with ω-regular objectives. These games have applications in the verification
and synthesis of reactive systems. Important distinctions are whether a graph
game is turn-based or concurrent; deterministic or stochastic; zero-sum or not.
We cluster known results and open problems according to these classifications.
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671,
by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949,
and CCR-0225610.
article_processing_charge: No
article_type: original
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. A survey of stochastic ω regular games. Journal
of Computer and System Sciences. 2012;78(2):394-413. doi:10.1016/j.jcss.2011.05.002
apa: Chatterjee, K., & Henzinger, T. A. (2012). A survey of stochastic ω regular
games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2011.05.002
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic
ω Regular Games.” Journal of Computer and System Sciences. Elsevier, 2012.
https://doi.org/10.1016/j.jcss.2011.05.002.
ieee: K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,”
Journal of Computer and System Sciences, vol. 78, no. 2. Elsevier, pp.
394–413, 2012.
ista: Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games.
Journal of Computer and System Sciences. 78(2), 394–413.
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω
Regular Games.” Journal of Computer and System Sciences, vol. 78, no. 2,
Elsevier, 2012, pp. 394–413, doi:10.1016/j.jcss.2011.05.002.
short: K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78
(2012) 394–413.
corr_author: '1'
date_created: 2018-12-11T12:05:29Z
date_published: 2012-03-02T00:00:00Z
date_updated: 2025-09-30T07:32:39Z
day: '02'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jcss.2011.05.002
external_id:
isi:
- '000299719100002'
file:
- access_level: open_access
checksum: 241b939deb4517cdd4426d49c67e3fa2
content_type: application/pdf
creator: kschuh
date_created: 2019-01-29T10:54:28Z
date_updated: 2020-07-14T12:46:17Z
file_id: '5897'
file_name: a_survey_of_stochastic_omega-regular_games.pdf
file_size: 336450
relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: ' 78'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.jcss.2011.05.002
month: '03'
oa: 1
oa_version: Submitted Version
page: 394 - 413
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '2341'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A survey of stochastic ω regular games
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 78
year: '2012'
...