---
_id: '1227'
abstract:
- lang: eng
text: Many biological systems can be modeled as multiaffine hybrid systems. Due
to the nonlinearity of multiaffine systems, it is difficult to verify their properties
of interest directly. A common strategy to tackle this problem is to construct
and analyze a discrete overapproximation of the original system. However, the
conservativeness of a discrete abstraction significantly determines the level
of confidence we can have in the properties of the original system. In this paper,
in order to reduce the conservativeness of a discrete abstraction, we propose
a new method based on a sufficient and necessary decision condition for computing
discrete transitions between states in the abstract system. We assume the state
space partition of a multiaffine system to be based on a set of multivariate polynomials.
Hence, a rectangular partition defined in terms of polynomials of the form (xi
− c) is just a simple case of multivariate polynomial partition, and the new decision
condition applies naturally. We analyze and demonstrate the improvement of our
method over the existing methods using some examples.
acknowledgement: This research was supported in part 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
article_processing_charge: No
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- 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
- 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: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine
systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9'
apa: 'Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang,
Y., & Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol.
9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France:
Springer. https://doi.org/10.1007/978-3-319-47151-8_9'
chicago: Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger,
Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,”
9957:128–44. Springer, 2016. https://doi.org/10.1007/978-3-319-47151-8_9.
ieee: 'H. Kong et al., “Discrete abstraction of multiaffine systems,” presented
at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.'
ista: 'Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling
C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology,
LNCS, vol. 9957, 128–144.'
mla: Kong, Hui, et al. Discrete Abstraction of Multiaffine Systems. Vol.
9957, Springer, 2016, pp. 128–44, doi:10.1007/978-3-319-47151-8_9.
short: H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C.
Schilling, in:, Springer, 2016, pp. 128–144.
conference:
end_date: 2016-10-21
location: Grenoble, France
name: 'HSB: Hybrid Systems Biology'
start_date: 2016-10-20
date_created: 2018-12-11T11:50:49Z
date_published: 2016-09-25T00:00:00Z
date_updated: 2025-09-22T09:24:50Z
day: '25'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-47151-8_9
external_id:
isi:
- '000389928100009'
file:
- access_level: open_access
checksum: 994e164b558c47bacf8dc066dd27c8fc
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:49Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4840'
file_name: IST-2017-781-v1+1_main.pdf
file_size: 683955
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 9957'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 128 - 144
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _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: '6107'
pubrep_id: '781'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discrete abstraction of multiaffine systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9957
year: '2016'
...
---
_id: '1230'
abstract:
- lang: eng
text: Concolic testing is a promising method for generating test suites for large
programs. However, it suffers from the path-explosion problem and often fails
to find tests that cover difficult-to-reach parts of programs. In contrast, model
checkers based on counterexample-guided abstraction refinement explore programs
exhaustively, while failing to scale on large programs with precision. In this
paper, we present a novel method that iteratively combines concolic testing and
model checking to find a test suite for a given coverage criterion. If concolic
testing fails to cover some test goals, then the model checker refines its program
abstraction to prove more paths infeasible, which reduces the search space for
concolic testing. We have implemented our method on top of the concolictesting
tool Crest and the model checker CpaChecker. We evaluated our tool on a collection
of programs and a category of SvComp benchmarks. In our experiments, we observed
an improvement in branch coverage compared to Crest from 48% to 63% in the best
case, and from 66% to 71% on average.
acknowledgement: "We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand
Michael Tautschnig for help with preparing the experiments. This research 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 (RiSE) and Z211-N23 (Wittgenstein
Award)."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: 'Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol
9583. Springer; 2016:328-347. doi:10.1007/978-3-662-49122-5_16'
apa: 'Daca, P., Gupta, A., & Henzinger, T. A. (2016). Abstraction-driven concolic
testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model
Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. https://doi.org/10.1007/978-3-662-49122-5_16'
chicago: Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven
Concolic Testing,” 9583:328–47. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_16.
ieee: 'P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,”
presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.'
ista: 'Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583,
328–347.'
mla: Daca, Przemyslaw, et al. Abstraction-Driven Concolic Testing. Vol. 9583,
Springer, 2016, pp. 328–47, doi:10.1007/978-3-662-49122-5_16.
short: P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.
conference:
end_date: 2016-01-19
location: St. Petersburg, FL, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2016-01-17
date_created: 2018-12-11T11:50:50Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_16
ec_funded: 1
external_id:
arxiv:
- '1511.02615'
isi:
- '000375148800016'
intvolume: ' 9583'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1511.02615
month: '01'
oa: 1
oa_version: Preprint
page: 328 - 347
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: Formal methods for the design and analysis of complex systems
- _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: '6104'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Abstraction-driven concolic testing
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9583
year: '2016'
...
---
_id: '1234'
abstract:
- lang: eng
text: We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under\r\ngrant agreement 267989 (QUAREM), the Austrian Science Fund
\ (FWF) under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh
Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility
Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation
under grant agreement P202/12/G061."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Faster
statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129).
Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-662-49674-9_7'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29.
Springer, 2016. https://doi.org/10.1007/978-3-662-49674-9_7.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” presented at the TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands,
2016, vol. 9636, pp. 112–129.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model
checking for unbounded temporal properties. TACAS: Tools and Algorithms for the
Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.'
mla: Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded
Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp.
112–129.
conference:
end_date: 2016-04-08
location: Eindhoven, The Netherlands
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2016-04-02
date_created: 2018-12-11T11:50:51Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1007/978-3-662-49674-9_7
ec_funded: 1
external_id:
arxiv:
- '1504.05739'
isi:
- '000406428000007'
intvolume: ' 9636'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '01'
oa: 1
oa_version: Preprint
page: 112 - 129
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: Formal methods for the design and analysis of complex systems
- _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: '6099'
quality_controlled: '1'
related_material:
record:
- id: '471'
relation: later_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Faster statistical model checking for unbounded temporal properties
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9636
year: '2016'
...
---
_id: '1256'
abstract:
- lang: eng
text: Simulink is widely used for model driven development (MDD) of industrial software
systems. Typically, the Simulink based development is initiated from Stateflow
modeling, followed by simulation, validation and code generation mapped to physical
execution platforms. However, recent industrial trends have raised the demands
of rigorous verification on safety-critical applications, which is unfortunately
challenging for Simulink. In this paper, we present an approach to bridge the
Stateflow based model driven development and a well- defined rigorous verification.
First, we develop a self- contained toolkit to translate Stateflow model into
timed automata, where major advanced modeling features in Stateflow are supported.
Taking advantage of the strong verification capability of Uppaal, we can not only
find bugs in Stateflow models which are missed by Simulink Design Verifier, but
also check more important temporal properties. Next, we customize a runtime verifier
for the generated nonintrusive VHDL and C code of Stateflow model for monitoring.
The major strength of the customization is the flexibility to collect and analyze
runtime properties with a pure software monitor, which opens more opportunities
for engineers to achieve high reliability of the target system compared with the
traditional act that only relies on Simulink Polyspace. We incorporate these two
parts into original Stateflow based MDD seamlessly. In this way, safety-critical
properties are both verified at the model level, and at the consistent system
implementation level with physical execution environment in consideration. We
apply our approach on a train controller design, and the verified implementation
is tested and deployed on a real hardware platform.
acknowledgement: This work is supported in part by NSF CNS 13-30077, NSF CNS 13-29886,
NSF CNS 15-45002, NSFC 61303014, NSFC 61202010, and NSFC 91218302.
article_number: '7461337'
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Yixiao
full_name: Yang, Yixiao
last_name: Yang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ming
full_name: Gu, Ming
last_name: Gu
- first_name: Jiaguang
full_name: Sun, Jiaguang
last_name: Sun
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
citation:
ama: 'Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation:
A verification approach and a real-time train controller design. In: IEEE; 2016.
doi:10.1109/RTAS.2016.7461337'
apa: 'Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., & Sha, L. (2016).
From stateflow simulation to verified implementation: A verification approach
and a real-time train controller design. Presented at the RTAS: Real-time and
Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. https://doi.org/10.1109/RTAS.2016.7461337'
chicago: 'Jiang, Yu, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, and
Lui Sha. “From Stateflow Simulation to Verified Implementation: A Verification
Approach and a Real-Time Train Controller Design.” IEEE, 2016. https://doi.org/10.1109/RTAS.2016.7461337.'
ieee: 'Y. Jiang et al., “From stateflow simulation to verified implementation:
A verification approach and a real-time train controller design,” presented at
the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna,
Austria, 2016.'
ista: 'Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L. 2016. From stateflow
simulation to verified implementation: A verification approach and a real-time
train controller design. RTAS: Real-time and Embedded Technology and Applications
Symposium, 7461337.'
mla: 'Jiang, Yu, et al. From Stateflow Simulation to Verified Implementation:
A Verification Approach and a Real-Time Train Controller Design. 7461337,
IEEE, 2016, doi:10.1109/RTAS.2016.7461337.'
short: Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.
conference:
end_date: 2016-04-14
location: Vienna, Austria
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
start_date: 2016-04-11
date_created: 2018-12-11T11:50:58Z
date_published: 2016-04-27T00:00:00Z
date_updated: 2021-01-12T06:49:26Z
day: '27'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1109/RTAS.2016.7461337
file:
- access_level: open_access
checksum: 42f0462911cc9957f2356b12fb33b4b6
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:31Z
date_updated: 2020-07-14T12:44:41Z
file_id: '4949'
file_name: IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf
file_size: 1293599
relation: main_file
file_date_updated: 2020-07-14T12:44:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
publication_status: published
publisher: IEEE
publist_id: '6069'
pubrep_id: '780'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'From stateflow simulation to verified implementation: A verification approach
and a real-time train controller design'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1335'
abstract:
- lang: eng
text: In this paper we review various automata-theoretic formalisms for expressing
quantitative properties. We start with finite-state Boolean automata that express
the traditional regular properties. We then consider weighted ω-automata that
can measure the average density of events, which finite-state Boolean automata
cannot. However, even weighted ω-automata cannot express basic performance properties
like average response time. We finally consider two formalisms of weighted ω-automata
with monitors, where the monitors are either (a) counters or (b) weighted automata
themselves. We present a translation result to establish that these two formalisms
are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata,
and can express average response time property. They present a natural, robust,
and expressive framework for quantitative specifications, with important decidable
properties.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol
9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor
automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium,
Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,”
presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016,
vol. 9837, pp. 23–38.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata.
SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.'
mla: Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837,
Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.
conference:
end_date: 2016-09-10
location: Edinburgh, United Kingdom
name: 'SAS: Static Analysis Symposium'
start_date: 2016-09-08
corr_author: '1'
date_created: 2018-12-11T11:51:26Z
date_published: 2016-08-31T00:00:00Z
date_updated: 2025-09-22T08:19:49Z
day: '31'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-53413-7_2
ec_funded: 1
external_id:
arxiv:
- '1604.06764'
isi:
- '000388924600002'
intvolume: ' 9837'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '08'
oa: 1
oa_version: Preprint
page: 23 - 38
project:
- _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: Formal methods for the design and analysis of complex systems
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '5932'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative monitor automata
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9837
year: '2016'
...
---
_id: '1341'
abstract:
- lang: eng
text: In resource allocation games, selfish players share resources that are needed
in order to fulfill their objectives. The cost of using a resource depends on
the load on it. In the traditional setting, the players make their choices concurrently
and in one-shot. That is, a strategy for a player is a subset of the resources.
We introduce and study dynamic resource allocation games. In this setting, the
game proceeds in phases. In each phase each player chooses one resource. A scheduler
dictates the order in which the players proceed in a phase, possibly scheduling
several players to proceed concurrently. The game ends when each player has collected
a set of resources that fulfills his objective. The cost for each player then
depends on this set as well as on the load on the resources in it – we consider
both congestion and cost-sharing games. We argue that the dynamic setting is the
suitable setting for many applications in practice. We study the stability of
dynamic resource allocation games, where the appropriate notion of stability is
that of subgame perfect equilibrium, study the inefficiency incurred due to selfish
behavior, and also study problems that are particular to the dynamic setting,
like constraints on the order in which resources can be chosen or the problem
of finding a scheduler that achieves stability.
acknowledgement: This research was supported in part by the European Research Council
(ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science
Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In:
Vol 9928. Springer; 2016:153-166. doi:10.1007/978-3-662-53354-3_13'
apa: 'Avni, G., Henzinger, T. A., & Kupferman, O. (2016). Dynamic resource allocation
games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic
Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_13'
chicago: Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation
Games,” 9928:153–66. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_13.
ieee: 'G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation
games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool,
United Kingdom, 2016, vol. 9928, pp. 153–166.'
ista: 'Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games.
SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.'
mla: Avni, Guy, et al. Dynamic Resource Allocation Games. Vol. 9928, Springer,
2016, pp. 153–66, doi:10.1007/978-3-662-53354-3_13.
short: G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.
conference:
end_date: 2016-09-21
location: Liverpool, United Kingdom
name: 'SAGT: Symposium on Algorithmic Game Theory'
start_date: 2016-09-19
corr_author: '1'
date_created: 2018-12-11T11:51:28Z
date_published: 2016-09-01T00:00:00Z
date_updated: 2026-04-16T09:35:14Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-53354-3_13
ec_funded: 1
external_id:
isi:
- '000389020400013'
file:
- access_level: open_access
checksum: 0825eefd4e22774f6f62cb7d7389b05a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:22Z
date_updated: 2020-07-14T12:44:45Z
file_id: '5073'
file_name: IST-2016-645-v1+1_sagt-cr.pdf
file_size: 243458
relation: main_file
file_date_updated: 2020-07-14T12:44:45Z
has_accepted_license: '1'
intvolume: ' 9928'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Preprint
page: 153 - 166
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: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Springer
publist_id: '5926'
pubrep_id: '645'
quality_controlled: '1'
related_material:
record:
- id: '6761'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Dynamic resource allocation games
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9928
year: '2016'
...
---
_id: '1390'
abstract:
- lang: eng
text: "The goal of automatic program repair is to identify a set of syntactic changes
that can turn a program that is incorrect with respect\r\nto a given specification
into a correct one. Existing program repair techniques typically aim to find any
program that meets the given specification. Such “best-effort” strategies can
end up generating a program that is quite different from the original one. Novel
techniques have been proposed to compute syntactically minimal program fixes,
but the smallest syntactic fix to a program can still significantly alter the
original program’s behaviour. We propose a new approach to program repair based
on program distances, which can quantify changes not only to the program syntax
but also to the program semantics. We call this the quantitative program repair
problem where the “optimal” repair is derived using multiple distances. We implement
a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively
close), using the program synthesizer Sketch. We evaluate the effectiveness of
different distances in obtaining desirable repairs by evaluating\r\nQlose on programs
taken from educational tools such as CodeHunt and edX."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Loris
full_name: D'Antoni, Loris
last_name: D'Antoni
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
- first_name: Rishabh
full_name: Singh, Rishabh
last_name: Singh
citation:
ama: 'D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives.
In: Vol 9780. Springer; 2016:383-401. doi:10.1007/978-3-319-41540-6_21'
apa: 'D’Antoni, L., Samanta, R., & Singh, R. (2016). QLOSE: Program repair with
quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer
Aided Verification, Toronto, Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_21'
chicago: 'D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair
with Quantitative Objectives,” 9780:383–401. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_21.'
ieee: 'L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative
objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada,
2016, vol. 9780, pp. 383–401.'
ista: 'D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative
objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.'
mla: 'D’Antoni, Loris, et al. QLOSE: Program Repair with Quantitative Objectives.
Vol. 9780, Springer, 2016, pp. 383–401, doi:10.1007/978-3-319-41540-6_21.'
short: L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
corr_author: '1'
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2025-09-22T07:30:07Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_21
ec_funded: 1
external_id:
isi:
- '000387731400021'
intvolume: ' 9780'
isi: 1
language:
- iso: eng
month: '07'
oa_version: None
page: 383 - 401
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: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Springer
publist_id: '5819'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'QLOSE: Program repair with quantitative objectives'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9780
year: '2016'
...
---
_id: '1391'
abstract:
- lang: eng
text: "We present an extension to the quantifier-free theory of integer arrays which
allows us to express counting. The properties expressible in Array Folds Logic
(AFL) include statements such as "the first array cell contains the array
length," and "the array contains equally many minimal and maximal elements."
These properties cannot be expressed in quantified fragments of the theory of
arrays, nor in the theory of concatenation. Using reduction to counter machines,
we show that the satisfiability problem of AFL is PSPACE-complete, and with a
natural restriction the complexity decreases to NP. We also show that adding either
universal quantifiers or concatenation leads to undecidability.\r\nAFL contains
terms that fold a function over an array. We demonstrate that folding, a well-known
concept from functional languages, allows us to concisely summarize loops that
count over arrays, which occurs frequently in real-life programs. We provide a
tool that can discharge proof obligations in AFL, and we demonstrate on practical
examples that our decision procedure can solve a broad range of problems in symbolic
testing and program verification."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Andrey
full_name: Kupriyanov, Andrey
id: 2C311BF8-F248-11E8-B48F-1D18A9856A87
last_name: Kupriyanov
citation:
ama: 'Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer;
2016:230-248. doi:10.1007/978-3-319-41540-6_13'
apa: 'Daca, P., Henzinger, T. A., & Kupriyanov, A. (2016). Array folds logic
(Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto,
Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_13'
chicago: Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds
Logic,” 9780:230–48. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_13.
ieee: 'P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented
at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp.
230–248.'
ista: 'Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer
Aided Verification, LNCS, vol. 9780, 230–248.'
mla: Daca, Przemyslaw, et al. Array Folds Logic. Vol. 9780, Springer, 2016,
pp. 230–48, doi:10.1007/978-3-319-41540-6_13.
short: P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
corr_author: '1'
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_13
ec_funded: 1
external_id:
arxiv:
- '1603.06850'
isi:
- '000387731400013'
intvolume: ' 9780'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1603.06850
month: '07'
oa: 1
oa_version: Preprint
page: 230 - 248
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: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Springer
publist_id: '5818'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Array folds logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9780
year: '2016'
...
---
_id: '1421'
abstract:
- lang: eng
text: 'Hybridization methods enable the analysis of hybrid automata with complex,
nonlinear dynamics through a sound abstraction process. Complex dynamics are converted
to simpler ones with added noise, and then analysis is done using a reachability
method for the simpler dynamics. Several such recent approaches advocate that
only "dynamic" hybridization techniquesi.e., those where the dynamics
are abstracted on-The-fly during a reachability computation are effective. In
this paper, we demonstrate this is not the case, and create static hybridization
methods that are more scalable than earlier approaches. The main insight in our
approach is that quick, numeric simulations can be used to guide the process,
eliminating the need for an exponential number of hybridization domains. Transitions
between domains are generally timetriggered, avoiding accumulated error from geometric
intersections. We enhance our static technique by combining time-Triggered transitions
with occasional space-Triggered transitions, and demonstrate the benefits of the
combined approach in what we call mixed-Triggered hybridization. Finally, error
modes are inserted to confirm that the reachable states stay within the hybridized
regions. The developed techniques can scale to higher dimensions than previous
static approaches, while enabling the parallelization of the main performance
bottleneck for many dynamic hybridization approaches: The nonlinear optimization
required for sound dynamics abstraction. We implement our method as a model transformation
pass in the HYST tool, and perform reachability analysis and evaluation using
an unmodified version of SpaceEx on nonlinear models with up to six dimensions.'
article_processing_charge: No
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Pradyot
full_name: Prakash, Pradyot
last_name: Prakash
citation:
ama: 'Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization
methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:10.1145/2883817.2883837'
apa: 'Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., & Prakash, P. (2016).
Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164).
Presented at the HSCC: Hybrid Systems - Computation and Control, Vienna, Austria:
Springer. https://doi.org/10.1145/2883817.2883837'
chicago: Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, Taylor Johnson, and
Pradyot Prakash. “Scalable Static Hybridization Methods for Analysis of Nonlinear
Systems,” 155–64. Springer, 2016. https://doi.org/10.1145/2883817.2883837.
ieee: 'S. Bak, S. Bogomolov, T. A. Henzinger, T. Johnson, and P. Prakash, “Scalable
static hybridization methods for analysis of nonlinear systems,” presented at
the HSCC: Hybrid Systems - Computation and Control, Vienna, Austria, 2016, pp.
155–164.'
ista: 'Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static
hybridization methods for analysis of nonlinear systems. HSCC: Hybrid Systems
- Computation and Control, 155–164.'
mla: Bak, Stanley, et al. Scalable Static Hybridization Methods for Analysis
of Nonlinear Systems. Springer, 2016, pp. 155–64, doi:10.1145/2883817.2883837.
short: S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer,
2016, pp. 155–164.
conference:
end_date: 2016-04-14
location: Vienna, Austria
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2016-04-12
date_created: 2018-12-11T11:51:55Z
date_published: 2016-04-11T00:00:00Z
date_updated: 2025-09-18T14:21:28Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2883817.2883837
ec_funded: 1
external_id:
isi:
- '000390844400018'
isi: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 155 - 164
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: Formal methods for the design and analysis of complex systems
- _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: '5786'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Scalable static hybridization methods for analysis of nonlinear systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2016'
...
---
_id: '1439'
abstract:
- lang: eng
text: Fault-tolerant distributed algorithms play an important role in many critical/high-availability
applications. These algorithms are notoriously difficult to implement correctly,
due to asynchronous communication and the occurrence of faults, such as the network
dropping messages or computers crashing. We introduce PSYNC, a domain specific
language based on the Heard-Of model, which views asynchronous faulty systems
as synchronous ones with an adversarial environment that simulates asynchrony
and faults by dropping messages. We define a runtime system for PSYNC that efficiently
executes on asynchronous networks. We formalize the relation between the runtime
system and PSYNC in terms of observational refinement. The high-level lockstep
abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant
distributed algorithms and enables automated formal verification. We have implemented
an embedding of PSYNC in the SCALA programming language with a runtime system
for asynchronous networks. We show the applicability of PSYNC by implementing
several important fault-tolerant distributed algorithms and we compare the implementation
of consensus algorithms in PSYNC against implementations in other languages in
terms of code size, runtime efficiency, and verification.
acknowledgement: 'Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192
and FA8650-15-C-7564) and NSF (Grant CCF-1138967). '
alternative_title:
- ACM SIGPLAN Notices
article_processing_charge: No
author:
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- 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: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language
for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:10.1145/2837614.2837650'
apa: 'Dragoi, C., Henzinger, T. A., & Zufferey, D. (2016). PSYNC: A partially
synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp.
400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg,
FL, USA: ACM. https://doi.org/10.1145/2837614.2837650'
chicago: 'Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “PSYNC: A Partially
Synchronous Language for Fault-Tolerant Distributed Algorithms,” 20–22:400–415.
ACM, 2016. https://doi.org/10.1145/2837614.2837650.'
ieee: 'C. Dragoi, T. A. Henzinger, and D. Zufferey, “PSYNC: A partially synchronous
language for fault-tolerant distributed algorithms,” presented at the POPL: Principles
of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 400–415.'
ista: 'Dragoi C, Henzinger TA, Zufferey D. 2016. PSYNC: A partially synchronous
language for fault-tolerant distributed algorithms. POPL: Principles of Programming
Languages, ACM SIGPLAN Notices, vol. 20–22, 400–415.'
mla: 'Dragoi, Cezara, et al. PSYNC: A Partially Synchronous Language for Fault-Tolerant
Distributed Algorithms. Vol. 20–22, ACM, 2016, pp. 400–15, doi:10.1145/2837614.2837650.'
short: C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2025-09-18T11:44:23Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2837614.2837650
ec_funded: 1
external_id:
isi:
- '000374053600033'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://hal.inria.fr/hal-01251199/
month: '01'
oa: 1
oa_version: Preprint
page: 400 - 415
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: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: ACM
publist_id: '5759'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'PSYNC: A partially synchronous language for fault-tolerant distributed algorithms'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 20-22
year: '2016'
...
---
_id: '1524'
abstract:
- lang: eng
text: "When designing genetic circuits, the typical primitives used in major existing
modelling formalisms are gene interaction graphs, where edges between genes denote
either an activation or inhibition relation. However, when designing experiments,
it is important to be precise about the low-level mechanistic details as to how
each such relation is implemented. The rule-based modelling language Kappa allows
to unambiguously specify mechanistic details such as DNA binding sites, dimerisation
of transcription factors, or co-operative interactions. Such a detailed description
comes with complexity and computationally costly executions. We propose a general
method for automatically transforming a rule-based program, by eliminating intermediate
species and adjusting the rate constants accordingly. To the best of our knowledge,
we show the first automated reduction of rule-based models based on equilibrium
approximations.\r\nOur algorithm is an adaptation of an existing algorithm, which
was designed for reducing reaction-based programs; our version of the algorithm
scans the rule-based Kappa model in search for those interaction patterns known
to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional
checks are then performed in order to verify if the reduction is meaningful in
the context of the full model. The reduced model is efficiently obtained by static
inspection over the rule-set. The tool is tested on a detailed rule-based model
of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has
11 rules and 5 agents, and provides a dramatic reduction in simulation time of
several orders of magnitude."
acknowledgement: This research was supported by the People Programme (Marie Curie
Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under
REA grant agreement no. 291734, and the SNSF Early Postdoc.Mobility Fellowship,
the grant number P2EZP2_148797.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Andreea
full_name: Beica, Andreea
last_name: Beica
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Beica A, Guet CC, Petrov T. Efficient reduction of kappa models by static
inspection of the rule-set. In: Vol 9271. Springer; 2016:173-191. doi:10.1007/978-3-319-26916-0_10'
apa: 'Beica, A., Guet, C. C., & Petrov, T. (2016). Efficient reduction of kappa
models by static inspection of the rule-set (Vol. 9271, pp. 173–191). Presented
at the HSB: Hybrid Systems Biology, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-319-26916-0_10'
chicago: Beica, Andreea, Calin C Guet, and Tatjana Petrov. “Efficient Reduction
of Kappa Models by Static Inspection of the Rule-Set,” 9271:173–91. Springer,
2016. https://doi.org/10.1007/978-3-319-26916-0_10.
ieee: 'A. Beica, C. C. Guet, and T. Petrov, “Efficient reduction of kappa models
by static inspection of the rule-set,” presented at the HSB: Hybrid Systems Biology,
Madrid, Spain, 2016, vol. 9271, pp. 173–191.'
ista: 'Beica A, Guet CC, Petrov T. 2016. Efficient reduction of kappa models by
static inspection of the rule-set. HSB: Hybrid Systems Biology, LNCS, vol. 9271,
173–191.'
mla: Beica, Andreea, et al. Efficient Reduction of Kappa Models by Static Inspection
of the Rule-Set. Vol. 9271, Springer, 2016, pp. 173–91, doi:10.1007/978-3-319-26916-0_10.
short: A. Beica, C.C. Guet, T. Petrov, in:, Springer, 2016, pp. 173–191.
conference:
end_date: 2015-09-05
location: Madrid, Spain
name: 'HSB: Hybrid Systems Biology'
start_date: 2015-09-04
corr_author: '1'
date_created: 2018-12-11T11:52:31Z
date_published: 2016-01-10T00:00:00Z
date_updated: 2025-06-04T12:06:27Z
day: '10'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-319-26916-0_10
ec_funded: 1
external_id:
arxiv:
- '1501.00440'
intvolume: ' 9271'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1501.00440
month: '01'
oa: 1
oa_version: Preprint
page: 173 - 191
project:
- _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: '5649'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient reduction of kappa models by static inspection of the rule-set
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9271
year: '2016'
...
---
_id: '1526'
abstract:
- lang: eng
text: 'We present the first study of robustness of systems that are both timed as
well as reactive (I/O). We study the behavior of such timed I/O systems in the
presence of uncertain inputs and formalize their robustness using the analytic
notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if
the perturbation in its output is at most K times the perturbation in its input.
We quantify input and output perturbation using similarity functions over timed
words such as the timed version of the Manhattan distance and the Skorokhod distance.
We consider two models of timed I/O systems — timed transducers and asynchronous
sequential circuits. We show that K-robustness of timed transducers can be decided
in polynomial space under certain conditions. For asynchronous sequential circuits,
we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete
letter-to-letter transducers and show PSpace-completeness of the problem.'
acknowledgement: This research was supported in part 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 National Science
Centre (NCN), Poland under grant 2014/15/D/ST6/04543.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
citation:
ama: 'Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems.
In: Vol 9583. Springer; 2016:250-267. doi:10.1007/978-3-662-49122-5_12'
apa: 'Henzinger, T. A., Otop, J., & Samanta, R. (2016). Lipschitz robustness
of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification,
Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer.
https://doi.org/10.1007/978-3-662-49122-5_12'
chicago: Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness
of Timed I/O Systems,” 9583:250–67. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_12.
ieee: 'T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed
I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract
Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267.'
ista: 'Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O
systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS,
vol. 9583, 250–267.'
mla: Henzinger, Thomas A., et al. Lipschitz Robustness of Timed I/O Systems.
Vol. 9583, Springer, 2016, pp. 250–67, doi:10.1007/978-3-662-49122-5_12.
short: T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.
conference:
end_date: 2016-01-19
location: St. Petersburg, FL, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2016-01-17
corr_author: '1'
date_created: 2018-12-11T11:52:32Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2025-09-18T11:06:25Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_12
ec_funded: 1
external_id:
arxiv:
- '1506.01233'
isi:
- '000375148800012'
intvolume: ' 9583'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1506.01233
month: '01'
oa: 1
oa_version: Preprint
page: 250 - 267
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: Formal methods for the design and analysis of complex systems
- _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: '5647'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lipschitz robustness of timed I/O systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9583
year: '2016'
...
---
_id: '1705'
abstract:
- lang: eng
text: Hybrid systems represent an important and powerful formalism for modeling
real-world applications such as embedded systems. A verification tool like SpaceEx
is based on the exploration of a symbolic search space (the region space). As
a verification tool, it is typically optimized towards proving the absence of
errors. In some settings, e.g., when the verification tool is employed in a feedback-directed
design cycle, one would like to have the option to call a version that is optimized
towards finding an error trajectory in the region space. A recent approach in
this direction is based on guided search. Guided search relies on a cost function
that indicates which states are promising to be explored, and preferably explores
more promising states first. In this paper, we propose an abstraction-based cost
function based on coarse-grained space abstractions for guiding the reachability
analysis. For this purpose, a suitable abstraction technique that exploits the
flexible granularity of modern reachability analysis algorithms is introduced.
The new cost function is an effective extension of pattern database approaches
that have been successfully applied in other areas. The approach has been implemented
in the SpaceEx model checker. The evaluation shows its practical potential.
article_processing_charge: Yes (via OA deal)
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Alexandre
full_name: Donzé, Alexandre
last_name: Donzé
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Hamed
full_name: Ladan, Hamed
last_name: Ladan
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Martin
full_name: Wehrle, Martin
last_name: Wehrle
citation:
ama: Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based
on coarse-grained space abstractions. International Journal on Software Tools
for Technology Transfer. 2016;18(4):449-467. doi:10.1007/s10009-015-0393-y
apa: Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H., …
Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space
abstractions. International Journal on Software Tools for Technology Transfer.
Springer. https://doi.org/10.1007/s10009-015-0393-y
chicago: Bogomolov, Sergiy, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor Johnson,
Hamed Ladan, Andreas Podelski, and Martin Wehrle. “Guided Search for Hybrid Systems
Based on Coarse-Grained Space Abstractions.” International Journal on Software
Tools for Technology Transfer. Springer, 2016. https://doi.org/10.1007/s10009-015-0393-y.
ieee: S. Bogomolov et al., “Guided search for hybrid systems based on coarse-grained
space abstractions,” International Journal on Software Tools for Technology
Transfer, vol. 18, no. 4. Springer, pp. 449–467, 2016.
ista: Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle
M. 2016. Guided search for hybrid systems based on coarse-grained space abstractions.
International Journal on Software Tools for Technology Transfer. 18(4), 449–467.
mla: Bogomolov, Sergiy, et al. “Guided Search for Hybrid Systems Based on Coarse-Grained
Space Abstractions.” International Journal on Software Tools for Technology
Transfer, vol. 18, no. 4, Springer, 2016, pp. 449–67, doi:10.1007/s10009-015-0393-y.
short: S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. Johnson, H. Ladan, A. Podelski,
M. Wehrle, International Journal on Software Tools for Technology Transfer 18
(2016) 449–467.
corr_author: '1'
date_created: 2018-12-11T11:53:34Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2025-09-18T10:50:19Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10009-015-0393-y
ec_funded: 1
external_id:
isi:
- '000379708300007'
file:
- access_level: open_access
checksum: 31561d7705599a9bd4ea816accc0752e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:26Z
date_updated: 2020-07-14T12:45:13Z
file_id: '5146'
file_name: IST-2016-457-v1+1_s10009-015-0393-y.pdf
file_size: 2296522
relation: main_file
file_date_updated: 2020-07-14T12:45:13Z
has_accepted_license: '1'
intvolume: ' 18'
isi: 1
issue: '4'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: 449 - 467
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: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '5431'
pubrep_id: '457'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Guided search for hybrid systems based on coarse-grained space abstractions
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 18
year: '2016'
...
---
_id: '479'
abstract:
- lang: eng
text: Clinical guidelines and decision support systems (DSS) play an important role
in daily practices of medicine. Many text-based guidelines have been encoded for
work-flow simulation of DSS to automate health care. During the collaboration
with Carle hospital to develop a DSS, we identify that, for some complex and life-critical
diseases, it is highly desirable to automatically rigorously verify some complex
temporal properties in guidelines, which brings new challenges to current simulation
based DSS with limited support of automatical formal verification and real-time
data analysis. In this paper, we conduct the first study on applying runtime verification
to cooperate with current DSS based on real-time data. Within the proposed technique,
a user-friendly domain specific language, named DRTV, is designed to specify vital
real-time data sampled by medical devices and temporal properties originated from
clinical guidelines. Some interfaces are developed for data acquisition and communication.
Then, for medical practice scenarios described in DRTV model, we will automatically
generate event sequences and runtime property verifier automata. If a temporal
property violates, real-time warnings will be produced by the formal verifier
and passed to medical DSS. We have used DRTV to specify different kinds of medical
care scenarios, and applied the proposed technique to assist existing DSS. As
presented in experiment results, in terms of warning detection, it outperforms
the only use of DSS or human inspection, and improves the quality of clinical
health care of hospital
acknowledgement: "This work is supported by NSF CNS 13-30077, NSF CNS 13-29886, NSF
CNS 15-45002, and NSFC 61303014.\r\nThe authors thank Dr. Bobby and Dr. Hill at
Carle Hospital, Urbana, IL for their help with the discussion on medical knowledge.\r\n\r\n"
alternative_title:
- Proceedings International Conference on Software Engineering
article_processing_charge: No
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Rui
full_name: Wang, Rui
last_name: Wang
- first_name: Mohamad
full_name: Hosseini, Mohamad
last_name: Hosseini
- first_name: Jiaguang
full_name: Sun, Jiaguang
last_name: Sun
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
citation:
ama: 'Jiang Y, Liu H, Kong H, et al. Use runtime verification to improve the quality
of medical care practice. In: Proceedings of the 38th International Conference
on Software Engineering Companion . IEEE; 2016:112-121. doi:10.1145/2889160.2889233'
apa: 'Jiang, Y., Liu, H., Kong, H., Wang, R., Hosseini, M., Sun, J., & Sha,
L. (2016). Use runtime verification to improve the quality of medical care practice.
In Proceedings of the 38th International Conference on Software Engineering
Companion (pp. 112–121). Austin, TX, USA: IEEE. https://doi.org/10.1145/2889160.2889233'
chicago: Jiang, Yu, Han Liu, Hui Kong, Rui Wang, Mohamad Hosseini, Jiaguang Sun,
and Lui Sha. “Use Runtime Verification to Improve the Quality of Medical Care
Practice.” In Proceedings of the 38th International Conference on Software
Engineering Companion , 112–21. IEEE, 2016. https://doi.org/10.1145/2889160.2889233.
ieee: Y. Jiang et al., “Use runtime verification to improve the quality of
medical care practice,” in Proceedings of the 38th International Conference
on Software Engineering Companion , Austin, TX, USA, 2016, pp. 112–121.
ista: 'Jiang Y, Liu H, Kong H, Wang R, Hosseini M, Sun J, Sha L. 2016. Use runtime
verification to improve the quality of medical care practice. Proceedings of the
38th International Conference on Software Engineering Companion . ICSE: International
Conference on Software Engineering, Proceedings International Conference on Software
Engineering, , 112–121.'
mla: Jiang, Yu, et al. “Use Runtime Verification to Improve the Quality of Medical
Care Practice.” Proceedings of the 38th International Conference on Software
Engineering Companion , IEEE, 2016, pp. 112–21, doi:10.1145/2889160.2889233.
short: Y. Jiang, H. Liu, H. Kong, R. Wang, M. Hosseini, J. Sun, L. Sha, in:, Proceedings
of the 38th International Conference on Software Engineering Companion , IEEE,
2016, pp. 112–121.
conference:
end_date: 2016-05-22
location: Austin, TX, USA
name: 'ICSE: International Conference on Software Engineering'
start_date: 2016-05-14
date_created: 2018-12-11T11:46:42Z
date_published: 2016-05-14T00:00:00Z
date_updated: 2025-09-22T14:22:48Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2889160.2889233
external_id:
isi:
- '000402155300016'
isi: 1
language:
- iso: eng
month: '05'
oa_version: None
page: 112 - 121
publication: 'Proceedings of the 38th International Conference on Software Engineering
Companion '
publication_status: published
publisher: IEEE
publist_id: '7341'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Use runtime verification to improve the quality of medical care practice
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2016'
...
---
_id: '1498'
abstract:
- lang: eng
text: Fault-tolerant distributed algorithms play an important role in many critical/high-availability
applications. These algorithms are notoriously difficult to implement correctly,
due to asynchronous communication and the occurrence of faults, such as the network
dropping messages or computers crashing. Nonetheless there is surprisingly little
language and verification support to build distributed systems based on fault-tolerant
algorithms. In this paper, we present some of the challenges that a designer has
to overcome to implement a fault-tolerant distributed system. Then we review different
models that have been proposed to reason about distributed algorithms and sketch
how such a model can form the basis for a domain-specific programming language.
Adopting a high-level programming model can simplify the programmer's life and
make the code amenable to automated verification, while still compiling to efficiently
executable code. We conclude by summarizing the current status of an ongoing language
design and implementation project that is based on this idea.
alternative_title:
- LIPIcs
author:
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- 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: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant
distributed systems. 2015;32:90-102. doi:10.4230/LIPIcs.SNAPL.2015.90
apa: 'Dragoi, C., Henzinger, T. A., & Zufferey, D. (2015). The need for language
support for fault-tolerant distributed systems. Presented at the SNAPL: Summit
oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90'
chicago: Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for
Language Support for Fault-Tolerant Distributed Systems.” Leibniz International
Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2015. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90.
ieee: C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support
for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, pp. 90–102, 2015.
ista: Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for
fault-tolerant distributed systems. 32, 90–102.
mla: Dragoi, Cezara, et al. The Need for Language Support for Fault-Tolerant
Distributed Systems. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2015, pp. 90–102, doi:10.4230/LIPIcs.SNAPL.2015.90.
short: C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.
conference:
end_date: 2015-05-06
location: Asilomar, CA, United States
name: 'SNAPL: Summit oN Advances in Programming Languages'
start_date: 2015-05-03
corr_author: '1'
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2025-04-15T06:26:02Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.SNAPL.2015.90
ec_funded: 1
file:
- access_level: open_access
checksum: cf5e94baa89a2dc4c5de01abc676eda8
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:02Z
date_updated: 2020-07-14T12:44:58Z
file_id: '5050'
file_name: IST-2016-499-v1+1_9.pdf
file_size: 489362
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 32'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 90 - 102
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication_identifier:
isbn:
- '978-3-939897-80-4 '
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5681'
pubrep_id: '499'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: The need for language support for fault-tolerant distributed systems
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 32
year: '2015'
...
---
_id: '1499'
abstract:
- lang: eng
text: "We consider weighted automata with both positive and negative integer weights
on edges and\r\nstudy the problem of synchronization using adaptive strategies
that may only observe whether\r\nthe current weight-level is negative or nonnegative.
We show that the synchronization problem is decidable in polynomial time for deterministic
weighted automata."
acknowledgement: "The research leading to these results has received funding from
the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement
601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center
IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM),
the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award), the Czech Science Foundation under grant agreement P202/12/G061, and People
Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme
(FP7/2007-2013) REA Grant No 291734."
alternative_title:
- LIPIcs
author:
- 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: Simon
full_name: Laursen, Simon
last_name: Laursen
- first_name: Jiří
full_name: Srba, Jiří
last_name: Srba
citation:
ama: 'Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of
weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142'
apa: 'Kretinsky, J., Larsen, K., Laursen, S., & Srba, J. (2015). Polynomial
time decidability of weighted synchronization under partial observability (Vol.
42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142'
chicago: Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time
Decidability of Weighted Synchronization under Partial Observability,” 42:142–54.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.
ieee: 'J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability
of weighted synchronization under partial observability,” presented at the CONCUR:
Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.'
ista: 'Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability
of weighted synchronization under partial observability. CONCUR: Concurrency Theory,
LIPIcs, vol. 42, 142–154.'
mla: Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization
under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
short: J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2015, pp. 142–154.
conference:
end_date: 2015-09-04
location: Madrid, Spain
name: 'CONCUR: Concurrency Theory'
start_date: 2015-09-01
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2025-04-15T06:26:02Z
day: '01'
ddc:
- '000'
- '003'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2015.142
ec_funded: 1
file:
- access_level: open_access
checksum: 49eb5021caafaabe5356c65b9c5f8c9c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:12Z
date_updated: 2020-07-14T12:44:58Z
file_id: '4672'
file_name: IST-2016-498-v1+1_32.pdf
file_size: 623563
relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: ' 42'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 142 - 154
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: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5680'
pubrep_id: '498'
quality_controlled: '1'
scopus_import: 1
status: public
title: Polynomial time decidability of weighted synchronization under partial observability
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 42
year: '2015'
...
---
_id: '1501'
abstract:
- lang: eng
text: 'We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems. We focus on qualitative properties for MDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability. We introduce a new simulation relation to capture
the refinement relation of MDPs with respect to qualitative properties, and present
discrete graph algorithms with quadratic complexity to compute the simulation
relation. We present an automated technique for assume-guarantee style reasoning
for compositional analysis of two-player games by giving a counterexample guided
abstraction-refinement approach to compute our new simulation relation. We show
a tight link between two-player games and MDPs, and as a consequence the results
for games are lifted to MDPs with qualitative properties. We have implemented
our algorithms and show that the compositional analysis leads to significant improvements. '
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE),
and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games),
Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive
Modeling).'
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative
properties in Markov decision processes. Formal Methods in System Design.
2015;47(2):230-264. doi:10.1007/s10703-015-0235-2
apa: Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional
analysis of qualitative properties in Markov decision processes. Formal Methods
in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
Compositional Analysis of Qualitative Properties in Markov Decision Processes.”
Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2.
ieee: K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis
of qualitative properties in Markov decision processes,” Formal Methods in
System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015.
ista: Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of
qualitative properties in Markov decision processes. Formal Methods in System
Design. 47(2), 230–264.
mla: Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative
Properties in Markov Decision Processes.” Formal Methods in System Design,
vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2.
short: K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015)
230–264.
corr_author: '1'
date_created: 2018-12-11T11:52:23Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-015-0235-2
ec_funded: 1
external_id:
arxiv:
- '1405.0835'
isi:
- '000361752300003'
intvolume: ' 47'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1405.0835
month: '10'
oa: 1
oa_version: Preprint
page: 230 - 264
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _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: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '5677'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: CEGAR for compositional analysis of qualitative properties in Markov decision
processes
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 47
year: '2015'
...
---
_id: '1502'
abstract:
- lang: eng
text: We extend the theory of input-output conformance with operators for merge
and quotient. The former is useful when testing against multiple requirements
or views. The latter can be used to generate tests for patches of an already tested
system. Both operators can combine systems with different action alphabets, which
is usually the case when constructing complex systems and specifications from
parts, for instance different views as well as newly defined functionality of
a~previous version of the system.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF)
projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme
(Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013)
under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373
(nSafeCer). Jan Křetínský has been partially supported by the Czech Science Foundation,
grant No. P202/12/G061. Nikola Beneš has been supported by the\r\nMEYS project
No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for
Scientific Excellence."
alternative_title:
- 'Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering '
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Dejan
full_name: Nickovic, Dejan
last_name: Nickovic
citation:
ama: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition
operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175'
apa: 'Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & Nickovic, D. (2015).
Complete composition operators for IOCO-testing theory (pp. 101–110). Presented
at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM.
https://doi.org/10.1145/2737166.2737175'
chicago: Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and
Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10.
ACM, 2015. https://doi.org/10.1145/2737166.2737175.
ieee: 'N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete
composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based
Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.'
ista: 'Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition
operators for IOCO-testing theory. CBSE: Component-Based Software Engineering
, Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based
Software Engineering , , 101–110.'
mla: Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory.
ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.
short: N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015,
pp. 101–110.
conference:
end_date: 2015-05-08
location: Montreal, QC, Canada
name: 'CBSE: Component-Based Software Engineering '
start_date: 2015-05-04
date_created: 2018-12-11T11:52:24Z
date_published: 2015-05-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2737166.2737175
ec_funded: 1
external_id:
isi:
- '000380554800013'
file:
- access_level: open_access
checksum: c6ce681035c163a158751f240cb7d389
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:46Z
date_updated: 2020-07-14T12:44:59Z
file_id: '5303'
file_name: IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf
file_size: 467561
relation: main_file
file_date_updated: 2020-07-14T12:44:59Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 101 - 110
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: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_identifier:
isbn:
- 978-1-4503-3471-6
publication_status: published
publisher: ACM
publist_id: '5676'
pubrep_id: '625'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Complete composition operators for IOCO-testing theory
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2015'
...
---
_id: '1538'
abstract:
- lang: eng
text: Systems biology rests on the idea that biological complexity can be better
unraveled through the interplay of modeling and experimentation. However, the
success of this approach depends critically on the informativeness of the chosen
experiments, which is usually unknown a priori. Here, we propose a systematic
scheme based on iterations of optimal experiment design, flow cytometry experiments,
and Bayesian parameter inference to guide the discovery process in the case of
stochastic biochemical reaction networks. To illustrate the benefit of our methodology,
we apply it to the characterization of an engineered light-inducible gene expression
circuit in yeast and compare the performance of the resulting model with models
identified from nonoptimal experiments. In particular, we compare the parameter
posterior distributions and the precision to which the outcome of future experiments
can be predicted. Moreover, we illustrate how the identified stochastic model
can be used to determine light induction patterns that make either the average
amount of protein or the variability in a population of cells follow a desired
profile. Our results show that optimal experiment design allows one to derive
models that are accurate enough to precisely predict and regulate the protein
expression in heterogeneous cell populations over extended periods of time.
acknowledgement: 'J.R., F.P., and J.L. acknowledge support from the European Commission
under the Network of Excellence HYCON2 (highly-complex and networked control systems)
and SystemsX.ch under the SignalX Project. J.R. acknowledges support from the People
Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme
FP7/2007-2013 under REA (Research Executive Agency) Grant 291734. M.K. acknowledges
support from Human Frontier Science Program Grant RP0061/2011 (www.hfsp.org). '
article_processing_charge: No
author:
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
- first_name: Francesca
full_name: Parise, Francesca
last_name: Parise
- first_name: Andreas
full_name: Milias Argeitis, Andreas
last_name: Milias Argeitis
- first_name: Mustafa
full_name: Khammash, Mustafa
last_name: Khammash
- first_name: John
full_name: Lygeros, John
last_name: Lygeros
citation:
ama: Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. Iterative experiment
design guides the characterization of a light-inducible gene expression circuit.
PNAS. 2015;112(26):8148-8153. doi:10.1073/pnas.1423947112
apa: Ruess, J., Parise, F., Milias Argeitis, A., Khammash, M., & Lygeros, J.
(2015). Iterative experiment design guides the characterization of a light-inducible
gene expression circuit. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.1423947112
chicago: Ruess, Jakob, Francesca Parise, Andreas Milias Argeitis, Mustafa Khammash,
and John Lygeros. “Iterative Experiment Design Guides the Characterization of
a Light-Inducible Gene Expression Circuit.” PNAS. National Academy of Sciences,
2015. https://doi.org/10.1073/pnas.1423947112.
ieee: J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, and J. Lygeros, “Iterative
experiment design guides the characterization of a light-inducible gene expression
circuit,” PNAS, vol. 112, no. 26. National Academy of Sciences, pp. 8148–8153,
2015.
ista: Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. 2015. Iterative
experiment design guides the characterization of a light-inducible gene expression
circuit. PNAS. 112(26), 8148–8153.
mla: Ruess, Jakob, et al. “Iterative Experiment Design Guides the Characterization
of a Light-Inducible Gene Expression Circuit.” PNAS, vol. 112, no. 26,
National Academy of Sciences, 2015, pp. 8148–53, doi:10.1073/pnas.1423947112.
short: J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, J. Lygeros, PNAS 112
(2015) 8148–8153.
date_created: 2018-12-11T11:52:36Z
date_published: 2015-06-30T00:00:00Z
date_updated: 2025-09-23T09:24:24Z
day: '30'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1073/pnas.1423947112
ec_funded: 1
external_id:
isi:
- '000357079400070'
pmid:
- '26085136'
intvolume: ' 112'
isi: 1
issue: '26'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4491780/
month: '06'
oa: 1
oa_version: Submitted Version
page: 8148 - 8153
pmid: 1
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: PNAS
publication_status: published
publisher: National Academy of Sciences
publist_id: '5633'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Iterative experiment design guides the characterization of a light-inducible
gene expression circuit
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 112
year: '2015'
...
---
_id: '1539'
abstract:
- lang: eng
text: 'Many stochastic models of biochemical reaction networks contain some chemical
species for which the number of molecules that are present in the system can only
be finite (for instance due to conservation laws), but also other species that
can be present in arbitrarily large amounts. The prime example of such networks
are models of gene expression, which typically contain a small and finite number
of possible states for the promoter but an infinite number of possible states
for the amount of mRNA and protein. One of the main approaches to analyze such
models is through the use of equations for the time evolution of moments of the
chemical species. Recently, a new approach based on conditional moments of the
species with infinite state space given all the different possible states of the
finite species has been proposed. It was argued that this approach allows one
to capture more details about the full underlying probability distribution with
a smaller number of equations. Here, I show that the result that less moments
provide more information can only stem from an unnecessarily complicated description
of the system in the classical formulation. The foundation of this argument will
be the derivation of moment equations that describe the complete probability distribution
over the finite state space but only low-order moments over the infinite state
space. I will show that the number of equations that is needed is always less
than what was previously claimed and always less than the number of conditional
moment equations up to the same order. To support these arguments, a symbolic
algorithm is provided that can be used to derive minimal systems of unconditional
moment equations for models with partially finite state space. '
article_number: '244103'
article_processing_charge: No
author:
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
citation:
ama: Ruess J. Minimal moment equations for stochastic models of biochemical reaction
networks with partially finite state space. Journal of Chemical Physics.
2015;143(24). doi:10.1063/1.4937937
apa: Ruess, J. (2015). Minimal moment equations for stochastic models of biochemical
reaction networks with partially finite state space. Journal of Chemical Physics.
American Institute of Physics. https://doi.org/10.1063/1.4937937
chicago: Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical
Reaction Networks with Partially Finite State Space.” Journal of Chemical Physics.
American Institute of Physics, 2015. https://doi.org/10.1063/1.4937937.
ieee: J. Ruess, “Minimal moment equations for stochastic models of biochemical reaction
networks with partially finite state space,” Journal of Chemical Physics,
vol. 143, no. 24. American Institute of Physics, 2015.
ista: Ruess J. 2015. Minimal moment equations for stochastic models of biochemical
reaction networks with partially finite state space. Journal of Chemical Physics.
143(24), 244103.
mla: Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical
Reaction Networks with Partially Finite State Space.” Journal of Chemical Physics,
vol. 143, no. 24, 244103, American Institute of Physics, 2015, doi:10.1063/1.4937937.
short: J. Ruess, Journal of Chemical Physics 143 (2015).
corr_author: '1'
date_created: 2018-12-11T11:52:36Z
date_published: 2015-12-22T00:00:00Z
date_updated: 2025-09-23T09:34:48Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1063/1.4937937
ec_funded: 1
external_id:
isi:
- '000370412900068'
file:
- access_level: open_access
checksum: 838657118ae286463a2b7737319f35ce
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:43Z
date_updated: 2020-07-14T12:45:01Z
file_id: '4641'
file_name: IST-2016-593-v1+1_Minimal_moment_equations.pdf
file_size: 605355
relation: main_file
file_date_updated: 2020-07-14T12:45:01Z
has_accepted_license: '1'
intvolume: ' 143'
isi: 1
issue: '24'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
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: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Journal of Chemical Physics
publication_status: published
publisher: American Institute of Physics
publist_id: '5632'
pubrep_id: '593'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Minimal moment equations for stochastic models of biochemical reaction networks
with partially finite state space
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 143
year: '2015'
...