---
_id: '1541'
abstract:
- lang: eng
text: We present XSpeed a parallel state-space exploration algorithm for continuous
systems with linear dynamics and nondeterministic inputs. The motivation of having
parallel algorithms is to exploit the computational power of multi-core processors
to speed-up performance. The parallelization is achieved on two fronts. First,
we propose a parallel implementation of the support function algorithm by sampling
functions in parallel. Second, we propose a parallel state-space exploration by
slicing the time horizon and computing the reachable states in the time slices
in parallel. The second method can be however applied only to a class of linear
systems with invertible dynamics and fixed input. A GP-GPU implementation is also
presented following a lazy evaluation strategy on support functions. The parallel
algorithms are implemented in the tool XSpeed. We evaluated the performance on
two benchmarks including an 28 dimension Helicopter model. Comparison with the
sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread
Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up
of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario),
the state of the art tool for reachability analysis of linear hybrid systems.
Experiments illustrate that our parallel algorithm with time slicing not only
speeds-up performance but also improves precision.
acknowledgement: This work was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants
S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
author:
- first_name: Rajarshi
full_name: Ray, Rajarshi
last_name: Ray
- first_name: Amit
full_name: Gurung, Amit
last_name: Gurung
- first_name: Binayak
full_name: Das, Binayak
last_name: Das
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating
reachability analysis on multi-core processors. 2015;9434:3-18. doi:10.1007/978-3-319-26287-1_1'
apa: 'Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., & Grosu, R.
(2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented
at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_1'
chicago: 'Ray, Rajarshi, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov,
and Radu Grosu. “XSpeed: Accelerating Reachability Analysis on Multi-Core Processors.”
Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-26287-1_1.'
ieee: 'R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, and R. Grosu, “XSpeed:
Accelerating reachability analysis on multi-core processors,” vol. 9434. Springer,
pp. 3–18, 2015.'
ista: 'Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating
reachability analysis on multi-core processors. 9434, 3–18.'
mla: 'Ray, Rajarshi, et al. XSpeed: Accelerating Reachability Analysis on Multi-Core
Processors. Vol. 9434, Springer, 2015, pp. 3–18, doi:10.1007/978-3-319-26287-1_1.'
short: R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015)
3–18.
conference:
end_date: 2015-11-19
location: Haifa, Israel
name: 'HVC: Haifa Verification Conference'
start_date: 2015-11-17
date_created: 2018-12-11T11:52:37Z
date_published: 2015-11-28T00:00:00Z
date_updated: 2020-08-11T10:09:17Z
day: '28'
department:
- _id: ToHe
doi: 10.1007/978-3-319-26287-1_1
ec_funded: 1
intvolume: ' 9434'
language:
- iso: eng
month: '11'
oa_version: None
page: 3 - 18
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '5630'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: 'XSpeed: Accelerating reachability analysis on multi-core processors'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9434
year: '2015'
...
---
_id: '1594'
abstract:
- lang: eng
text: Quantitative extensions of temporal logics have recently attracted significant
attention. In this work, we study frequency LTL (fLTL), an extension of LTL which
allows to speak about frequencies of events along an execution. Such an extension
is particularly useful for probabilistic systems that often cannot fulfil strict
qualitative guarantees on the behaviour. It has been recently shown that controller
synthesis for Markov decision processes and fLTL is decidable when all the bounds
on frequencies are 1. As a step towards a complete quantitative solution, we show
that the problem is decidable for the fragment fLTL\GU, where U does not occur
in the scope of G (but still F can). Our solution is based on a novel translation
of such quantitative formulae into equivalent deterministic automata.
acknowledgement: "This work is partly supported by the German Research Council (DFG)
as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by
the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework
Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the
CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative
Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie
Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE),
and by the ERC Start Grant (279307: Graph Games).\r\n"
alternative_title:
- LNCS
author:
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Krčál, Jan
last_name: Krčál
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
citation:
ama: 'Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency
LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12'
apa: 'Forejt, V., Krčál, J., & Kretinsky, J. (2015). Controller synthesis for
MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic
for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer.
https://doi.org/10.1007/978-3-662-48899-7_12'
chicago: Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for
MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12.
ieee: 'V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and
frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.'
ista: 'Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency
LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS,
vol. 9450, 162–177.'
mla: Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU.
Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.
short: V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
conference:
end_date: 2015-11-28
location: Suva, Fiji
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
start_date: 2015-11-24
date_created: 2018-12-11T11:52:55Z
date_published: 2015-11-22T00:00:00Z
date_updated: 2021-01-12T06:51:50Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-48899-7_12
ec_funded: 1
intvolume: ' 9450'
language:
- iso: eng
month: '11'
oa_version: None
page: 162 - 177
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _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_status: published
publisher: Springer
publist_id: '5577'
quality_controlled: '1'
scopus_import: 1
status: public
title: Controller synthesis for MDPs and frequency LTL\GU
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9450
year: '2015'
...
---
_id: '1601'
abstract:
- lang: eng
text: We propose a flexible exchange format for ω-automata, as typically used in
formal verification, and implement support for it in a range of established tools.
Our aim is to simplify the interaction of tools, helping the research community
to build upon other people’s work. A key feature of the format is the use of very
generic acceptance conditions, specified by Boolean combinations of acceptance
primitives, rather than being limited to common cases such as Büchi, Streett,
or Rabin. Such flexibility in the choice of acceptance conditions can be exploited
in applications, for example in probabilistic model checking, and furthermore
encourages the development of acceptance-agnostic tools for automata manipulations.
The format allows acceptance conditions that are either state-based or transition-based,
and also supports alternating automata.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tomáš
full_name: Babiak, Tomáš
last_name: Babiak
- first_name: František
full_name: Blahoudek, František
last_name: Blahoudek
- first_name: Alexandre
full_name: Duret Lutz, Alexandre
last_name: Duret Lutz
- first_name: Joachim
full_name: Klein, Joachim
last_name: Klein
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Daniel
full_name: Mueller, Daniel
last_name: Mueller
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Jan
full_name: Strejček, Jan
last_name: Strejček
citation:
ama: 'Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format.
In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31'
apa: 'Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller,
D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486).
Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States:
Springer. https://doi.org/10.1007/978-3-319-21690-4_31'
chicago: Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein,
Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata
Format,” 9206:479–86. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_31.
ieee: 'T. Babiak et al., “The Hanoi omega-automata format,” presented at
the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
vol. 9206, pp. 479–486.'
ista: 'Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker
D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification,
LNCS, vol. 9206, 479–486.'
mla: Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer,
2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.
short: T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller,
D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.
conference:
end_date: 2015-07-24
location: San Francisco, CA, United States
name: 'CAV: Computer Aided Verification'
start_date: 2015-07-18
date_created: 2018-12-11T11:52:57Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2021-01-12T06:51:54Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-21690-4_31
ec_funded: 1
file:
- access_level: open_access
checksum: 5885236fa88a439baba9ac6f3e801e93
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:38:12Z
date_updated: 2020-07-14T12:45:04Z
file_id: '7850'
file_name: 2015_CAV_Babiak.pdf
file_size: 1651779
relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: ' 9206'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 479 - 486
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _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: '5566'
quality_controlled: '1'
scopus_import: 1
status: public
title: The Hanoi omega-automata format
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9206
year: '2015'
...
---
_id: '1605'
abstract:
- lang: eng
text: Multiaffine hybrid automata (MHA) represent a powerful formalism to model
complex dynamical systems. This formalism is particularly suited for the representation
of biological systems which often exhibit highly non-linear behavior. In this
paper, we consider the problem of parameter identification for MHA. We present
an abstraction of MHA based on linear hybrid automata, which can be analyzed by
the SpaceEx model checker. This abstraction enables a precise handling of time-dependent
properties. We demonstrate the potential of our approach on a model of a genetic
regulatory network and a myocyte model.
acknowledgement: This work was partly supported by the European Research Council (ERC)
under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23,
S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by
the German Research Foundation (DFG) as part of the Transregional Collaborative
Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR
14 AVACS, http://www.avacs.org/).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Grégory
full_name: Batt, Grégory
last_name: Batt
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based
parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35.
doi:10.1007/978-3-319-26287-1_2'
apa: 'Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., & Grosu,
R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol.
9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa,
Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_2'
chicago: Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui
Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,”
9434:19–35. Springer, 2015. https://doi.org/10.1007/978-3-319-26287-1_2.
ieee: 'S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu,
“Abstraction-based parameter synthesis for multiaffine systems,” presented at
the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.'
ista: 'Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based
parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference,
LNCS, vol. 9434, 19–35.'
mla: Bogomolov, Sergiy, et al. Abstraction-Based Parameter Synthesis for Multiaffine
Systems. Vol. 9434, Springer, 2015, pp. 19–35, doi:10.1007/978-3-319-26287-1_2.
short: S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:,
Springer, 2015, pp. 19–35.
conference:
end_date: 2015-11-19
location: Haifa, Israel
name: 'HVC: Haifa Verification Conference'
start_date: 2015-11-17
date_created: 2018-12-11T11:52:59Z
date_published: 2015-11-28T00:00:00Z
date_updated: 2021-01-12T06:51:56Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-26287-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: 3aab260f3f34641d622030ba22645b3e
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:43:19Z
date_updated: 2020-07-14T12:45:05Z
file_id: '7851'
file_name: 2015_LNCS_Bogomolov.pdf
file_size: 1053207
relation: main_file
file_date_updated: 2020-07-14T12:45:05Z
has_accepted_license: '1'
intvolume: ' 9434'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 19 - 35
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: '5561'
quality_controlled: '1'
scopus_import: 1
status: public
title: Abstraction-based parameter synthesis for multiaffine systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9434
year: '2015'
...
---
_id: '1606'
abstract:
- lang: eng
text: 'In this paper, we present the first steps toward a runtime verification framework
for monitoring hybrid and cyber-physical systems (CPS) development tools based
on randomized differential testing. The development tools include hybrid systems
reachability analysis tools, model-based development environments like Simulink/Stateflow
(SLSF), etc. First, hybrid automaton models are randomly generated. Next, these
hybrid automaton models are translated to a number of different tools (currently,
SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using
the HyST source transformation and translation tool. Then, the hybrid automaton
models are executed in the different tools and their outputs are parsed. The final
step is the differential comparison: the outputs of the different tools are compared.
If the results do not agree (in the sense that an analysis or verification result
from one tool does not match that of another tool, ignoring timeouts, etc.), a
candidate bug is flagged and the model is saved for future analysis by the user.
The process then repeats and the monitoring continues until the user terminates
the process. We present preliminary results that have been useful in identifying
a few bugs in the analysis methods of different development tools, and in an earlier
version of HyST.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luan
full_name: Nguyen, Luan
last_name: Nguyen
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
citation:
ama: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid
analysis tools. In: 6th International Conference. Vol 9333. Springer Nature;
2015:281-286. doi:10.1007/978-3-319-23820-3_19'
apa: 'Nguyen, L., Schilling, C., Bogomolov, S., & Johnson, T. (2015). Runtime
verification for hybrid analysis tools. In 6th International Conference
(Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. https://doi.org/10.1007/978-3-319-23820-3_19'
chicago: Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson.
“Runtime Verification for Hybrid Analysis Tools.” In 6th International Conference,
9333:281–86. Springer Nature, 2015. https://doi.org/10.1007/978-3-319-23820-3_19.
ieee: L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification
for hybrid analysis tools,” in 6th International Conference, Vienna, Austria,
2015, vol. 9333, pp. 281–286.
ista: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification
for hybrid analysis tools. 6th International Conference. RV: Runtime Verification,
LNCS, vol. 9333, 281–286.'
mla: Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” 6th
International Conference, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:10.1007/978-3-319-23820-3_19.
short: L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International
Conference, Springer Nature, 2015, pp. 281–286.
conference:
end_date: 2015-09-25
location: Vienna, Austria
name: 'RV: Runtime Verification'
start_date: 2015-09-22
date_created: 2018-12-11T11:52:59Z
date_published: 2015-11-15T00:00:00Z
date_updated: 2022-02-01T14:52:59Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-319-23820-3_19
ec_funded: 1
intvolume: ' 9333'
language:
- iso: eng
month: '11'
oa_version: None
page: 281 - 286
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 6th International Conference
publication_identifier:
isbn:
- 978-3-319-23819-7
publication_status: published
publisher: Springer Nature
publist_id: '5562'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Runtime verification for hybrid analysis tools
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9333
year: '2015'
...
---
_id: '1658'
abstract:
- lang: eng
text: Continuous-time Markov chain (CTMC) models have become a central tool for
understanding the dynamics of complex reaction networks and the importance of
stochasticity in the underlying biochemical processes. When such models are employed
to answer questions in applications, in order to ensure that the model provides
a sufficiently accurate representation of the real system, it is of vital importance
that the model parameters are inferred from real measured data. This, however,
is often a formidable task and all of the existing methods fail in one case or
the other, usually because the underlying CTMC model is high-dimensional and computationally
difficult to analyze. The parameter inference methods that tend to scale best
in the dimension of the CTMC are based on so-called moment closure approximations.
However, there exists a large number of different moment closure approximations
and it is typically hard to say a priori which of the approximations is the most
suitable for the inference procedure. Here, we propose a moment-based parameter
inference method that automatically chooses the most appropriate moment closure
method. Accordingly, contrary to existing methods, the user is not required to
be experienced in moment closure techniques. In addition to that, our method adaptively
changes the approximation during the parameter inference to ensure that always
the best approximation is used, even in cases where different approximations are
best in different regions of the parameter space.
alternative_title:
- LNCS
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- 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: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
citation:
ama: Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. Adaptive moment
closure for parameter inference of biochemical reaction networks. 2015;9308:77-89.
doi:10.1007/978-3-319-23401-4_8
apa: 'Bogomolov, S., Henzinger, T. A., Podelski, A., Ruess, J., & Schilling,
C. (2015). Adaptive moment closure for parameter inference of biochemical reaction
networks. Presented at the CMSB: Computational Methods in Systems Biology, Nantes,
France: Springer. https://doi.org/10.1007/978-3-319-23401-4_8'
chicago: Bogomolov, Sergiy, Thomas A Henzinger, Andreas Podelski, Jakob Ruess, and
Christian Schilling. “Adaptive Moment Closure for Parameter Inference of Biochemical
Reaction Networks.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-23401-4_8.
ieee: S. Bogomolov, T. A. Henzinger, A. Podelski, J. Ruess, and C. Schilling, “Adaptive
moment closure for parameter inference of biochemical reaction networks,” vol.
9308. Springer, pp. 77–89, 2015.
ista: Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. 2015. Adaptive
moment closure for parameter inference of biochemical reaction networks. 9308,
77–89.
mla: Bogomolov, Sergiy, et al. Adaptive Moment Closure for Parameter Inference
of Biochemical Reaction Networks. Vol. 9308, Springer, 2015, pp. 77–89, doi:10.1007/978-3-319-23401-4_8.
short: S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, C. Schilling, 9308 (2015)
77–89.
conference:
end_date: 2015-09-18
location: Nantes, France
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2015-09-16
date_created: 2018-12-11T11:53:18Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2023-02-21T16:17:24Z
day: '01'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1007/978-3-319-23401-4_8
ec_funded: 1
intvolume: ' 9308'
language:
- iso: eng
month: '09'
oa_version: None
page: 77 - 89
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5492'
quality_controlled: '1'
related_material:
record:
- id: '1148'
relation: later_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Adaptive moment closure for parameter inference of biochemical reaction networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9308
year: '2015'
...
---
_id: '1670'
abstract:
- lang: eng
text: Planning in hybrid domains poses a special challenge due to the involved mixed
discrete-continuous dynamics. A recent solving approach for such domains is based
on applying model checking techniques on a translation of PDDL+ planning problems
to hybrid automata. However, the proposed translation is limited because must
behavior is only overapproximated, and hence, processes and events are not reflected
exactly. In this paper, we present the theoretical foundation of an exact PDDL+
translation. We propose a schema to convert a hybrid automaton with must transitions
into an equivalent hybrid automaton featuring only may transitions.
acknowledgement: This work was partly supported by the German Research Foundation
(DFG) as part of the Transregional Collaborative Research Center “Automatic Verification
and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/), by the
European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science
Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and
by the Swiss National Science Foundation (SNSF) as part of the project “Automated
Reformulation and Pruning in Factored State Spaces (ARAP)”.
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Daniele
full_name: Magazzeni, Daniele
last_name: Magazzeni
- first_name: Stefano
full_name: Minopoli, Stefano
last_name: Minopoli
- first_name: Martin
full_name: Wehrle, Martin
last_name: Wehrle
citation:
ama: 'Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. PDDL+ planning with hybrid
automata: Foundations of translating must behavior. In: AAAI Press; 2015:42-46.'
apa: 'Bogomolov, S., Magazzeni, D., Minopoli, S., & Wehrle, M. (2015). PDDL+
planning with hybrid automata: Foundations of translating must behavior (pp. 42–46).
Presented at the ICAPS: International Conference on Automated Planning and Scheduling,
Jerusalem, Israel: AAAI Press.'
chicago: 'Bogomolov, Sergiy, Daniele Magazzeni, Stefano Minopoli, and Martin Wehrle.
“PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior,”
42–46. AAAI Press, 2015.'
ieee: 'S. Bogomolov, D. Magazzeni, S. Minopoli, and M. Wehrle, “PDDL+ planning with
hybrid automata: Foundations of translating must behavior,” presented at the ICAPS:
International Conference on Automated Planning and Scheduling, Jerusalem, Israel,
2015, pp. 42–46.'
ista: 'Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. 2015. PDDL+ planning with
hybrid automata: Foundations of translating must behavior. ICAPS: International
Conference on Automated Planning and Scheduling, 42–46.'
mla: 'Bogomolov, Sergiy, et al. PDDL+ Planning with Hybrid Automata: Foundations
of Translating Must Behavior. AAAI Press, 2015, pp. 42–46.'
short: S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 2015,
pp. 42–46.
conference:
end_date: 2015-06-11
location: Jerusalem, Israel
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2015-06-07
date_created: 2018-12-11T11:53:23Z
date_published: 2015-06-01T00:00:00Z
date_updated: 2021-01-12T06:52:25Z
day: '01'
department:
- _id: ToHe
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: https://www.aaai.org/ocs/index.php/ICAPS/ICAPS15/paper/view/10606/10394
month: '06'
oa_version: None
page: 42 - 46
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: AAAI Press
publist_id: '5479'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'PDDL+ planning with hybrid automata: Foundations of translating must behavior'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1680'
abstract:
- lang: eng
text: We consider the satisfiability problem for modal logic over first-order definable
classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008]
that modal logic is decidable over classes definable by universal Horn formulae.
We provide a full classification of Horn formulae with respect to the complexity
of the corresponding satisfiability problem. It turns out, that except for the
trivial case of inconsistent formulae, local satisfiability is eitherNP-complete
or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete,
or ExpTime-complete. We also show that the finite satisfiability problem for modal
logic over Horn definable classes of frames is decidable. On the negative side,
we show undecidability of two related problems. First, we exhibit a simple universal
three-variable formula defining the class of frames over which modal logic is
undecidable. Second, we consider the satisfiability problem of bimodal logic over
Horn definable classes of frames, and also present a formula leading to undecidability.
article_number: '2'
author:
- first_name: Jakub
full_name: Michaliszyn, Jakub
last_name: Michaliszyn
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Emanuel
full_name: Kieroňski, Emanuel
last_name: Kieroňski
citation:
ama: Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal
logics. ACM Transactions on Computational Logic. 2015;17(1). doi:10.1145/2817825
apa: Michaliszyn, J., Otop, J., & Kieroňski, E. (2015). On the decidability
of elementary modal logics. ACM Transactions on Computational Logic. ACM.
https://doi.org/10.1145/2817825
chicago: Michaliszyn, Jakub, Jan Otop, and Emanuel Kieroňski. “On the Decidability
of Elementary Modal Logics.” ACM Transactions on Computational Logic. ACM,
2015. https://doi.org/10.1145/2817825.
ieee: J. Michaliszyn, J. Otop, and E. Kieroňski, “On the decidability of elementary
modal logics,” ACM Transactions on Computational Logic, vol. 17, no. 1.
ACM, 2015.
ista: Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary
modal logics. ACM Transactions on Computational Logic. 17(1), 2.
mla: Michaliszyn, Jakub, et al. “On the Decidability of Elementary Modal Logics.”
ACM Transactions on Computational Logic, vol. 17, no. 1, 2, ACM, 2015,
doi:10.1145/2817825.
short: J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational
Logic 17 (2015).
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2021-01-12T06:52:29Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2817825
ec_funded: 1
intvolume: ' 17'
issue: '1'
language:
- iso: eng
month: '09'
oa_version: None
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '5468'
quality_controlled: '1'
status: public
title: On the decidability of elementary modal logics
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2015'
...
---
_id: '1692'
abstract:
- lang: eng
text: Computing an approximation of the reachable states of a hybrid system is a
challenge, mainly because overapproximating the solutions of ODEs with a finite
number of sets does not scale well. Using template polyhedra can greatly reduce
the computational complexity, since it replaces complex operations on sets with
a small number of optimization problems. However, the use of templates may make
the over-approximation too conservative. Spurious transitions, which are falsely
considered reachable, are particularly detrimental to performance and accuracy,
and may exacerbate the state explosion problem. In this paper, we examine how
spurious transitions can be avoided with minimal computational effort. To this
end, detecting spurious transitions is reduced to the well-known problem of showing
that two convex sets are disjoint by finding a hyperplane that separates them.
We generalize this to owpipes by considering hyperplanes that evolve with time
in correspondence to the dynamics of the system. The approach is implemented in
the model checker SpaceEx and demonstrated on examples.
author:
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Marius
full_name: Greitschus, Marius
last_name: Greitschus
- first_name: Thomas
full_name: Strump, Thomas
last_name: Strump
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
citation:
ama: 'Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. Eliminating spurious
transitions in reachability with support functions. In: Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control.
ACM; 2015:149-158. doi:10.1145/2728606.2728622'
apa: 'Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., & Podelski, A.
(2015). Eliminating spurious transitions in reachability with support functions.
In Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control (pp. 149–158). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728622'
chicago: 'Frehse, Goran, Sergiy Bogomolov, Marius Greitschus, Thomas Strump, and
Andreas Podelski. “Eliminating Spurious Transitions in Reachability with Support
Functions.” In Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control, 149–58. ACM, 2015. https://doi.org/10.1145/2728606.2728622.'
ieee: 'G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, and A. Podelski, “Eliminating
spurious transitions in reachability with support functions,” in Proceedings
of the 18th International Conference on Hybrid Systems: Computation and Control,
Seattle, WA, United States, 2015, pp. 149–158.'
ista: 'Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. 2015. Eliminating
spurious transitions in reachability with support functions. Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control. HSCC:
Hybrid Systems - Computation and Control, 149–158.'
mla: 'Frehse, Goran, et al. “Eliminating Spurious Transitions in Reachability with
Support Functions.” Proceedings of the 18th International Conference on Hybrid
Systems: Computation and Control, ACM, 2015, pp. 149–58, doi:10.1145/2728606.2728622.'
short: 'G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski, in:, Proceedings
of the 18th International Conference on Hybrid Systems: Computation and Control,
ACM, 2015, pp. 149–158.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:30Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2728606.2728622
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 149 - 158
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_identifier:
isbn:
- 978-1-4503-3433-4
publication_status: published
publisher: ACM
publist_id: '5452'
quality_controlled: '1'
scopus_import: 1
status: public
title: Eliminating spurious transitions in reachability with support functions
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1690'
abstract:
- lang: eng
text: A number of powerful and scalable hybrid systems model checkers have recently
emerged. Although all of them honor roughly the same hybrid systems semantics,
they have drastically different model description languages. This situation (a)
makes it difficult to quickly evaluate a specific hybrid automaton model using
the different tools, (b) obstructs comparisons of reachability approaches, and
(c) impedes the widespread application of research results that perform model
modification and could benefit many of the tools. In this paper, we present Hyst,
a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently
taking input in the SpaceEx model format, and translating to the formats of HyCreate,
Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation
passes that serve to both ease the translation and potentially improve reachability
results for the supported tools. Although these model transformation passes could
be implemented within each tool, the Hyst approach provides a single place for
model modification, generating modified input sources for the unmodified target
tools. Our evaluation demonstrates Hyst is capable of automatically translating
benchmarks in several classes (including affine and nonlinear hybrid automata)
to the input formats of several tools. Additionally, we illustrate a general model
transformation pass based on pseudo-invariants implemented in Hyst that illustrates
the reachability improvement.
acknowledgement: The material presented in this paper is based upon work sup-ported
by the Air Force Research Laboratory’s Information Directorate (AFRL/RI) through
the Visiting Faculty Research Program (VFRP) under contract number FA8750-13-2-0115
and the Air Force Office of Scientific Research (AFOSR). Any opinions,findings,
and conclusions or recommendations expressed in this publication are those of the
authors and do not necessarily reflect the views of the AFRL/RI or AFOSR. This work
was also partly supported in part by the German Research Foundation (DFG) as part
of the Transregional Collaborative Research Center “Automatic Verification and Analysis
of Complex Systems” (SFB/TR14 AVACS, http://www.avacs.org/), by the European Research
Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF)
under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
author:
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
citation:
ama: 'Bak S, Bogomolov S, Johnson T. HYST: A source transformation and translation
tool for hybrid automaton models. In: Springer; 2015:128-133. doi:10.1145/2728606.2728630'
apa: 'Bak, S., Bogomolov, S., & Johnson, T. (2015). HYST: A source transformation
and translation tool for hybrid automaton models (pp. 128–133). Presented at the
HSCC: Hybrid Systems - Computation and Control, Seattle, WA, United States: Springer.
https://doi.org/10.1145/2728606.2728630'
chicago: 'Bak, Stanley, Sergiy Bogomolov, and Taylor Johnson. “HYST: A Source Transformation
and Translation Tool for Hybrid Automaton Models,” 128–33. Springer, 2015. https://doi.org/10.1145/2728606.2728630.'
ieee: 'S. Bak, S. Bogomolov, and T. Johnson, “HYST: A source transformation and
translation tool for hybrid automaton models,” presented at the HSCC: Hybrid Systems
- Computation and Control, Seattle, WA, United States, 2015, pp. 128–133.'
ista: 'Bak S, Bogomolov S, Johnson T. 2015. HYST: A source transformation and translation
tool for hybrid automaton models. HSCC: Hybrid Systems - Computation and Control,
128–133.'
mla: 'Bak, Stanley, et al. HYST: A Source Transformation and Translation Tool
for Hybrid Automaton Models. Springer, 2015, pp. 128–33, doi:10.1145/2728606.2728630.'
short: S. Bak, S. Bogomolov, T. Johnson, in:, Springer, 2015, pp. 128–133.
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2728606.2728630
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 128 - 133
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: '5454'
quality_controlled: '1'
status: public
title: 'HYST: A source transformation and translation tool for hybrid automaton models'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1698'
abstract:
- lang: eng
text: 'In mean-payoff games, the objective of the protagonist is to ensure that
the limit average of an infinite sequence of numeric weights is nonnegative. In
energy games, the objective is to ensure that the running sum of weights is always
nonnegative. Multi-mean-payoff and multi-energy games replace individual weights
by tuples, and the limit average (resp., running sum) of each coordinate must
be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy
games and show inter-reducibility of multi-mean-payoff and multi-energy games
for finite-memory strategies. We improve the computational complexity for solving
both classes with finite-memory strategies: we prove coNP-completeness improving
the previous known EXPSPACE bound. For memoryless strategies, we show that deciding
the existence of a winning strategy for the protagonist is NP-complete. We present
the first solution of multi-mean-payoff games with infinite-memory strategies:
we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf
objectives are coNP-complete.'
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start
grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant
QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148),
ERC Start grant (279499: inVEST).'
author:
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
- 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
- first_name: Alexander
full_name: Rabinovich, Alexander
last_name: Rabinovich
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The
complexity of multi-mean-payoff and multi-energy games. Information and Computation.
2015;241(4):177-196. doi:10.1016/j.ic.2015.03.001
apa: Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &
Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games.
Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.03.001
chicago: Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger,
Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and
Multi-Energy Games.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.03.001.
ieee: Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J.
Raskin, “The complexity of multi-mean-payoff and multi-energy games,” Information
and Computation, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.
ista: Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015.
The complexity of multi-mean-payoff and multi-energy games. Information and Computation.
241(4), 177–196.
mla: Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy
Games.” Information and Computation, vol. 241, no. 4, Elsevier, 2015, pp.
177–96, doi:10.1016/j.ic.2015.03.001.
short: Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin,
Information and Computation 241 (2015) 177–196.
date_created: 2018-12-11T11:53:32Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:52:36Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2015.03.001
ec_funded: 1
intvolume: ' 241'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1209.3234
month: '04'
oa: 1
oa_version: Preprint
page: 177 - 196
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '5443'
quality_controlled: '1'
scopus_import: 1
status: public
title: The complexity of multi-mean-payoff and multi-energy games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 241
year: '2015'
...
---
_id: '1808'
article_number: '7'
author:
- 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
citation:
ama: Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational
methods in systems biology. ACM Transactions on Modeling and Computer Simulation.
2015;25(2). doi:10.1145/2745799
apa: Gupta, A., & Henzinger, T. A. (2015). Guest editors’ introduction to special
issue on computational methods in systems biology. ACM Transactions on Modeling
and Computer Simulation. ACM. https://doi.org/10.1145/2745799
chicago: Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to
Special Issue on Computational Methods in Systems Biology.” ACM Transactions
on Modeling and Computer Simulation. ACM, 2015. https://doi.org/10.1145/2745799.
ieee: A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue
on computational methods in systems biology,” ACM Transactions on Modeling
and Computer Simulation, vol. 25, no. 2. ACM, 2015.
ista: Gupta A, Henzinger TA. 2015. Guest editors’ introduction to special issue
on computational methods in systems biology. ACM Transactions on Modeling and
Computer Simulation. 25(2), 7.
mla: Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special
Issue on Computational Methods in Systems Biology.” ACM Transactions on Modeling
and Computer Simulation, vol. 25, no. 2, 7, ACM, 2015, doi:10.1145/2745799.
short: A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation
25 (2015).
date_created: 2018-12-11T11:54:07Z
date_published: 2015-05-01T00:00:00Z
date_updated: 2021-01-12T06:53:20Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2745799
intvolume: ' 25'
issue: '2'
language:
- iso: eng
month: '05'
oa_version: None
publication: ACM Transactions on Modeling and Computer Simulation
publication_status: published
publisher: ACM
publist_id: '5302'
quality_controlled: '1'
status: public
title: Guest editors' introduction to special issue on computational methods in systems
biology
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 25
year: '2015'
...
---
_id: '1836'
abstract:
- lang: eng
text: In the standard framework for worst-case execution time (WCET) analysis of
programs, the main data structure is a single instance of integer linear programming
(ILP) that represents the whole program. The instance of this NP-hard problem
must be solved to find an estimate forWCET, and it must be refined if the estimate
is not tight.We propose a new framework for WCET analysis, based on abstract segment
trees (ASTs) as the main data structure. The ASTs have two advantages. First,
they allow computing WCET by solving a number of independent small ILP instances.
Second, ASTs store more expressive constraints, thus enabling a more efficient
and precise refinement procedure. In order to realize our framework algorithmically,
we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based
counterexample-guided refinement scheme for ASTs. Furthermore, we extend our framework
to obtain parametric estimates of WCET. We experimentally evaluate our approach
on a set of examples from WCET benchmark suites and linear-algebra packages. We
show that our analysis, with comparable effort, provides WCET estimates that in
many cases significantly improve those computed by existing tools.
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Jakob
full_name: Zwirchmayr, Jakob
last_name: Zwirchmayr
citation:
ama: Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. Segment abstraction
for worst-case execution time analysis. 2015;9032:105-131. doi:10.1007/978-3-662-46669-8_5
apa: 'Cerny, P., Henzinger, T. A., Kovács, L., Radhakrishna, A., & Zwirchmayr,
J. (2015). Segment abstraction for worst-case execution time analysis. Presented
at the ESOP: European Symposium on Programming, London, United Kingdom: Springer.
https://doi.org/10.1007/978-3-662-46669-8_5'
chicago: Cerny, Pavol, Thomas A Henzinger, Laura Kovács, Arjun Radhakrishna, and
Jakob Zwirchmayr. “Segment Abstraction for Worst-Case Execution Time Analysis.”
Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-662-46669-8_5.
ieee: P. Cerny, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr,
“Segment abstraction for worst-case execution time analysis,” vol. 9032. Springer,
pp. 105–131, 2015.
ista: Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. 2015. Segment
abstraction for worst-case execution time analysis. 9032, 105–131.
mla: Cerny, Pavol, et al. Segment Abstraction for Worst-Case Execution Time Analysis.
Vol. 9032, Springer, 2015, pp. 105–31, doi:10.1007/978-3-662-46669-8_5.
short: P. Cerny, T.A. Henzinger, L. Kovács, A. Radhakrishna, J. Zwirchmayr, 9032
(2015) 105–131.
conference:
end_date: 2015-04-18
location: London, United Kingdom
name: 'ESOP: European Symposium on Programming'
start_date: 2015-04-11
date_created: 2018-12-11T11:54:16Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2020-08-11T10:09:32Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-46669-8_5
ec_funded: 1
intvolume: ' 9032'
language:
- iso: eng
month: '04'
oa_version: None
page: 105 - 131
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: '5266'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Segment abstraction for worst-case execution time analysis
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9032
year: '2015'
...
---
_id: '1846'
abstract:
- lang: eng
text: Modal transition systems (MTS) is a well-studied specification formalism of
reactive systems supporting a step-wise refinement methodology. Despite its many
advantages, the formalism as well as its currently known extensions are incapable
of expressing some practically needed aspects in the refinement process like exclusive,
conditional and persistent choices. We introduce a new model called parametric
modal transition systems (PMTS) together with a general modal refinement notion
that overcomes many of the limitations. We investigate the computational complexity
of modal and thorough refinement checking on PMTS and its subclasses and provide
a direct encoding of the modal refinement problem into quantified Boolean formulae,
allowing us to employ state-of-the-art QBF solvers for modal refinement checking.
The experiments we report on show that the feasibility of refinement checking
is more influenced by the degree of nondeterminism rather than by the syntactic
restrictions on the types of formulae allowed in the description of the PMTS.
article_processing_charge: No
article_type: original
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Kim
full_name: Larsen, Kim
last_name: Larsen
- first_name: Mikael
full_name: Möller, Mikael
last_name: Möller
- first_name: Salomon
full_name: Sickert, Salomon
last_name: Sickert
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking
on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297.
doi:10.1007/s00236-015-0215-4
apa: Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba,
J. (2015). Refinement checking on parametric modal transition systems. Acta
Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4
chicago: Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert,
and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta
Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.
ieee: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement
checking on parametric modal transition systems,” Acta Informatica, vol.
52, no. 2–3. Springer, pp. 269–297, 2015.
ista: Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement
checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.
mla: Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.”
Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.
short: N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica
52 (2015) 269–297.
date_created: 2018-12-11T11:54:20Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:53:35Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/s00236-015-0215-4
ec_funded: 1
file:
- access_level: open_access
checksum: fb4037ddc4fc05f33080dd3547ede350
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:57:44Z
date_updated: 2020-07-14T12:45:19Z
file_id: '7854'
file_name: 2015_ActaInfo_Benes.pdf
file_size: 488482
relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: ' 52'
issue: 2-3
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 269 - 297
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: Acta Informatica
publication_status: published
publisher: Springer
publist_id: '5255'
quality_controlled: '1'
scopus_import: 1
status: public
title: Refinement checking on parametric modal transition systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 52
year: '2015'
...
---
_id: '1840'
abstract:
- lang: eng
text: In this paper, we present a method for reducing a regular, discrete-time Markov
chain (DTMC) to another DTMC with a given, typically much smaller number of states.
The cost of reduction is defined as the Kullback-Leibler divergence rate between
a projection of the original process through a partition function and a DTMC on
the correspondingly partitioned state space. Finding the reduced model with minimal
cost is computationally expensive, as it requires an exhaustive search among all
state space partitions, and an exact evaluation of the reduction cost for each
candidate partition. Our approach deals with the latter problem by minimizing
an upper bound on the reduction cost instead of minimizing the exact cost. The
proposed upper bound is easy to compute and it is tight if the original chain
is lumpable with respect to the partition. Then, we express the problem in the
form of information bottleneck optimization, and propose using the agglomerative
information bottleneck algorithm for searching a suboptimal partition greedily,
rather than exhaustively. The theory is illustrated with examples and one application
scenario in the context of modeling bio-molecular interactions.
acknowledgement: "This work was supported by the Austrian Research Association under
Project 06/12684, by the Swiss National Science Foundation (SNSF) under Grant PP00P2
128503/1, by the SystemsX.ch (the Swiss Inititative for Systems Biology), and by
a SNSF Early Postdoc.Mobility Fellowship grant P2EZP2_148797.\r\n"
author:
- first_name: Bernhard
full_name: Geiger, Bernhard
last_name: Geiger
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
- first_name: Gernot
full_name: Kubin, Gernot
last_name: Kubin
- first_name: Heinz
full_name: Koeppl, Heinz
last_name: Koeppl
citation:
ama: Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation
via information bottleneck. IEEE Transactions on Automatic Control. 2015;60(4):1010-1022.
doi:10.1109/TAC.2014.2364971
apa: Geiger, B., Petrov, T., Kubin, G., & Koeppl, H. (2015). Optimal Kullback-Leibler
aggregation via information bottleneck. IEEE Transactions on Automatic Control.
IEEE. https://doi.org/10.1109/TAC.2014.2364971
chicago: Geiger, Bernhard, Tatjana Petrov, Gernot Kubin, and Heinz Koeppl. “Optimal
Kullback-Leibler Aggregation via Information Bottleneck.” IEEE Transactions
on Automatic Control. IEEE, 2015. https://doi.org/10.1109/TAC.2014.2364971.
ieee: B. Geiger, T. Petrov, G. Kubin, and H. Koeppl, “Optimal Kullback-Leibler aggregation
via information bottleneck,” IEEE Transactions on Automatic Control, vol.
60, no. 4. IEEE, pp. 1010–1022, 2015.
ista: Geiger B, Petrov T, Kubin G, Koeppl H. 2015. Optimal Kullback-Leibler aggregation
via information bottleneck. IEEE Transactions on Automatic Control. 60(4), 1010–1022.
mla: Geiger, Bernhard, et al. “Optimal Kullback-Leibler Aggregation via Information
Bottleneck.” IEEE Transactions on Automatic Control, vol. 60, no. 4, IEEE,
2015, pp. 1010–22, doi:10.1109/TAC.2014.2364971.
short: B. Geiger, T. Petrov, G. Kubin, H. Koeppl, IEEE Transactions on Automatic
Control 60 (2015) 1010–1022.
date_created: 2018-12-11T11:54:18Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:53:33Z
day: '01'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1109/TAC.2014.2364971
intvolume: ' 60'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1304.6603
month: '04'
oa: 1
oa_version: Preprint
page: 1010 - 1022
publication: IEEE Transactions on Automatic Control
publication_identifier:
issn:
- 0018-9286
publication_status: published
publisher: IEEE
publist_id: '5262'
quality_controlled: '1'
scopus_import: 1
status: public
title: Optimal Kullback-Leibler aggregation via information bottleneck
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 60
year: '2015'
...
---
_id: '1861'
abstract:
- lang: eng
text: Continuous-time Markov chains are commonly used in practice for modeling biochemical
reaction networks in which the inherent randomness of themolecular interactions
cannot be ignored. This has motivated recent research effort into methods for
parameter inference and experiment design for such models. The major difficulty
is that such methods usually require one to iteratively solve the chemical master
equation that governs the time evolution of the probability distribution of the
system. This, however, is rarely possible, and even approximation techniques remain
limited to relatively small and simple systems. An alternative explored in this
article is to base methods on only some low-order moments of the entire probability
distribution. We summarize the theory behind such moment-based methods for parameter
inference and experiment design and provide new case studies where we investigate
their performance.
acknowledgement: "HYCON2; EC; European Commission\r\n"
article_number: '8'
author:
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
- first_name: John
full_name: Lygeros, John
last_name: Lygeros
citation:
ama: Ruess J, Lygeros J. Moment-based methods for parameter inference and experiment
design for stochastic biochemical reaction networks. ACM Transactions on Modeling
and Computer Simulation. 2015;25(2). doi:10.1145/2688906
apa: Ruess, J., & Lygeros, J. (2015). Moment-based methods for parameter inference
and experiment design for stochastic biochemical reaction networks. ACM Transactions
on Modeling and Computer Simulation. ACM. https://doi.org/10.1145/2688906
chicago: Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference
and Experiment Design for Stochastic Biochemical Reaction Networks.” ACM Transactions
on Modeling and Computer Simulation. ACM, 2015. https://doi.org/10.1145/2688906.
ieee: J. Ruess and J. Lygeros, “Moment-based methods for parameter inference and
experiment design for stochastic biochemical reaction networks,” ACM Transactions
on Modeling and Computer Simulation, vol. 25, no. 2. ACM, 2015.
ista: Ruess J, Lygeros J. 2015. Moment-based methods for parameter inference and
experiment design for stochastic biochemical reaction networks. ACM Transactions
on Modeling and Computer Simulation. 25(2), 8.
mla: Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference
and Experiment Design for Stochastic Biochemical Reaction Networks.” ACM Transactions
on Modeling and Computer Simulation, vol. 25, no. 2, 8, ACM, 2015, doi:10.1145/2688906.
short: J. Ruess, J. Lygeros, ACM Transactions on Modeling and Computer Simulation
25 (2015).
date_created: 2018-12-11T11:54:25Z
date_published: 2015-02-01T00:00:00Z
date_updated: 2021-01-12T06:53:41Z
day: '01'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1145/2688906
intvolume: ' 25'
issue: '2'
language:
- iso: eng
month: '02'
oa_version: None
publication: ACM Transactions on Modeling and Computer Simulation
publication_status: published
publisher: ACM
publist_id: '5238'
quality_controlled: '1'
scopus_import: 1
status: public
title: Moment-based methods for parameter inference and experiment design for stochastic
biochemical reaction networks
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 25
year: '2015'
...
---
_id: '1866'
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: Jean
full_name: Raskin, Jean
last_name: Raskin
citation:
ama: 'Henzinger TA, Raskin J. The equivalence problem for finite automata: Technical
perspective. Communications of the ACM. 2015;58(2):86-86. doi:10.1145/2701001'
apa: 'Henzinger, T. A., & Raskin, J. (2015). The equivalence problem for finite
automata: Technical perspective. Communications of the ACM. ACM. https://doi.org/10.1145/2701001'
chicago: 'Henzinger, Thomas A, and Jean Raskin. “The Equivalence Problem for Finite
Automata: Technical Perspective.” Communications of the ACM. ACM, 2015.
https://doi.org/10.1145/2701001.'
ieee: 'T. A. Henzinger and J. Raskin, “The equivalence problem for finite automata:
Technical perspective,” Communications of the ACM, vol. 58, no. 2. ACM,
pp. 86–86, 2015.'
ista: 'Henzinger TA, Raskin J. 2015. The equivalence problem for finite automata:
Technical perspective. Communications of the ACM. 58(2), 86–86.'
mla: 'Henzinger, Thomas A., and Jean Raskin. “The Equivalence Problem for Finite
Automata: Technical Perspective.” Communications of the ACM, vol. 58, no.
2, ACM, 2015, pp. 86–86, doi:10.1145/2701001.'
short: T.A. Henzinger, J. Raskin, Communications of the ACM 58 (2015) 86–86.
date_created: 2018-12-11T11:54:26Z
date_published: 2015-01-28T00:00:00Z
date_updated: 2021-01-12T06:53:43Z
day: '28'
department:
- _id: ToHe
doi: 10.1145/2701001
intvolume: ' 58'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 86-86
publication: Communications of the ACM
publication_status: published
publisher: ACM
publist_id: '5232'
scopus_import: 1
status: public
title: 'The equivalence problem for finite automata: Technical perspective'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2015'
...
---
_id: '1882'
abstract:
- lang: eng
text: We provide a framework for compositional and iterative design and verification
of systems with quantitative information, such as rewards, time or energy. It
is based on disjunctive modal transition systems where we allow actions to bear
various types of quantitative information. Throughout the design process the actions
can be further refined and the information made more precise. We show how to compute
the results of standard operations on the systems, including the quotient (residual),
which has not been previously considered for quantitative non-deterministic systems.
Our quantitative framework has close connections to the modal nu-calculus and
is compositional with respect to general notions of distances between systems
and the standard operations.
acknowledgement: This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.
alternative_title:
- LNCS
author:
- first_name: Uli
full_name: Fahrenberg, Uli
last_name: Fahrenberg
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Louis
full_name: Traonouez, Louis
last_name: Traonouez
citation:
ama: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative
specifications. In: Vol 8997. Springer; 2015:306-324. doi:10.1007/978-3-319-15317-9_19'
apa: 'Fahrenberg, U., Kretinsky, J., Legay, A., & Traonouez, L. (2015). Compositionality
for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS:
Formal Aspects of Component Software, Bertinoro, Italy: Springer. https://doi.org/10.1007/978-3-319-15317-9_19'
chicago: Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality
for Quantitative Specifications,” 8997:306–24. Springer, 2015. https://doi.org/10.1007/978-3-319-15317-9_19.
ieee: 'U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality
for quantitative specifications,” presented at the FACS: Formal Aspects of Component
Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.'
ista: 'Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for
quantitative specifications. FACS: Formal Aspects of Component Software, LNCS,
vol. 8997, 306–324.'
mla: Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications.
Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19.
short: U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015,
pp. 306–324.
conference:
end_date: 2014-09-12
location: Bertinoro, Italy
name: 'FACS: Formal Aspects of Component Software'
start_date: 2014-09-10
date_created: 2018-12-11T11:54:31Z
date_published: 2015-01-30T00:00:00Z
date_updated: 2021-01-12T06:53:49Z
day: '30'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-319-15317-9_19
ec_funded: 1
intvolume: ' 8997'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1408.1256
month: '01'
oa: 1
oa_version: Preprint
page: 306 - 324
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: '5216'
quality_controlled: '1'
scopus_import: 1
status: public
title: Compositionality for quantitative specifications
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8997
year: '2015'
...
---
_id: '1992'
abstract:
- lang: eng
text: "We present a method and a tool for generating succinct representations of
sets of concurrent traces. We focus on trace sets that contain all correct or
all incorrect permutations of events from a given trace. We represent trace sets
as HB-Formulas that are Boolean combinations of happens-before constraints between
events. To generate a representation of incorrect interleavings, our method iteratively
explores interleavings that violate the specification and gathers generalizations
of the discovered interleavings into an HB-Formula; its complement yields a representation
of correct interleavings.\r\n\r\nWe claim that our trace set representations can
drive diverse verification, fault localization, repair, and synthesis techniques
for concurrent programs. We demonstrate this by using our tool in three case studies
involving synchronization synthesis, bug summarization, and abstraction refinement
based verification. In each case study, our initial experimental results have
been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring
missing synchronization from an HB-Formula representing correct interleavings
of a given trace. The algorithm applies rules to rewrite specific patterns in
the HB-Formula into locks, barriers, and wait-notify constructs. In the second
case study, we use an HB-Formula representing incorrect interleavings for bug
summarization. While the HB-Formula itself is a concise counterexample summary,
we present additional inference rules to help identify specific concurrency bugs
such as data races, define-use order violations, and two-stage access bugs. In
the final case study, we present a novel predicate learning procedure that uses
HB-Formulas representing abstract counterexamples to accelerate counterexample-guided
abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure
refines the abstraction to eliminate multiple spurious abstract counterexamples
drawn from the HB-Formula."
author:
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
- first_name: Thorsten
full_name: Tarrach, Thorsten
id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
last_name: Tarrach
orcid: 0000-0003-4409-8487
citation:
ama: 'Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation
of concurrent trace sets. In: ACM; 2015:433-444. doi:10.1145/2676726.2677008'
apa: 'Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., & Tarrach,
T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented
at the POPL: Principles of Programming Languages, Mumbai, India: ACM. https://doi.org/10.1145/2676726.2677008'
chicago: Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta,
and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44.
ACM, 2015. https://doi.org/10.1145/2676726.2677008.
ieee: 'A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct
representation of concurrent trace sets,” presented at the POPL: Principles of
Programming Languages, Mumbai, India, 2015, pp. 433–444.'
ista: 'Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct
representation of concurrent trace sets. POPL: Principles of Programming Languages,
433–444.'
mla: Gupta, Ashutosh, et al. Succinct Representation of Concurrent Trace Sets.
ACM, 2015, pp. 433–44, doi:10.1145/2676726.2677008.
short: A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM,
2015, pp. 433–444.
conference:
end_date: 2015-01-17
location: Mumbai, India
name: 'POPL: Principles of Programming Languages'
start_date: 2015-01-15
date_created: 2018-12-11T11:55:05Z
date_published: 2015-01-15T00:00:00Z
date_updated: 2021-01-12T06:54:33Z
day: '15'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/2676726.2677008
file:
- access_level: open_access
checksum: f0d4395b600f410a191256ac0b73af32
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:56Z
date_updated: 2020-07-14T12:45:22Z
file_id: '5314'
file_name: IST-2015-317-v1+1_author_version.pdf
file_size: 399462
relation: main_file
file_date_updated: 2020-07-14T12:45:22Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 433 - 444
publication_identifier:
isbn:
- 978-1-4503-3300-9
publication_status: published
publisher: ACM
publist_id: '5091'
pubrep_id: '317'
quality_controlled: '1'
scopus_import: 1
status: public
title: Succinct representation of concurrent trace sets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1832'
abstract:
- lang: eng
text: 'Linearizability of concurrent data structures is usually proved by monolithic
simulation arguments relying on the identification of the so-called linearization
points. Regrettably, such proofs, whether manual or automatic, are often complicated
and scale poorly to advanced non-blocking concurrency patterns, such as helping
and optimistic updates. In response, we propose a more modular way of checking
linearizability of concurrent queue algorithms that does not involve identifying
linearization points. We reduce the task of proving linearizability with respect
to the queue specification to establishing four basic properties, each of which
can be proved independently by simpler arguments. As a demonstration of our approach,
we verify the Herlihy and Wing queue, an algorithm that is challenging to verify
by a simulation proof. '
article_number: '20'
article_processing_charge: No
article_type: original
author:
- first_name: Soham
full_name: Chakraborty, Soham
last_name: Chakraborty
- 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: Ali
full_name: Sezgin, Ali
last_name: Sezgin
- first_name: Viktor
full_name: Vafeiadis, Viktor
last_name: Vafeiadis
citation:
ama: Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability
proofs. Logical Methods in Computer Science. 2015;11(1). doi:10.2168/LMCS-11(1:20)2015
apa: Chakraborty, S., Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2015).
Aspect-oriented linearizability proofs. Logical Methods in Computer Science.
International Federation of Computational Logic. https://doi.org/10.2168/LMCS-11(1:20)2015
chicago: Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis.
“Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science.
International Federation of Computational Logic, 2015. https://doi.org/10.2168/LMCS-11(1:20)2015.
ieee: S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented
linearizability proofs,” Logical Methods in Computer Science, vol. 11,
no. 1. International Federation of Computational Logic, 2015.
ista: Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented
linearizability proofs. Logical Methods in Computer Science. 11(1), 20.
mla: Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” Logical
Methods in Computer Science, vol. 11, no. 1, 20, International Federation
of Computational Logic, 2015, doi:10.2168/LMCS-11(1:20)2015.
short: S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods
in Computer Science 11 (2015).
date_created: 2018-12-11T11:54:15Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2023-02-23T10:38:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.2168/LMCS-11(1:20)2015
ec_funded: 1
file:
- access_level: open_access
checksum: 7370e164d0a731f442424a92669efc34
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:27Z
date_updated: 2020-07-14T12:45:17Z
file_id: '4881'
file_name: IST-2015-390-v1+1_1502.07639.pdf
file_size: 380203
relation: main_file
file_date_updated: 2020-07-14T12:45:17Z
has_accepted_license: '1'
intvolume: ' 11'
issue: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '04'
oa: 1
oa_version: Published Version
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: Logical Methods in Computer Science
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '5271'
pubrep_id: '390'
quality_controlled: '1'
related_material:
record:
- id: '2328'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Aspect-oriented linearizability proofs
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 11
year: '2015'
...