---
_id: '3271'
abstract:
- lang: eng
text: In this paper we present an efficient framework for computation of persis-
tent homology of cubical data in arbitrary dimensions. An existing algorithm using
simplicial complexes is adapted to the setting of cubical complexes. The proposed
approach enables efficient application of persistent homology in domains where
the data is naturally given in a cubical form. By avoiding triangulation of the
data, we significantly reduce the size of the complex. We also present a data-structure
de- signed to compactly store and quickly manipulate cubical complexes. By means
of numerical experiments, we show high speed and memory efficiency of our ap-
proach. We compare our framework to other available implementations, showing its
superiority. Finally, we report performance on selected 3D and 4D data-sets.
alternative_title:
- Theory, Algorithms, and Applications
author:
- first_name: Hubert
full_name: Wagner, Hubert
last_name: Wagner
- first_name: Chao
full_name: Chen, Chao
id: 3E92416E-F248-11E8-B48F-1D18A9856A87
last_name: Chen
- first_name: Erald
full_name: Vuçini, Erald
last_name: Vuçini
citation:
ama: 'Wagner H, Chen C, Vuçini E. Efficient computation of persistent homology for
cubical data. In: Peikert R, Hauser H, Carr H, Fuchs R, eds. Topological Methods
in Data Analysis and Visualization II. Springer; 2011:91-106. doi:10.1007/978-3-642-23175-9_7'
apa: Wagner, H., Chen, C., & Vuçini, E. (2011). Efficient computation of persistent
homology for cubical data. In R. Peikert, H. Hauser, H. Carr, & R. Fuchs (Eds.),
Topological Methods in Data Analysis and Visualization II (pp. 91–106).
Springer. https://doi.org/10.1007/978-3-642-23175-9_7
chicago: Wagner, Hubert, Chao Chen, and Erald Vuçini. “Efficient Computation of
Persistent Homology for Cubical Data.” In Topological Methods in Data Analysis
and Visualization II, edited by Ronald Peikert, Helwig Hauser, Hamish Carr,
and Raphael Fuchs, 91–106. Springer, 2011. https://doi.org/10.1007/978-3-642-23175-9_7.
ieee: H. Wagner, C. Chen, and E. Vuçini, “Efficient computation of persistent homology
for cubical data,” in Topological Methods in Data Analysis and Visualization
II, R. Peikert, H. Hauser, H. Carr, and R. Fuchs, Eds. Springer, 2011, pp.
91–106.
ista: 'Wagner H, Chen C, Vuçini E. 2011.Efficient computation of persistent homology
for cubical data. In: Topological Methods in Data Analysis and Visualization II.
Theory, Algorithms, and Applications, , 91–106.'
mla: Wagner, Hubert, et al. “Efficient Computation of Persistent Homology for Cubical
Data.” Topological Methods in Data Analysis and Visualization II, edited
by Ronald Peikert et al., Springer, 2011, pp. 91–106, doi:10.1007/978-3-642-23175-9_7.
short: H. Wagner, C. Chen, E. Vuçini, in:, R. Peikert, H. Hauser, H. Carr, R. Fuchs
(Eds.), Topological Methods in Data Analysis and Visualization II, Springer, 2011,
pp. 91–106.
date_created: 2018-12-11T12:02:23Z
date_published: 2011-11-14T00:00:00Z
date_updated: 2021-01-12T07:42:18Z
day: '14'
department:
- _id: HeEd
doi: 10.1007/978-3-642-23175-9_7
editor:
- first_name: Ronald
full_name: Peikert, Ronald
last_name: Peikert
- first_name: Helwig
full_name: Hauser, Helwig
last_name: Hauser
- first_name: Hamish
full_name: Carr, Hamish
last_name: Carr
- first_name: Raphael
full_name: Fuchs, Raphael
last_name: Fuchs
language:
- iso: eng
month: '11'
oa_version: None
page: 91 - 106
publication: Topological Methods in Data Analysis and Visualization II
publication_status: published
publisher: Springer
publist_id: '3375'
quality_controlled: '1'
scopus_import: 1
status: public
title: Efficient computation of persistent homology for cubical data
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3323'
abstract:
- lang: eng
text: We present a new decidable logic called TREX for expressing constraints about
imperative tree data structures. In particular, TREX supports a transitive closure
operator that can express reachability constraints, which often appear in data
structure invariants. We show that our logic is closed under weakest precondition
computation, which enables its use for automated software verification. We further
show that satisfiability of formulas in TREX is decidable in NP. The low complexity
makes it an attractive alternative to more expensive logics such as monadic second-order
logic (MSOL) over trees, which have been traditionally used for reasoning about
tree data structures.
alternative_title:
- 'LNAI '
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Marco
full_name: Muñiz, Marco
last_name: Muñiz
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: 'Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative
tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:10.1007/978-3-642-22438-6_36'
apa: 'Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure
for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the
CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36'
chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure
for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36.
ieee: 'T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative
tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław,
Poland, 2011, vol. 6803, pp. 476–491.'
ista: 'Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative
tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.'
mla: Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree
Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.
short: T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.
conference:
end_date: 2011-08-05
location: Wrocław, Poland
name: 'CADE 23: Automated Deduction '
start_date: 2011-07-31
corr_author: '1'
date_created: 2018-12-11T12:02:40Z
date_published: 2011-07-19T00:00:00Z
date_updated: 2024-10-09T20:54:31Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-642-22438-6_36
intvolume: ' 6803'
language:
- iso: eng
month: '07'
oa_version: None
page: 476 - 491
publication_status: published
publisher: Springer
publist_id: '3312'
quality_controlled: '1'
related_material:
record:
- id: '5383'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: An efficient decision procedure for imperative tree data structures
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6803
year: '2011'
...
---
_id: '3324'
abstract:
- lang: eng
text: 'Automated termination provers often use the following schema to prove that
a program terminates: construct a relational abstraction of the program''s transition
relation and then show that the relational abstraction is well-founded. The focus
of current tools has been on developing sophisticated techniques for constructing
the abstractions while relying on known decidable logics (such as linear arithmetic)
to express them. We believe we can significantly increase the class of programs
that are amenable to automated termination proofs by identifying more expressive
decidable logics for reasoning about well-founded relations. We therefore present
a new decision procedure for reasoning about multiset orderings, which are among
the most powerful orderings used to prove termination. We show that, using our
decision procedure, one can automatically prove termination of natural abstractions
of programs.'
alternative_title:
- LNCS
author:
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Piskac R, Wies T. Decision procedures for automating termination proofs. In:
Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:10.1007/978-3-642-18275-4_26'
apa: 'Piskac, R., & Wies, T. (2011). Decision procedures for automating termination
proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented
at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas,
USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26'
chicago: Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination
Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011.
https://doi.org/10.1007/978-3-642-18275-4_26.
ieee: 'R. Piskac and T. Wies, “Decision procedures for automating termination proofs,”
presented at the VMCAI: Verification Model Checking and Abstract Interpretation,
Texas, USA, 2011, vol. 6538, pp. 371–386.'
ista: 'Piskac R, Wies T. 2011. Decision procedures for automating termination proofs.
VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538,
371–386.'
mla: Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination
Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011,
pp. 371–86, doi:10.1007/978-3-642-18275-4_26.
short: R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp.
371–386.
conference:
end_date: 2011-01-25
location: Texas, USA
name: 'VMCAI: Verification Model Checking and Abstract Interpretation'
start_date: 2011-01-23
date_created: 2018-12-11T12:02:40Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:39Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-18275-4_26
editor:
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: David
full_name: Schmidt, David
last_name: Schmidt
intvolume: ' 6538'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://infoscience.epfl.ch/record/170697/
month: '01'
oa: 1
oa_version: Submitted Version
page: 371 - 386
publication_status: published
publisher: Springer
publist_id: '3311'
quality_controlled: '1'
scopus_import: 1
status: public
title: Decision procedures for automating termination proofs
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6538
year: '2011'
...
---
_id: '3326'
abstract:
- lang: eng
text: 'Weighted automata map input words to numerical values. Ap- plications of
weighted automata include formal verification of quantitative properties, as well
as text, speech, and image processing. A weighted au- tomaton is defined with
respect to a semiring. For the tropical semiring, the weight of a run is the sum
of the weights of the transitions taken along the run, and the value of a word
is the minimal weight of an accepting run on it. In the 90’s, Krob studied the
decidability of problems on rational series defined with respect to the tropical
semiring. Rational series are strongly related to weighted automata, and Krob’s
results apply to them. In par- ticular, it follows from Krob’s results that the
universality problem (that is, deciding whether the values of all words are below
some threshold) is decidable for weighted automata defined with respect to the
tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable
when the domain is ∪ {∞}. In this paper we continue the study of the borders of
decidability in weighted automata, describe alternative and direct proofs of the
above results, and tighten them further. Unlike the proofs of Krob, which are
algebraic in their nature, our proofs stay in the terrain of state machines, and
the reduction is from the halting problem of a two-counter machine. This enables
us to significantly simplify Krob’s reasoning, make the un- decidability result
accessible to the automata-theoretic community, and strengthen it to apply already
to a very simple class of automata: all the states are accepting, there are no
initial nor final weights, and all the weights on the transitions are from the
set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten
also the decidability re- sults and to show that the universality problem for
weighted automata defined with respect to the tropical semiring with domain ∪
{∞}, and in fact even with domain ≥0 ∪ {∞}, is PSPACE-complete. Our results thus
draw a sharper picture about the decidability of decision problems for weighted
automata, in both the front of containment vs. universality and the front of the
∪ {∞} vs. the ∪ {∞} domains.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Shaull
full_name: Almagor, Shaull
last_name: Almagor
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Almagor S, Boker U, Kupferman O. What’s decidable about weighted automata.
In: Vol 6996. Springer; 2011:482-491. doi:10.1007/978-3-642-24372-1_37'
apa: 'Almagor, S., Boker, U., & Kupferman, O. (2011). What’s decidable about
weighted automata (Vol. 6996, pp. 482–491). Presented at the ATVA: Automated Technology
for Verification and Analysis, Taipei, Taiwan: Springer. https://doi.org/10.1007/978-3-642-24372-1_37'
chicago: Almagor, Shaull, Udi Boker, and Orna Kupferman. “What’s Decidable about
Weighted Automata,” 6996:482–91. Springer, 2011. https://doi.org/10.1007/978-3-642-24372-1_37.
ieee: 'S. Almagor, U. Boker, and O. Kupferman, “What’s decidable about weighted
automata,” presented at the ATVA: Automated Technology for Verification and Analysis,
Taipei, Taiwan, 2011, vol. 6996, pp. 482–491.'
ista: 'Almagor S, Boker U, Kupferman O. 2011. What’s decidable about weighted automata.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6996, 482–491.'
mla: Almagor, Shaull, et al. What’s Decidable about Weighted Automata. Vol.
6996, Springer, 2011, pp. 482–91, doi:10.1007/978-3-642-24372-1_37.
short: S. Almagor, U. Boker, O. Kupferman, in:, Springer, 2011, pp. 482–491.
conference:
end_date: 2011-10-14
location: Taipei, Taiwan
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2011-10-11
date_created: 2018-12-11T12:02:41Z
date_published: 2011-10-14T00:00:00Z
date_updated: 2025-01-14T12:09:37Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-24372-1_37
file:
- access_level: open_access
checksum: a7ca08a2cb1b6925f4c18a3034ae5659
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:08:32Z
date_updated: 2020-07-14T12:46:07Z
file_id: '7868'
file_name: 2011_LNCS_Almagor.pdf
file_size: 182309
relation: main_file
file_date_updated: 2020-07-14T12:46:07Z
has_accepted_license: '1'
intvolume: ' 6996'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 482 - 491
publication_status: published
publisher: Springer
publist_id: '3309'
quality_controlled: '1'
scopus_import: '1'
status: public
title: What’s decidable about weighted automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6996
year: '2011'
...
---
_id: '3327'
abstract:
- lang: eng
text: We solve the open problems of translating, when possible, all common classes
of nondeterministic word automata to deterministic and nondeterministic co-Büchi
word automata. The handled classes include Büchi, parity, Rabin, Streett and Muller
automata. The translations follow a unified approach and are all asymptotically
tight. The problem of translating Büchi automata to equivalent co-Büchi automata
was solved in [2], leaving open the problems of translating automata with richer
acceptance conditions. For these classes, one cannot easily extend or use the
construction in [2]. In particular, going via an intermediate Büchi automaton
is not optimal and might involve a blow-up exponentially higher than the known
lower bound. Other known translations are also not optimal and involve a doubly
exponential blow-up. We describe direct, simple, and asymptotically tight constructions,
involving a 2Θ(n) blow-up. The constructions are variants of the subset construction,
and allow for symbolic implementations. Beyond the theoretical importance of the
results, the new constructions have various applications, among which is an improved
algorithm for translating, when possible, LTL formulas to deterministic Büchi
word automata.
alternative_title:
- LNCS
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Boker U, Kupferman O. Co-Büching them all. In: Hofmann M, ed. Vol 6604. Springer;
2011:184-198. doi:10.1007/978-3-642-19805-2_13'
apa: 'Boker, U., & Kupferman, O. (2011). Co-Büching them all. In M. Hofmann
(Ed.) (Vol. 6604, pp. 184–198). Presented at the FoSSaCS: Foundations of Software
Science and Computation Structures, Saarbrücken, Germany: Springer. https://doi.org/10.1007/978-3-642-19805-2_13'
chicago: Boker, Udi, and Orna Kupferman. “Co-Büching Them All.” edited by Martin
Hofmann, 6604:184–98. Springer, 2011. https://doi.org/10.1007/978-3-642-19805-2_13.
ieee: 'U. Boker and O. Kupferman, “Co-Büching them all,” presented at the FoSSaCS:
Foundations of Software Science and Computation Structures, Saarbrücken, Germany,
2011, vol. 6604, pp. 184–198.'
ista: 'Boker U, Kupferman O. 2011. Co-Büching them all. FoSSaCS: Foundations of
Software Science and Computation Structures, LNCS, vol. 6604, 184–198.'
mla: Boker, Udi, and Orna Kupferman. Co-Büching Them All. Edited by Martin
Hofmann, vol. 6604, Springer, 2011, pp. 184–98, doi:10.1007/978-3-642-19805-2_13.
short: U. Boker, O. Kupferman, in:, M. Hofmann (Ed.), Springer, 2011, pp. 184–198.
conference:
end_date: 2011-04-03
location: Saarbrücken, Germany
name: 'FoSSaCS: Foundations of Software Science and Computation Structures'
start_date: 2011-03-26
date_created: 2018-12-11T12:02:41Z
date_published: 2011-03-29T00:00:00Z
date_updated: 2021-01-12T07:42:41Z
day: '29'
doi: 10.1007/978-3-642-19805-2_13
editor:
- first_name: Martin
full_name: Hofmann, Martin
last_name: Hofmann
extern: '1'
intvolume: ' 6604'
language:
- iso: eng
month: '03'
oa_version: None
page: 184 - 198
publication_status: published
publisher: Springer
publist_id: '3308'
quality_controlled: '1'
status: public
title: Co-Büching them all
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6604
year: '2011'
...
---
_id: '3332'
abstract:
- lang: eng
text: Given an algebraic hypersurface O in ℝd, how many simplices are necessary
for a simplicial complex isotopic to O? We address this problem and the variant
where all vertices of the complex must lie on O. We give asymptotically tight
worst-case bounds for algebraic plane curves. Our results gradually improve known
bounds in higher dimensions; however, the question for tight bounds remains unsolved
for d ≥ 3.
article_processing_charge: No
article_type: original
author:
- first_name: Michael
full_name: Kerber, Michael
id: 36E4574A-F248-11E8-B48F-1D18A9856A87
last_name: Kerber
orcid: 0000-0002-8030-9299
- first_name: Michael
full_name: Sagraloff, Michael
last_name: Sagraloff
citation:
ama: Kerber M, Sagraloff M. A note on the complexity of real algebraic hypersurfaces.
Graphs and Combinatorics. 2011;27(3):419-430. doi:10.1007/s00373-011-1020-7
apa: Kerber, M., & Sagraloff, M. (2011). A note on the complexity of real algebraic
hypersurfaces. Graphs and Combinatorics. Springer. https://doi.org/10.1007/s00373-011-1020-7
chicago: Kerber, Michael, and Michael Sagraloff. “A Note on the Complexity of Real
Algebraic Hypersurfaces.” Graphs and Combinatorics. Springer, 2011. https://doi.org/10.1007/s00373-011-1020-7.
ieee: M. Kerber and M. Sagraloff, “A note on the complexity of real algebraic hypersurfaces,”
Graphs and Combinatorics, vol. 27, no. 3. Springer, pp. 419–430, 2011.
ista: Kerber M, Sagraloff M. 2011. A note on the complexity of real algebraic hypersurfaces.
Graphs and Combinatorics. 27(3), 419–430.
mla: Kerber, Michael, and Michael Sagraloff. “A Note on the Complexity of Real Algebraic
Hypersurfaces.” Graphs and Combinatorics, vol. 27, no. 3, Springer, 2011,
pp. 419–30, doi:10.1007/s00373-011-1020-7.
short: M. Kerber, M. Sagraloff, Graphs and Combinatorics 27 (2011) 419–430.
corr_author: '1'
date_created: 2018-12-11T12:02:43Z
date_published: 2011-03-17T00:00:00Z
date_updated: 2025-09-30T09:09:33Z
day: '17'
ddc:
- '500'
department:
- _id: HeEd
doi: 10.1007/s00373-011-1020-7
external_id:
isi:
- '000289438700011'
file:
- access_level: open_access
checksum: a63a1e3e885dcc68f1e3dea68dfbe213
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:11:36Z
date_updated: 2020-07-14T12:46:08Z
file_id: '7869'
file_name: 2011_GraphsCombi_Kerber.pdf
file_size: 143976
relation: main_file
file_date_updated: 2020-07-14T12:46:08Z
has_accepted_license: '1'
intvolume: ' 27'
isi: 1
issue: '3'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 419 - 430
publication: Graphs and Combinatorics
publication_status: published
publisher: Springer
publist_id: '3301'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A note on the complexity of real algebraic hypersurfaces
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 27
year: '2011'
...
---
_id: '3335'
abstract:
- lang: eng
text: We study the topology of the Megaparsec Cosmic Web in terms of the scale-dependent
Betti numbers, which formalize the topological information content of the cosmic
mass distribution. While the Betti numbers do not fully quantify topology, they
extend the information beyond conventional cosmological studies of topology in
terms of genus and Euler characteristic. The richer information content of Betti
numbers goes along the availability of fast algorithms to compute them. For continuous
density fields, we determine the scale-dependence of Betti numbers by invoking
the cosmologically familiar filtration of sublevel or superlevel sets defined
by density thresholds. For the discrete galaxy distribution, however, the analysis
is based on the alpha shapes of the particles. These simplicial complexes constitute
an ordered sequence of nested subsets of the Delaunay tessellation, a filtration
defined by the scale parameter, α. As they are homotopy equivalent to the sublevel
sets of the distance field, they are an excellent tool for assessing the topological
structure of a discrete point distribution. In order to develop an intuitive understanding
for the behavior of Betti numbers as a function of α, and their relation to the
morphological patterns in the Cosmic Web, we first study them within the context
of simple heuristic Voronoi clustering models. These can be tuned to consist of
specific morphological elements of the Cosmic Web, i.e. clusters, filaments, or
sheets. To elucidate the relative prominence of the various Betti numbers in different
stages of morphological evolution, we introduce the concept of alpha tracks. Subsequently,
we address the topology of structures emerging in the standard LCDM scenario and
in cosmological scenarios with alternative dark energy content. The evolution
of the Betti numbers is shown to reflect the hierarchical evolution of the Cosmic
Web. We also demonstrate that the scale-dependence of the Betti numbers yields
a promising measure of cosmological parameters, with a potential to help in determining
the nature of dark energy and to probe primordial non-Gaussianities. We also discuss
the expected Betti numbers as a function of the density threshold for superlevel
sets of a Gaussian random field. Finally, we introduce the concept of persistent
homology. It measures scale levels of the mass distribution and allows us to separate
small from large scale features. Within the context of the hierarchical cosmic
structure formation, persistence provides a natural formalism for a multiscale
topology study of the Cosmic Web.
alternative_title:
- LNCS
arxiv: 1
author:
- first_name: Rien
full_name: Van De Weygaert, Rien
last_name: Van De Weygaert
- first_name: Gert
full_name: Vegter, Gert
last_name: Vegter
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Bernard
full_name: Jones, Bernard
last_name: Jones
- first_name: Pratyush
full_name: Pranav, Pratyush
last_name: Pranav
- first_name: Changbom
full_name: Park, Changbom
last_name: Park
- first_name: Wojciech
full_name: Hellwing, Wojciech
last_name: Hellwing
- first_name: Bob
full_name: Eldering, Bob
last_name: Eldering
- first_name: Nico
full_name: Kruithof, Nico
last_name: Kruithof
- first_name: Patrick
full_name: Bos, Patrick
last_name: Bos
- first_name: Johan
full_name: Hidding, Johan
last_name: Hidding
- first_name: Job
full_name: Feldbrugge, Job
last_name: Feldbrugge
- first_name: Eline
full_name: Ten Have, Eline
last_name: Ten Have
- first_name: Matti
full_name: Van Engelen, Matti
last_name: Van Engelen
- first_name: Manuel
full_name: Caroli, Manuel
last_name: Caroli
- first_name: Monique
full_name: Teillaud, Monique
last_name: Teillaud
citation:
ama: 'Van De Weygaert R, Vegter G, Edelsbrunner H, et al. Alpha, Betti and the Megaparsec
Universe: On the topology of the Cosmic Web. In: Gavrilova M, Tan K, Mostafavi
M, eds. Transactions on Computational Science XIV. Vol 6970. Special Issue
on Voronoi Diagrams and Delaunay Triangulation. Springer; 2011:60-101. doi:10.1007/978-3-642-25249-5_3'
apa: 'Van De Weygaert, R., Vegter, G., Edelsbrunner, H., Jones, B., Pranav, P.,
Park, C., … Teillaud, M. (2011). Alpha, Betti and the Megaparsec Universe: On
the topology of the Cosmic Web. In M. Gavrilova, K. Tan, & M. Mostafavi (Eds.),
Transactions on Computational Science XIV (Vol. 6970, pp. 60–101). Springer.
https://doi.org/10.1007/978-3-642-25249-5_3'
chicago: 'Van De Weygaert, Rien, Gert Vegter, Herbert Edelsbrunner, Bernard Jones,
Pratyush Pranav, Changbom Park, Wojciech Hellwing, et al. “Alpha, Betti and the
Megaparsec Universe: On the Topology of the Cosmic Web.” In Transactions on
Computational Science XIV, edited by Marina Gavrilova, Kenneth Tan, and Mir
Mostafavi, 6970:60–101. Special Issue on Voronoi Diagrams and Delaunay Triangulation.
Springer, 2011. https://doi.org/10.1007/978-3-642-25249-5_3.'
ieee: 'R. Van De Weygaert et al., “Alpha, Betti and the Megaparsec Universe:
On the topology of the Cosmic Web,” in Transactions on Computational Science
XIV, vol. 6970, M. Gavrilova, K. Tan, and M. Mostafavi, Eds. Springer, 2011,
pp. 60–101.'
ista: 'Van De Weygaert R, Vegter G, Edelsbrunner H, Jones B, Pranav P, Park C, Hellwing
W, Eldering B, Kruithof N, Bos P, Hidding J, Feldbrugge J, Ten Have E, Van Engelen
M, Caroli M, Teillaud M. 2011.Alpha, Betti and the Megaparsec Universe: On the
topology of the Cosmic Web. In: Transactions on Computational Science XIV. LNCS,
vol. 6970, 60–101.'
mla: 'Van De Weygaert, Rien, et al. “Alpha, Betti and the Megaparsec Universe: On
the Topology of the Cosmic Web.” Transactions on Computational Science XIV,
edited by Marina Gavrilova et al., vol. 6970, Springer, 2011, pp. 60–101, doi:10.1007/978-3-642-25249-5_3.'
short: R. Van De Weygaert, G. Vegter, H. Edelsbrunner, B. Jones, P. Pranav, C. Park,
W. Hellwing, B. Eldering, N. Kruithof, P. Bos, J. Hidding, J. Feldbrugge, E. Ten
Have, M. Van Engelen, M. Caroli, M. Teillaud, in:, M. Gavrilova, K. Tan, M. Mostafavi
(Eds.), Transactions on Computational Science XIV, Springer, 2011, pp. 60–101.
date_created: 2018-12-11T12:02:44Z
date_published: 2011-11-09T00:00:00Z
date_updated: 2021-01-12T07:42:44Z
day: '09'
department:
- _id: HeEd
doi: 10.1007/978-3-642-25249-5_3
editor:
- first_name: Marina
full_name: Gavrilova, Marina
last_name: Gavrilova
- first_name: Kenneth
full_name: Tan, Kenneth
last_name: Tan
- first_name: Mir
full_name: Mostafavi, Mir
last_name: Mostafavi
external_id:
arxiv:
- '1306.3640'
intvolume: ' 6970'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1306.3640
month: '11'
oa: 1
oa_version: Preprint
page: 60 - 101
publication: Transactions on Computational Science XIV
publication_status: published
publisher: Springer
publist_id: '3295'
quality_controlled: '1'
scopus_import: 1
series_title: Special Issue on Voronoi Diagrams and Delaunay Triangulation
status: public
title: 'Alpha, Betti and the Megaparsec Universe: On the topology of the Cosmic Web'
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6970
year: '2011'
...
---
_id: '3338'
abstract:
- lang: eng
text: 'We consider 2-player games played on a finite state space for an infinite
number of rounds. The games are concurrent: in each round, the two players (player
1 and player 2) choose their moves inde- pendently and simultaneously; the current
state and the two moves determine the successor state. We study concurrent games
with ω-regular winning conditions specified as parity objectives. We consider
the qualitative analysis problems: the computation of the almost-sure and limit-sure
winning set of states, where player 1 can ensure to win with probability 1 and
with probability arbitrarily close to 1, respec- tively. In general the almost-sure
and limit-sure winning strategies require both infinite-memory as well as infinite-precision
(to describe probabilities). We study the bounded-rationality problem for qualitative
analysis of concurrent parity games, where the strategy set for player 1 is restricted
to bounded-resource strategies. In terms of precision, strategies can be deterministic,
uniform, finite-precision or infinite- precision; and in terms of memory, strategies
can be memoryless, finite-memory or infinite-memory. We present a precise and
complete characterization of the qualitative winning sets for all combinations
of classes of strategies. In particular, we show that uniform memoryless strategies
are as powerful as finite-precision infinite-memory strategies, and infinite-precision
memoryless strategies are as power- ful as infinite-precision finite-memory strategies.
We show that the winning sets can be computed in O(n2d+3) time, where n is the
size of the game structure and 2d is the number of priorities (or colors), and
our algorithms are symbolic. The membership problem of whether a state belongs
to a winning set can be decided in NP ∩ coNP. While this complexity is the same
as for the simpler class of turn-based parity games, where in each state only
one of the two players has a choice of moves, our algorithms, that are obtained
by characterization of the winning sets as μ-calculus formulas, are considerably
more involved than those for turn-based games.'
article_number: '1107.2146'
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
citation:
ama: Chatterjee K. Bounded rationality in concurrent parity games. arXiv.:1-51.
doi:10.48550/arXiv.1107.2146
apa: Chatterjee, K. (n.d.). Bounded rationality in concurrent parity games. arXiv.
https://doi.org/10.48550/arXiv.1107.2146
chicago: Chatterjee, Krishnendu. “Bounded Rationality in Concurrent Parity Games.”
ArXiv, n.d. https://doi.org/10.48550/arXiv.1107.2146.
ieee: K. Chatterjee, “Bounded rationality in concurrent parity games,” arXiv.
pp. 1–51.
ista: Chatterjee K. Bounded rationality in concurrent parity games. arXiv, 1–51,
1107.2146.
mla: Chatterjee, Krishnendu. “Bounded Rationality in Concurrent Parity Games.” ArXiv,
1107.2146, pp. 1–51, doi:10.48550/arXiv.1107.2146.
short: K. Chatterjee, ArXiv (n.d.) 1–51.
corr_author: '1'
date_created: 2018-12-11T12:02:45Z
date_published: 2011-07-11T00:00:00Z
date_updated: 2025-06-26T09:28:52Z
day: '11'
department:
- _id: KrCh
doi: 10.48550/arXiv.1107.2146
external_id:
arxiv:
- '1107.2146'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1107.2146
month: '07'
oa: 1
oa_version: Preprint
page: 1 - 51
publication: arXiv
publication_status: submitted
publist_id: '3287'
related_material:
record:
- id: '5380'
relation: earlier_version
status: public
status: public
title: Bounded rationality in concurrent parity games
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3342'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) with ω-regular specifications
given as parity objectives. We consider the problem of computing the set of almost-sure
winning states from where the objective can be ensured with probability 1. The
algorithms for the computation of the almost-sure winning set for parity objectives
iteratively use the solutions for the almost-sure winning set for Büchi objectives
(a special case of parity objectives). Our contributions are as follows: First,
we present the first subquadratic symbolic algorithm to compute the almost-sure
winning set for MDPs with Büchi objectives; our algorithm takes O(nm) symbolic
steps as compared to the previous known algorithm that takes O(n 2) symbolic steps,
where n is the number of states and m is the number of edges of the MDP. In practice
MDPs often have constant out-degree, and then our symbolic algorithm takes O(nn) symbolic
steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second,
we present a new algorithm, namely win-lose algorithm, with the following two
properties: (a) the algorithm iteratively computes subsets of the almost-sure
winning set and its complement, as compared to all previous algorithms that discover
the almost-sure winning set upon termination; and (b) requires O(nK) symbolic
steps, where K is the maximal number of edges of strongly connected components
(scc’s) of the MDP. The win-lose algorithm requires symbolic computation of scc’s.
Third, we improve the algorithm for symbolic scc computation; the previous known
algorithm takes linear symbolic steps, and our new algorithm improves the constants
associated with the linear number of steps. In the worst case the previous known
algorithm takes 5·n symbolic steps, whereas our new algorithm takes 4 ·n symbolic
steps.'
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: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Manas
full_name: Joglekar, Manas
last_name: Joglekar
- first_name: Shah
full_name: Nisarg, Shah
last_name: Nisarg
citation:
ama: 'Chatterjee K, Henzinger M, Joglekar M, Nisarg S. Symbolic algorithms for qualitative
analysis of Markov decision processes with Büchi objectives. In: Gopalakrishnan
G, Qadeer S, eds. Vol 6806. Springer; 2011:260-276. doi:10.1007/978-3-642-22110-1_21'
apa: 'Chatterjee, K., Henzinger, M., Joglekar, M., & Nisarg, S. (2011). Symbolic
algorithms for qualitative analysis of Markov decision processes with Büchi objectives.
In G. Gopalakrishnan & S. Qadeer (Eds.) (Vol. 6806, pp. 260–276). Presented
at the CAV: Computer Aided Verification, Snowbird, USA: Springer. https://doi.org/10.1007/978-3-642-22110-1_21'
chicago: Chatterjee, Krishnendu, Monika Henzinger, Manas Joglekar, and Shah Nisarg.
“Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with
Büchi Objectives.” edited by Ganesh Gopalakrishnan and Shaz Qadeer, 6806:260–76.
Springer, 2011. https://doi.org/10.1007/978-3-642-22110-1_21.
ieee: 'K. Chatterjee, M. Henzinger, M. Joglekar, and S. Nisarg, “Symbolic algorithms
for qualitative analysis of Markov decision processes with Büchi objectives,”
presented at the CAV: Computer Aided Verification, Snowbird, USA, 2011, vol. 6806,
pp. 260–276.'
ista: 'Chatterjee K, Henzinger M, Joglekar M, Nisarg S. 2011. Symbolic algorithms
for qualitative analysis of Markov decision processes with Büchi objectives. CAV:
Computer Aided Verification, LNCS, vol. 6806, 260–276.'
mla: Chatterjee, Krishnendu, et al. Symbolic Algorithms for Qualitative Analysis
of Markov Decision Processes with Büchi Objectives. Edited by Ganesh Gopalakrishnan
and Shaz Qadeer, vol. 6806, Springer, 2011, pp. 260–76, doi:10.1007/978-3-642-22110-1_21.
short: K. Chatterjee, M. Henzinger, M. Joglekar, S. Nisarg, in:, G. Gopalakrishnan,
S. Qadeer (Eds.), Springer, 2011, pp. 260–276.
conference:
end_date: 2011-07-20
location: Snowbird, USA
name: 'CAV: Computer Aided Verification'
start_date: 2011-07-14
date_created: 2018-12-11T12:02:47Z
date_published: 2011-08-11T00:00:00Z
date_updated: 2025-09-29T13:50:32Z
day: '11'
department:
- _id: KrCh
doi: 10.1007/978-3-642-22110-1_21
editor:
- first_name: Ganesh
full_name: Gopalakrishnan, Ganesh
last_name: Gopalakrishnan
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
external_id:
arxiv:
- '1104.3348'
intvolume: ' 6806'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1104.3348
month: '08'
oa: 1
oa_version: Preprint
page: 260 - 276
project:
- _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: '3282'
quality_controlled: '1'
related_material:
record:
- id: '2831'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Symbolic algorithms for qualitative analysis of Markov decision processes with
Büchi objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6806
year: '2011'
...
---
_id: '3343'
abstract:
- lang: eng
text: 'We present faster and dynamic algorithms for the following problems arising
in probabilistic verification: Computation of the maximal end-component (mec)
decomposition of Markov decision processes (MDPs), and of the almost sure winning
set for reachability and parity objectives in MDPs. We achieve the following running
time for static algorithms in MDPs with graphs of n vertices and m edges: (1)
O(m · min{ √m, n2/3 }) for the mec decomposition, improving the longstanding O(m·n)
bound; (2) O(m·n2/3) for reachability objectives, improving the previous O(m ·
√m) bound for m > n4/3; and (3) O(m · min{ √m, n2/3 } · log(d)) for parity
objectives with d priorities, improving the previous O(m · √m · d) bound. We also
give incremental and decremental algorithms in linear time for mec decomposition
and reachability objectives and O(m · log d) time for parity ob jectives.'
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: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: 'Chatterjee K, Henzinger M. Faster and dynamic algorithms for maximal end-component
decomposition and related graph problems in probabilistic verification. In: SIAM;
2011:1318-1336. doi:10.1137/1.9781611973082.101'
apa: 'Chatterjee, K., & Henzinger, M. (2011). Faster and dynamic algorithms
for maximal end-component decomposition and related graph problems in probabilistic
verification (pp. 1318–1336). Presented at the SODA: Symposium on Discrete Algorithms,
San Francisco, SA, United States: SIAM. https://doi.org/10.1137/1.9781611973082.101'
chicago: Chatterjee, Krishnendu, and Monika Henzinger. “Faster and Dynamic Algorithms
for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic
Verification,” 1318–36. SIAM, 2011. https://doi.org/10.1137/1.9781611973082.101.
ieee: 'K. Chatterjee and M. Henzinger, “Faster and dynamic algorithms for maximal
end-component decomposition and related graph problems in probabilistic verification,”
presented at the SODA: Symposium on Discrete Algorithms, San Francisco, SA, United
States, 2011, pp. 1318–1336.'
ista: 'Chatterjee K, Henzinger M. 2011. Faster and dynamic algorithms for maximal
end-component decomposition and related graph problems in probabilistic verification.
SODA: Symposium on Discrete Algorithms, 1318–1336.'
mla: Chatterjee, Krishnendu, and Monika Henzinger. Faster and Dynamic Algorithms
for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic
Verification. SIAM, 2011, pp. 1318–36, doi:10.1137/1.9781611973082.101.
short: K. Chatterjee, M. Henzinger, in:, SIAM, 2011, pp. 1318–1336.
conference:
end_date: 2011-01-25
location: San Francisco, SA, United States
name: 'SODA: Symposium on Discrete Algorithms'
start_date: 2011-01-23
date_created: 2018-12-11T12:02:47Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2024-11-06T12:28:50Z
day: '01'
department:
- _id: KrCh
doi: 10.1137/1.9781611973082.101
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprints.cs.univie.ac.at/21/
month: '01'
oa: 1
oa_version: Submitted Version
page: 1318 - 1336
publication_status: published
publisher: SIAM
publist_id: '3278'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster and dynamic algorithms for maximal end-component decomposition and related
graph problems in probabilistic verification
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
OA_type: closed access
_id: '3344'
abstract:
- lang: eng
text: 'Games played on graphs provide the mathematical framework to analyze several
important problems in computer science as well as mathematics, such as the synthesis
problem of Church, model checking of open reactive systems and many others. On
the basis of mode of interaction of the players these games can be classified
as follows: (a) turn-based (players make moves in turns); and (b) concurrent (players
make moves simultaneously). On the basis of the information available to the players
these games can be classified as follows: (a) perfect-information (players have
perfect view of the game); and (b) partial-information (players have partial view
of the game). In this talk we will consider all these classes of games with reachability
objectives, where the goal of one player is to reach a set of target vertices
of the graph, and the goal of the opponent player is to prevent the player from
reaching the target. We will survey the results for various classes of games,
and the results range from linear time decision algorithms to EXPTIME-complete
problems to undecidable problems.'
alternative_title:
- LNCS
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
citation:
ama: 'Chatterjee K. Graph games with reachability objectives. In: 5th International
Workshop on Reachability Problems. Vol 6945. Springer; 2011:1-1. doi:10.1007/978-3-642-24288-5_1'
apa: 'Chatterjee, K. (2011). Graph games with reachability objectives. In 5th
International Workshop on Reachability Problems (Vol. 6945, pp. 1–1). Genoa,
Italy: Springer. https://doi.org/10.1007/978-3-642-24288-5_1'
chicago: Chatterjee, Krishnendu. “Graph Games with Reachability Objectives.” In
5th International Workshop on Reachability Problems, 6945:1–1. Springer,
2011. https://doi.org/10.1007/978-3-642-24288-5_1.
ieee: K. Chatterjee, “Graph games with reachability objectives,” in 5th International
Workshop on Reachability Problems, Genoa, Italy, 2011, vol. 6945, pp. 1–1.
ista: 'Chatterjee K. 2011. Graph games with reachability objectives. 5th International
Workshop on Reachability Problems. RP: Reachability Problems, LNCS, vol. 6945,
1–1.'
mla: Chatterjee, Krishnendu. “Graph Games with Reachability Objectives.” 5th
International Workshop on Reachability Problems, vol. 6945, Springer, 2011,
pp. 1–1, doi:10.1007/978-3-642-24288-5_1.
short: K. Chatterjee, in:, 5th International Workshop on Reachability Problems,
Springer, 2011, pp. 1–1.
conference:
end_date: 2011-09-30
location: Genoa, Italy
name: 'RP: Reachability Problems'
start_date: 2011-09-28
corr_author: '1'
date_created: 2018-12-11T12:02:47Z
date_published: 2011-10-15T00:00:00Z
date_updated: 2025-05-20T06:00:59Z
day: '15'
department:
- _id: KrCh
doi: 10.1007/978-3-642-24288-5_1
intvolume: ' 6945'
language:
- iso: eng
month: '10'
oa_version: None
page: 1 - 1
publication: 5th International Workshop on Reachability Problems
publication_identifier:
eisbn:
- '9783642242885'
eissn:
- 1611-3349
publication_status: published
publisher: Springer
publist_id: '3277'
quality_controlled: '1'
status: public
title: Graph games with reachability objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6945
year: '2011'
...
---
_id: '3345'
abstract:
- lang: eng
text: We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy
parity objectives. In system design, the parity objective is used to encode ω-regular
specifications, and the mean-payoff and energy objectives can be used to model
quantitative resource constraints. The energy condition re- quires that the resource
level never drops below 0, and the mean-payoff condi- tion requires that the limit-average
value of the resource consumption is within a threshold. While these two (energy
and mean-payoff) classical conditions are equivalent for two-player games, we
show that they differ for MDPs. We show that the problem of deciding whether a
state is almost-sure winning (i.e., winning with probability 1) in energy parity
MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable
in polynomial time, improving a recent PSPACE bound.
alternative_title:
- LNCS
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
citation:
ama: 'Chatterjee K, Doyen L. Energy and mean-payoff parity Markov Decision Processes.
In: Vol 6907. Springer; 2011:206-218. doi:10.1007/978-3-642-22993-0_21'
apa: 'Chatterjee, K., & Doyen, L. (2011). Energy and mean-payoff parity Markov
Decision Processes (Vol. 6907, pp. 206–218). Presented at the MFCS: Mathematical
Foundations of Computer Science, Warsaw, Poland: Springer. https://doi.org/10.1007/978-3-642-22993-0_21'
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Energy and Mean-Payoff Parity
Markov Decision Processes,” 6907:206–18. Springer, 2011. https://doi.org/10.1007/978-3-642-22993-0_21.
ieee: 'K. Chatterjee and L. Doyen, “Energy and mean-payoff parity Markov Decision
Processes,” presented at the MFCS: Mathematical Foundations of Computer Science,
Warsaw, Poland, 2011, vol. 6907, pp. 206–218.'
ista: 'Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov Decision
Processes. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6907,
206–218.'
mla: Chatterjee, Krishnendu, and Laurent Doyen. Energy and Mean-Payoff Parity
Markov Decision Processes. Vol. 6907, Springer, 2011, pp. 206–18, doi:10.1007/978-3-642-22993-0_21.
short: K. Chatterjee, L. Doyen, in:, Springer, 2011, pp. 206–218.
conference:
end_date: 2011-08-26
location: Warsaw, Poland
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2011-08-22
date_created: 2018-12-11T12:02:48Z
date_published: 2011-09-28T00:00:00Z
date_updated: 2023-02-23T12:23:59Z
day: '28'
department:
- _id: KrCh
doi: 10.1007/978-3-642-22993-0_21
external_id:
arxiv:
- '1104.2909'
intvolume: ' 6907'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1104.2909
month: '09'
oa: 1
oa_version: Preprint
page: 206 - 218
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '3276'
quality_controlled: '1'
related_material:
record:
- id: '5387'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Energy and mean-payoff parity Markov Decision Processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6907
year: '2011'
...
---
_id: '3347'
abstract:
- lang: eng
text: 'The class of omega-regular languages provides a robust specification language
in verification. Every omega-regular condition can be decomposed into a safety
part and a liveness part. The liveness part ensures that something good happens
"eventually". Finitary liveness was proposed by Alur and Henzinger as
a stronger formulation of liveness. It requires that there exists an unknown,
fixed bound b such that something good happens within b transitions. In this work
we consider automata with finitary acceptance conditions defined by finitary Buchi,
parity and Streett languages. We study languages expressible by such automata:
we give their topological complexity and present a regular-expression characterization.
We compare the expressive power of finitary automata and give optimal algorithms
for classical decisions questions. We show that the finitary languages are Sigma
2-complete; we present a complete picture of the expressive power of various classes
of automata with finitary and infinitary acceptance conditions; we show that the
languages defined by finitary parity automata exactly characterize the star-free
fragment of omega B-regular languages; and we show that emptiness is NLOGSPACE-complete
and universality as well as language inclusion are PSPACE-complete for finitary
parity and Streett automata.'
alternative_title:
- LNCS
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: Nathanaël
full_name: Fijalkow, Nathanaël
id: A1B5DD72-E997-11E9-8398-E808B6C6ADC0
last_name: Fijalkow
citation:
ama: 'Chatterjee K, Fijalkow N. Finitary languages. In: Vol 6638. Springer; 2011:216-226.
doi:10.1007/978-3-642-21254-3_16'
apa: 'Chatterjee, K., & Fijalkow, N. (2011). Finitary languages (Vol. 6638,
pp. 216–226). Presented at the LATA: Language and Automata Theory and Applications,
Tarragona, Spain: Springer. https://doi.org/10.1007/978-3-642-21254-3_16'
chicago: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Finitary Languages,” 6638:216–26.
Springer, 2011. https://doi.org/10.1007/978-3-642-21254-3_16.
ieee: 'K. Chatterjee and N. Fijalkow, “Finitary languages,” presented at the LATA:
Language and Automata Theory and Applications, Tarragona, Spain, 2011, vol. 6638,
pp. 216–226.'
ista: 'Chatterjee K, Fijalkow N. 2011. Finitary languages. LATA: Language and Automata
Theory and Applications, LNCS, vol. 6638, 216–226.'
mla: Chatterjee, Krishnendu, and Nathanaël Fijalkow. Finitary Languages.
Vol. 6638, Springer, 2011, pp. 216–26, doi:10.1007/978-3-642-21254-3_16.
short: K. Chatterjee, N. Fijalkow, in:, Springer, 2011, pp. 216–226.
conference:
end_date: 2011-05-31
location: Tarragona, Spain
name: 'LATA: Language and Automata Theory and Applications'
start_date: 2011-05-26
corr_author: '1'
date_created: 2018-12-11T12:02:48Z
date_published: 2011-06-16T00:00:00Z
date_updated: 2024-10-09T20:54:28Z
day: '16'
department:
- _id: KrCh
doi: 10.1007/978-3-642-21254-3_16
external_id:
arxiv:
- '1101.1727'
intvolume: ' 6638'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1101.1727
month: '06'
oa: 1
oa_version: Preprint
page: 216 - 226
project:
- _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: '3274'
quality_controlled: '1'
scopus_import: 1
status: public
title: Finitary languages
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6638
year: '2011'
...
---
_id: '3348'
abstract:
- lang: eng
text: We study synthesis of controllers for real-time systems, where the objective
is to stay in a given safe set. The problem is solved by obtaining winning strategies
in the setting of concurrent two-player timed automaton games with safety objectives.
To prevent a player from winning by blocking time, we restrict each player to
strategies that ensure that the player cannot be responsible for causing a zeno
run. We construct winning strategies for the controller which require access only
to (1) the system clocks (thus, controllers which require their own internal infinitely
precise clocks are not necessary), and (2) a linear (in the number of clocks)
number of memory bits. Precisely, we show that for safety objectives, a memory
of size (3 · |C|+lg(|C|+1)) bits suffices for winning controller strategies, where
C is the set of clocks of the timed automaton game, significantly improving the
previous known exponential bound. We also settle the open question of whether
winning region controller strategies require memory for safety objectives by showing
with an example the necessity of memory for region strategies to win for safety
objectives.
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: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: 'Chatterjee K, Prabhu V. Synthesis of memory efficient real time controllers
for safety objectives. In: Springer; 2011:221-230. doi:10.1145/1967701.1967734'
apa: 'Chatterjee, K., & Prabhu, V. (2011). Synthesis of memory efficient real
time controllers for safety objectives (pp. 221–230). Presented at the HSCC: Hybrid
Systems - Computation and Control, Chicago, USA: Springer. https://doi.org/10.1145/1967701.1967734'
chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory Efficient
Real Time Controllers for Safety Objectives,” 221–30. Springer, 2011. https://doi.org/10.1145/1967701.1967734.
ieee: 'K. Chatterjee and V. Prabhu, “Synthesis of memory efficient real time controllers
for safety objectives,” presented at the HSCC: Hybrid Systems - Computation and
Control, Chicago, USA, 2011, pp. 221–230.'
ista: 'Chatterjee K, Prabhu V. 2011. Synthesis of memory efficient real time controllers
for safety objectives. HSCC: Hybrid Systems - Computation and Control, 221–230.'
mla: Chatterjee, Krishnendu, and Vinayak Prabhu. Synthesis of Memory Efficient
Real Time Controllers for Safety Objectives. Springer, 2011, pp. 221–30, doi:10.1145/1967701.1967734.
short: K. Chatterjee, V. Prabhu, in:, Springer, 2011, pp. 221–230.
conference:
end_date: 2011-04-14
location: Chicago, USA
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2011-04-12
corr_author: '1'
date_created: 2018-12-11T12:02:49Z
date_published: 2011-01-31T00:00:00Z
date_updated: 2025-06-11T08:11:56Z
day: '31'
department:
- _id: KrCh
doi: 10.1145/1967701.1967734
external_id:
arxiv:
- '1101.5842'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1101.5842
month: '01'
oa: 1
oa_version: Submitted Version
page: 221 - 230
project:
- _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: '3273'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of memory efficient real time controllers for safety objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3350'
abstract:
- lang: eng
text: A controller for a discrete game with ω-regular objectives requires attention
if, intuitively, it requires measuring the state and switching from the current
control action. Minimum attention controllers are preferable in modern shared
implementations of cyber-physical systems because they produce the least burden
on system resources such as processor time or communication bandwidth. We give
algorithms to compute minimum attention controllers for ω-regular objectives in
imperfect information discrete two-player games. We show a polynomial-time reduction
from minimum attention controller synthesis to synthesis of controllers for mean-payoff
parity objectives in games of incomplete information. This gives an optimal EXPTIME-complete
synthesis algorithm. We show that the minimum attention controller problem is
decidable for infinite state systems with finite bisimulation quotients. In particular,
the problem is decidable for timed and rectangular automata.
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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Chatterjee K, Majumdar R. Minimum attention controller synthesis for omega
regular objectives. In: Fahrenberg U, Tripakis S, eds. Vol 6919. Springer; 2011:145-159.
doi:10.1007/978-3-642-24310-3_11'
apa: 'Chatterjee, K., & Majumdar, R. (2011). Minimum attention controller synthesis
for omega regular objectives. In U. Fahrenberg & S. Tripakis (Eds.) (Vol.
6919, pp. 145–159). Presented at the FORMATS: Formal Modeling and Analysis of
Timed Systems, Aalborg, Denmark: Springer. https://doi.org/10.1007/978-3-642-24310-3_11'
chicago: Chatterjee, Krishnendu, and Ritankar Majumdar. “Minimum Attention Controller
Synthesis for Omega Regular Objectives.” edited by Uli Fahrenberg and Stavros
Tripakis, 6919:145–59. Springer, 2011. https://doi.org/10.1007/978-3-642-24310-3_11.
ieee: 'K. Chatterjee and R. Majumdar, “Minimum attention controller synthesis for
omega regular objectives,” presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, Aalborg, Denmark, 2011, vol. 6919, pp. 145–159.'
ista: 'Chatterjee K, Majumdar R. 2011. Minimum attention controller synthesis for
omega regular objectives. FORMATS: Formal Modeling and Analysis of Timed Systems,
LNCS, vol. 6919, 145–159.'
mla: Chatterjee, Krishnendu, and Ritankar Majumdar. Minimum Attention Controller
Synthesis for Omega Regular Objectives. Edited by Uli Fahrenberg and Stavros
Tripakis, vol. 6919, Springer, 2011, pp. 145–59, doi:10.1007/978-3-642-24310-3_11.
short: K. Chatterjee, R. Majumdar, in:, U. Fahrenberg, S. Tripakis (Eds.), Springer,
2011, pp. 145–159.
conference:
end_date: 2011-09-23
location: Aalborg, Denmark
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2011-09-21
date_created: 2018-12-11T12:02:49Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:51Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-24310-3_11
editor:
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- first_name: Stavros
full_name: Tripakis, Stavros
last_name: Tripakis
intvolume: ' 6919'
language:
- iso: eng
month: '01'
oa_version: None
page: 145 - 159
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '3271'
quality_controlled: '1'
scopus_import: 1
status: public
title: Minimum attention controller synthesis for omega regular objectives
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6919
year: '2011'
...
---
_id: '3351'
abstract:
- lang: eng
text: In two-player games on graph, the players construct an infinite path through
the game graph and get a reward computed by a payoff function over infinite paths.
Over weighted graphs, the typical and most studied payoff functions compute the
limit-average or the discounted sum of the rewards along the path. Besides their
simple definition, these two payoff functions enjoy the property that memoryless
optimal strategies always exist. In an attempt to construct other simple payoff
functions, we define a class of payoff functions which compute an (infinite) weighted
average of the rewards. This new class contains both the limit-average and the
discounted sum functions, and we show that they are the only members of this class
which induce memoryless optimal strategies, showing that there is essentially
no other simple payoff functions.
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: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: 'Chatterjee K, Doyen L, Singh R. On memoryless quantitative objectives. In:
Owe O, Steffen M, Telle JA, eds. Vol 6914. Springer; 2011:148-159. doi:10.1007/978-3-642-22953-4_13'
apa: 'Chatterjee, K., Doyen, L., & Singh, R. (2011). On memoryless quantitative
objectives. In O. Owe, M. Steffen, & J. A. Telle (Eds.) (Vol. 6914, pp. 148–159).
Presented at the FCT: Fundamentals of Computation Theory, Oslo, Norway: Springer.
https://doi.org/10.1007/978-3-642-22953-4_13'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Rohit Singh. “On Memoryless
Quantitative Objectives.” edited by Olaf Owe, Martin Steffen, and Jan Arne Telle,
6914:148–59. Springer, 2011. https://doi.org/10.1007/978-3-642-22953-4_13.
ieee: 'K. Chatterjee, L. Doyen, and R. Singh, “On memoryless quantitative objectives,”
presented at the FCT: Fundamentals of Computation Theory, Oslo, Norway, 2011,
vol. 6914, pp. 148–159.'
ista: 'Chatterjee K, Doyen L, Singh R. 2011. On memoryless quantitative objectives.
FCT: Fundamentals of Computation Theory, LNCS, vol. 6914, 148–159.'
mla: Chatterjee, Krishnendu, et al. On Memoryless Quantitative Objectives.
Edited by Olaf Owe et al., vol. 6914, Springer, 2011, pp. 148–59, doi:10.1007/978-3-642-22953-4_13.
short: K. Chatterjee, L. Doyen, R. Singh, in:, O. Owe, M. Steffen, J.A. Telle (Eds.),
Springer, 2011, pp. 148–159.
conference:
end_date: 2011-08-25
location: Oslo, Norway
name: 'FCT: Fundamentals of Computation Theory'
start_date: 2011-08-22
date_created: 2018-12-11T12:02:50Z
date_published: 2011-04-16T00:00:00Z
date_updated: 2025-06-11T08:12:32Z
day: '16'
department:
- _id: KrCh
doi: 10.1007/978-3-642-22953-4_13
editor:
- first_name: Olaf
full_name: Owe, Olaf
last_name: Owe
- first_name: Martin
full_name: Steffen, Martin
last_name: Steffen
- first_name: Jan Arne
full_name: Telle, Jan Arne
last_name: Telle
external_id:
arxiv:
- '1104.3211'
intvolume: ' 6914'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1104.3211
month: '04'
oa: 1
oa_version: Submitted Version
page: 148 - 159
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '3270'
quality_controlled: '1'
scopus_import: '1'
status: public
title: On memoryless quantitative objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6914
year: '2011'
...
---
_id: '3357'
abstract:
- lang: eng
text: We consider two-player graph games whose objectives are request-response condition,
i.e conjunctions of conditions of the form "if a state with property Rq is visited,
then later a state with property Rp is visited". The winner of such games can
be decided in EXPTIME and the problem is known to be NP-hard. In this paper, we
close this gap by showing that this problem is, in fact, EXPTIME-complete. We
show that the problem becomes PSPACE-complete if we only consider games played
on DAGs, and NP-complete or PTIME-complete if there is only one player (depending
on whether he wants to enforce or spoil the request-response condition). We also
present near-optimal bounds on the memory needed to design winning strategies
for each player, in each case.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Florian
full_name: Horn, Florian
id: 37327ACE-F248-11E8-B48F-1D18A9856A87
last_name: Horn
citation:
ama: 'Chatterjee K, Henzinger TA, Horn F. The complexity of request-response games.
In: Dediu A-H, Inenaga S, Martín-Vide C, eds. Vol 6638. Springer; 2011:227-237.
doi:10.1007/978-3-642-21254-3_17'
apa: 'Chatterjee, K., Henzinger, T. A., & Horn, F. (2011). The complexity of
request-response games. In A.-H. Dediu, S. Inenaga, & C. Martín-Vide (Eds.)
(Vol. 6638, pp. 227–237). Presented at the LATA: Language and Automata Theory
and Applications, Tarragona, Spain: Springer. https://doi.org/10.1007/978-3-642-21254-3_17'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “The Complexity
of Request-Response Games.” edited by Adrian-Horia Dediu, Shunsuke Inenaga, and
Carlos Martín-Vide, 6638:227–37. Springer, 2011. https://doi.org/10.1007/978-3-642-21254-3_17.
ieee: 'K. Chatterjee, T. A. Henzinger, and F. Horn, “The complexity of request-response
games,” presented at the LATA: Language and Automata Theory and Applications,
Tarragona, Spain, 2011, vol. 6638, pp. 227–237.'
ista: 'Chatterjee K, Henzinger TA, Horn F. 2011. The complexity of request-response
games. LATA: Language and Automata Theory and Applications, LNCS, vol. 6638, 227–237.'
mla: Chatterjee, Krishnendu, et al. The Complexity of Request-Response Games.
Edited by Adrian-Horia Dediu et al., vol. 6638, Springer, 2011, pp. 227–37, doi:10.1007/978-3-642-21254-3_17.
short: K. Chatterjee, T.A. Henzinger, F. Horn, in:, A.-H. Dediu, S. Inenaga, C.
Martín-Vide (Eds.), Springer, 2011, pp. 227–237.
conference:
end_date: 2011-05-31
location: Tarragona, Spain
name: 'LATA: Language and Automata Theory and Applications'
start_date: 2011-05-26
corr_author: '1'
date_created: 2018-12-11T12:02:52Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2024-10-09T20:54:27Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-21254-3_17
editor:
- first_name: Adrian-Horia
full_name: Dediu, Adrian-Horia
last_name: Dediu
- first_name: Shunsuke
full_name: Inenaga, Shunsuke
last_name: Inenaga
- first_name: Carlos
full_name: Martín-Vide, Carlos
last_name: Martín-Vide
intvolume: ' 6638'
language:
- iso: eng
month: '01'
oa_version: None
page: 227 - 237
publication_status: published
publisher: Springer
publist_id: '3258'
quality_controlled: '1'
scopus_import: 1
status: public
title: The complexity of request-response games
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6638
year: '2011'
...
---
_id: '3362'
abstract:
- lang: eng
text: State-transition systems communicating by shared variables have been the underlying
model of choice for applications of model checking. Such formalisms, however,
have difficulty with modeling process creation or death and communication reconfigurability.
Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling
formalism that supports dynamic reconfiguration and creation/death of processes.
The resulting formalism supports two types of variables, data variables and reference
variables. Reference variables enable changing the connectivity between processes
and referring to instances of processes. We show how this new formalism supports
parallel composition and refinement through trace containment. DRM provide a natural
language for modeling (and ultimately reasoning about) biological systems and
multiple threads communicating through shared variables.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
- first_name: Anmol
full_name: Singh, Anmol
last_name: Singh
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. Dynamic
reactive modules. In: Vol 6901. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2011:404-418. doi:10.1007/978-3-642-23217-6_27'
apa: 'Fisher, J., Henzinger, T. A., Nickovic, D., Piterman, N., Singh, A., &
Vardi, M. (2011). Dynamic reactive modules (Vol. 6901, pp. 404–418). Presented
at the CONCUR: Concurrency Theory, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.1007/978-3-642-23217-6_27'
chicago: Fisher, Jasmin, Thomas A Henzinger, Dejan Nickovic, Nir Piterman, Anmol
Singh, and Moshe Vardi. “Dynamic Reactive Modules,” 6901:404–18. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2011. https://doi.org/10.1007/978-3-642-23217-6_27.
ieee: 'J. Fisher, T. A. Henzinger, D. Nickovic, N. Piterman, A. Singh, and M. Vardi,
“Dynamic reactive modules,” presented at the CONCUR: Concurrency Theory, Aachen,
Germany, 2011, vol. 6901, pp. 404–418.'
ista: 'Fisher J, Henzinger TA, Nickovic D, Piterman N, Singh A, Vardi M. 2011. Dynamic
reactive modules. CONCUR: Concurrency Theory, LNCS, vol. 6901, 404–418.'
mla: Fisher, Jasmin, et al. Dynamic Reactive Modules. Vol. 6901, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–18, doi:10.1007/978-3-642-23217-6_27.
short: J. Fisher, T.A. Henzinger, D. Nickovic, N. Piterman, A. Singh, M. Vardi,
in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 404–418.
conference:
end_date: 2011-09-09
location: Aachen, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2011-09-06
date_created: 2018-12-11T12:02:54Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-23217-6_27
ec_funded: 1
file:
- access_level: open_access
checksum: 6bf2453d8e52e979ddb58d17325bad26
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:17:48Z
date_updated: 2020-07-14T12:46:10Z
file_id: '7870'
file_name: 2011_CONCUR_Fisher.pdf
file_size: 337125
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6901'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 404 - 418
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '3253'
quality_controlled: '1'
scopus_import: 1
status: public
title: Dynamic reactive modules
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6901
year: '2011'
...
---
_id: '3365'
abstract:
- lang: eng
text: We present the tool Quasy, a quantitative synthesis tool. Quasy takes qualitative
and quantitative specifications and automatically constructs a system that satisfies
the qualitative specification and optimizes the quantitative specification, if
such a system exists. The user can choose between a system that satisfies and
optimizes the specifications (a) under all possible environment behaviors or (b)
under the most-likely environment behaviors given as a probability distribution
on the possible input sequences. Quasy solves these two quantitative synthesis
problems by reduction to instances of 2-player games and Markov Decision Processes
(MDPs) with quantitative winning objectives. Quasy can also be seen as a game
solver for quantitative games. Most notable, it can solve lexicographic mean-payoff
games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with
mean-payoff parity objectives.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. QUASY: quantitative synthesis
tool. In: Vol 6605. Springer; 2011:267-271. doi:10.1007/978-3-642-19835-9_24'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Singh, R. (2011). QUASY:
quantitative synthesis tool (Vol. 6605, pp. 267–271). Presented at the TACAS:
Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken,
Germany: Springer. https://doi.org/10.1007/978-3-642-19835-9_24'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
Singh. “QUASY: Quantitative Synthesis Tool,” 6605:267–71. Springer, 2011. https://doi.org/10.1007/978-3-642-19835-9_24.'
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “QUASY: quantitative
synthesis tool,” presented at the TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, Saarbrucken, Germany, 2011, vol. 6605, pp. 267–271.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2011. QUASY: quantitative
synthesis tool. TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, LNCS, vol. 6605, 267–271.'
mla: 'Chatterjee, Krishnendu, et al. QUASY: Quantitative Synthesis Tool.
Vol. 6605, Springer, 2011, pp. 267–71, doi:10.1007/978-3-642-19835-9_24.'
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2011,
pp. 267–271.
conference:
end_date: 2011-04-03
location: Saarbrucken, Germany
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2011-03-26
date_created: 2018-12-11T12:02:55Z
date_published: 2011-09-29T00:00:00Z
date_updated: 2021-01-12T07:42:58Z
day: '29'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-19835-9_24
file:
- access_level: open_access
checksum: 762e52eb296f6dbfbf2a75d98b8ebaee
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:37Z
date_updated: 2020-07-14T12:46:10Z
file_id: '5022'
file_name: IST-2012-77-v1+1_QUASY-_quantitative_synthesis_tool.pdf
file_size: 475661
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6605'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 267 - 271
publication_status: published
publisher: Springer
publist_id: '3248'
pubrep_id: '77'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'QUASY: quantitative synthesis tool'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6605
year: '2011'
...
---
_id: '3366'
abstract:
- lang: eng
text: 'We present an algorithmic method for the quantitative, performance-aware
synthesis of concurrent programs. The input consists of a nondeterministic partial
program and of a parametric performance model. The nondeterminism allows the programmer
to omit which (if any) synchronization construct is used at a particular program
location. The performance model, specified as a weighted automaton, can capture
system architectures by assigning different costs to actions such as locking,
context switching, and memory and cache accesses. The quantitative synthesis problem
is to automatically resolve the nondeterminism of the partial program so that
both correctness is guaranteed and performance is optimal. As is standard for
shared memory concurrency, correctness is formalized "specification free",
in particular as race freedom or deadlock freedom. For worst-case (average-case)
performance, we show that the problem can be reduced to 2-player graph games (with
probabilistic transitions) with quantitative objectives. While we show, using
game-theoretic methods, that the synthesis problem is Nexp-complete, we present
an algorithmic method and an implementation that works efficiently for concurrent
programs and performance models of practical interest. We have implemented a prototype
tool and used it to synthesize finite-state concurrent programs that exhibit different
programming patterns, for several performance models representing different architectures. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: 'Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. Quantitative
synthesis for concurrent programs. In: Gopalakrishnan G, Qadeer S, eds. Vol 6806.
Springer; 2011:243-259. doi:10.1007/978-3-642-22110-1_20'
apa: 'Cerny, P., Chatterjee, K., Henzinger, T. A., Radhakrishna, A., & Singh,
R. (2011). Quantitative synthesis for concurrent programs. In G. Gopalakrishnan
& S. Qadeer (Eds.) (Vol. 6806, pp. 243–259). Presented at the CAV: Computer
Aided Verification, Snowbird, USA: Springer. https://doi.org/10.1007/978-3-642-22110-1_20'
chicago: Cerny, Pavol, Krishnendu Chatterjee, Thomas A Henzinger, Arjun Radhakrishna,
and Rohit Singh. “Quantitative Synthesis for Concurrent Programs.” edited by Ganesh
Gopalakrishnan and Shaz Qadeer, 6806:243–59. Springer, 2011. https://doi.org/10.1007/978-3-642-22110-1_20.
ieee: 'P. Cerny, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh,
“Quantitative synthesis for concurrent programs,” presented at the CAV: Computer
Aided Verification, Snowbird, USA, 2011, vol. 6806, pp. 243–259.'
ista: 'Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. 2011. Quantitative
synthesis for concurrent programs. CAV: Computer Aided Verification, LNCS, vol.
6806, 243–259.'
mla: Cerny, Pavol, et al. Quantitative Synthesis for Concurrent Programs.
Edited by Ganesh Gopalakrishnan and Shaz Qadeer, vol. 6806, Springer, 2011, pp.
243–59, doi:10.1007/978-3-642-22110-1_20.
short: P. Cerny, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, R. Singh, in:,
G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 243–259.
conference:
end_date: 2011-07-20
location: Snowbird, USA
name: 'CAV: Computer Aided Verification'
start_date: 2011-07-14
corr_author: '1'
date_created: 2018-12-11T12:02:55Z
date_published: 2011-04-21T00:00:00Z
date_updated: 2024-10-21T06:03:04Z
day: '21'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-642-22110-1_20
ec_funded: 1
editor:
- first_name: Ganesh
full_name: Gopalakrishnan, Ganesh
last_name: Gopalakrishnan
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
file:
- access_level: open_access
checksum: c033689355f45742dc7c99b5af13ce7a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:51Z
date_updated: 2020-07-14T12:46:10Z
file_id: '5174'
file_name: IST-2012-76-v1+1_Quantitative_synthesis_for_concurrent_programs.pdf
file_size: 508946
relation: main_file
file_date_updated: 2020-07-14T12:46:10Z
has_accepted_license: '1'
intvolume: ' 6806'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 243 - 259
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '3247'
pubrep_id: '76'
quality_controlled: '1'
related_material:
record:
- id: '5388'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Quantitative synthesis for concurrent programs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6806
year: '2011'
...