---
_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
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
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_13
ec_funded: 1
intvolume: ' 9780'
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: The Wittgenstein Prize
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
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.'
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 2016: International Conference on 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 2016: International Conference on 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 2016: International
Conference on 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 2016: International Conference on 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: 2021-01-12T06:50:37Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2883817.2883837
ec_funded: 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: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5786'
quality_controlled: '1'
scopus_import: 1
status: public
title: Scalable static hybridization methods for analysis of nonlinear systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
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
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: 2021-01-12T06:50:45Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2837614.2837650
ec_funded: 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: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: 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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1090'
abstract:
- lang: eng
text: ' While weighted automata provide a natural framework to express quantitative
properties, many basic properties like average response time cannot be expressed
with weighted automata. Nested weighted automata extend weighted automata and
consist of a master automaton and a set of slave automata that are invoked by
the master automaton. Nested weighted automata are strictly more expressive than
weighted automata (e.g., average response time can be expressed with nested weighted
automata), but the basic decision questions have higher complexity (e.g., for
deterministic automata, the emptiness question for nested weighted automata is
PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME).
We consider a natural subclass of nested weighted automata where at any point
at most a bounded number k of slave automata can be active. We focus on automata
whose master value function is the limit average. We show that these nested weighted
automata with bounded width are strictly more expressive than weighted automata
(e.g., average response time with no overlapping requests can be expressed with
bound k=1, but not with non-nested weighted automata). We show that the complexity
of the basic decision problems (i.e., emptiness and universality) for the subclass
with k constant matches the complexity for weighted automata. Moreover, when k
is part of the input given in unary we establish PSPACE-completeness.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award),
ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF)
through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under
grant 2014/15/D/ST6/04543."
alternative_title:
- LIPIcs
article_number: '24'
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. Nested weighted limit-average automata
of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2016. doi:10.4230/LIPIcs.MFCS.2016.24'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Nested weighted limit-average
automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations
of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.24'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.24.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average
automata of bounded width,” presented at the MFCS: Mathematical Foundations of
Computer Science (SG), Krakow; Poland, 2016, vol. 58.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata
of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs,
vol. 58, 24.'
mla: Chatterjee, Krishnendu, et al. Nested Weighted Limit-Average Automata of
Bounded Width. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016, doi:10.4230/LIPIcs.MFCS.2016.24.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Krakow; Poland
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2016-08-22
date_created: 2018-12-11T11:50:05Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:12Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2016.24
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:31Z
date_updated: 2018-12-12T10:17:31Z
file_id: '5286'
file_name: IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf
file_size: 564560
relation: main_file
file_date_updated: 2018-12-12T10:17:31Z
has_accepted_license: '1'
intvolume: ' 58'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6286'
pubrep_id: '795'
quality_controlled: '1'
scopus_import: 1
status: public
title: Nested weighted limit-average automata of bounded width
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2016'
...
---
_id: '1093'
abstract:
- lang: eng
text: 'We introduce a general class of distances (metrics) between Markov chains,
which are based on linear behaviour. This class encompasses distances given topologically
(such as the total variation distance or trace distance) as well as by temporal
logics or automata. We investigate which of the distances can be approximated
by observing the systems, i.e. by black-box testing or simulation, and we provide
both negative and positive results. '
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF)
under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award),
by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced
Postdoc. Mobility Fellowship – grant number P300P2_161067."
alternative_title:
- LIPIcs
article_number: '20'
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. Linear distances between Markov
chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear
distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency
Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2016.20'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances
between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City;
Canada, 2016, vol. 59.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between
Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.'
mla: Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol.
59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City; Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
- _id: CaGu
doi: 10.4230/LIPIcs.CONCUR.2016.20
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:39Z
date_updated: 2018-12-12T10:11:39Z
file_id: '4895'
file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf
file_size: 501827
relation: main_file
file_date_updated: 2018-12-12T10:11:39Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
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: The Wittgenstein Prize
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6283'
pubrep_id: '794'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Linear distances between Markov chains
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1095'
abstract:
- lang: eng
text: ' The semantics of concurrent data structures is usually given by a sequential
specification and a consistency condition. Linearizability is the most popular
consistency condition due to its simplicity and general applicability. Nevertheless,
for applications that do not require all guarantees offered by linearizability,
recent research has focused on improving performance and scalability of concurrent
data structures by relaxing their semantics. In this paper, we present local linearizability,
a relaxed consistency condition that is applicable to container-type concurrent
data structures like pools, queues, and stacks. While linearizability requires
that the effect of each operation is observed by all threads at the same time,
local linearizability only requires that for each thread T, the effects of its
local insertion operations and the effects of those removal operations that remove
values inserted by T are observed by all threads at the same time. We investigate
theoretical and practical properties of local linearizability and its relationship
to many existing consistency conditions. We present a generic implementation method
for locally linearizable data structures that uses existing linearizable data
structures as building blocks. Our implementations show performance and scalability
improvements over the original building blocks and outperform the fastest existing
container-type implementations. '
acknowledgement: "This work has been supported by the National Research Network RiSE
on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23,
S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship
(Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1,
the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European
Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award)."
alternative_title:
- LIPIcs
article_number: '6'
author:
- first_name: Andreas
full_name: Haas, Andreas
last_name: Haas
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Andreas
full_name: Holzer, Andreas
last_name: Holzer
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Michael
full_name: Lippautz, Michael
last_name: Lippautz
- first_name: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- first_name: Ana
full_name: Sokolova, Ana
last_name: Sokolova
- first_name: Helmut
full_name: Veith, Helmut
last_name: Veith
citation:
ama: 'Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent
container-type data structures. In: Leibniz International Proceedings in Informatics.
Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.6'
apa: 'Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H.,
… Veith, H. (2016). Local linearizability for concurrent container-type data structures.
In Leibniz International Proceedings in Informatics (Vol. 59). Quebec City;
Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6'
chicago: Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael
Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability
for Concurrent Container-Type Data Structures.” In Leibniz International Proceedings
in Informatics, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6.
ieee: A. Haas et al., “Local linearizability for concurrent container-type
data structures,” in Leibniz International Proceedings in Informatics,
Quebec City; Canada, 2016, vol. 59.
ista: 'Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A,
Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type
data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency
Theory, LIPIcs, vol. 59, 6.'
mla: Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type
Data Structures.” Leibniz International Proceedings in Informatics, vol.
59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.6.
short: A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A.
Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City; Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:50:07Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:14Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2016.6
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:10Z
date_updated: 2018-12-12T10:10:10Z
file_id: '4795'
file_name: IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf
file_size: 589747
relation: main_file
file_date_updated: 2018-12-12T10:10:10Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Leibniz International Proceedings in Informatics
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6280'
pubrep_id: '793'
quality_controlled: '1'
scopus_import: 1
status: public
title: Local linearizability for concurrent container-type data structures
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1103'
abstract:
- lang: eng
text: We propose two parallel state-space-exploration algorithms for hybrid automaton
(HA), with the goal of enhancing performance on multi-core shared-memory systems.
The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN
model checker, when traversing the discrete modes of the HA, and enhances it with
a parallel exploration of the continuous states within each mode. We show that
this simple-minded extension of PBFS does not provide the desired load balancing
in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS),
which uses a cheap precomputation of the cost associated with the post operations
(both continuous and discrete) in order to improve load balancing. We illustrate
the TP-BFS and the cost precomputation of the post operators on a support-function-based
algorithm for state-space exploration. The performance comparison of the two algorithms
shows that, in general, TP-BFS provides a better utilization/load-balancing of
the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments
show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect
to SpaceEx LGG scenario. In order to make the comparison fair, we employed an
equal number of post operations in both tools. To the best of our knowledge, this
paper represents the first attempt to provide parallel, reachability-analysis
algorithms for HA.
acknowledgement: This work was supported in part by DST-SERB, GoI under Project No.
YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM)
and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23
(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
article_number: '7797741'
author:
- first_name: Amit
full_name: Gurung, Amit
last_name: Gurung
- first_name: Arup
full_name: Deka, Arup
last_name: Deka
- 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: Rajarshi
full_name: Ray, Rajarshi
last_name: Ray
citation:
ama: 'Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability
analysis for hybrid systems. In: IEEE; 2016. doi:10.1109/MEMCOD.2016.7797741'
apa: 'Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., & Ray, R.
(2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE:
International Conference on Formal Methods and Models for System Design, Kanpur,
India : IEEE. https://doi.org/10.1109/MEMCOD.2016.7797741'
chicago: Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and
Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016.
https://doi.org/10.1109/MEMCOD.2016.7797741.
ieee: 'A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel
reachability analysis for hybrid systems,” presented at the MEMOCODE: International
Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.'
ista: 'Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel
reachability analysis for hybrid systems. MEMOCODE: International Conference on
Formal Methods and Models for System Design, 7797741.'
mla: Gurung, Amit, et al. Parallel Reachability Analysis for Hybrid Systems.
7797741, IEEE, 2016, doi:10.1109/MEMCOD.2016.7797741.
short: A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE,
2016.
conference:
end_date: 2016-11-20
location: 'Kanpur, India '
name: 'MEMOCODE: International Conference on Formal Methods and Models for System
Design'
start_date: 2016-11-18
date_created: 2018-12-11T11:50:09Z
date_published: 2016-12-27T00:00:00Z
date_updated: 2021-01-12T06:48:18Z
day: '27'
department:
- _id: ToHe
doi: 10.1109/MEMCOD.2016.7797741
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1606.05473
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: IEEE
publist_id: '6272'
quality_controlled: '1'
scopus_import: 1
status: public
title: Parallel reachability analysis for hybrid systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1130'
abstract:
- lang: eng
text: "In this thesis we present a computer-aided programming approach to concurrency.
Our approach helps the programmer by automatically fixing concurrency-related
bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive
scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are
program behaviours that are incorrect w.r.t. a specification. We consider both
user-provided explicit specifications in the form of assertion\r\nstatements in
the code as well as an implicit specification. The implicit specification is inferred
from the non-preemptive behaviour. Let us consider sequences of calls that the
program makes to an external interface. The implicit specification requires that
any such sequence produced under a preemptive scheduler should be included in
the set of sequences produced under a non-preemptive scheduler. We consider several
semantics-preserving fixes that go beyond atomic sections typically explored in
the synchronisation synthesis literature. Our synthesis is able to place locks,
barriers and wait-signal statements and last, but not least reorder independent
statements. The latter may be useful if a thread is released to early, e.g., before
some initialisation is completed. We guarantee that our synthesis does not introduce
deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective
function. We dub our solution trace-based synchronisation synthesis and it is
loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis
works by discovering a trace that is incorrect w.r.t. the specification and identifying
ordering constraints crucial to trigger the specification violation. Synchronisation
may be placed immediately (greedy approach) or delayed until all incorrect traces
are found (non-greedy approach). For the non-greedy approach we construct a set
of global constraints over synchronisation placements. Each model of the global
constraints set corresponds to a correctness-ensuring synchronisation placement.
The placement that is optimal w.r.t. the given objective function is chosen as
the synchronisation solution. We evaluate our approach on a number of realistic
(albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions
of the drivers with known concurrency-related bugs. For the experiments with an
explicit specification we added assertions that would detect the bugs in the experiments.
Device drivers lend themselves to implicit specification, where the device and
the operating system are the external interfaces. Our experiments demonstrate
that our synthesis method is precise and efficient. We implemented objective functions
for coarse-grained and fine-grained locking and observed that different synchronisation
placements are produced for our experiments, favouring e.g. a minimal number of
synchronisation operations or maximum concurrency."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Thorsten
full_name: Tarrach, Thorsten
id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
last_name: Tarrach
orcid: 0000-0003-4409-8487
citation:
ama: Tarrach T. Automatic synthesis of synchronisation primitives for concurrent
programs. 2016. doi:10.15479/at:ista:1130
apa: Tarrach, T. (2016). Automatic synthesis of synchronisation primitives for
concurrent programs. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:1130
chicago: Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for
Concurrent Programs.” Institute of Science and Technology Austria, 2016. https://doi.org/10.15479/at:ista:1130.
ieee: T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent
programs,” Institute of Science and Technology Austria, 2016.
ista: Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent
programs. Institute of Science and Technology Austria.
mla: Tarrach, Thorsten. Automatic Synthesis of Synchronisation Primitives for
Concurrent Programs. Institute of Science and Technology Austria, 2016, doi:10.15479/at:ista:1130.
short: T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent
Programs, Institute of Science and Technology Austria, 2016.
date_created: 2018-12-11T11:50:19Z
date_published: 2016-07-07T00:00:00Z
date_updated: 2023-09-07T11:57:01Z
day: '07'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
- _id: GradSch
doi: 10.15479/at:ista:1130
ec_funded: 1
file:
- access_level: open_access
checksum: 319a506831650327e85376db41fc1094
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T11:39:32Z
date_updated: 2021-02-22T11:39:32Z
file_id: '9179'
file_name: 2016_Tarrach_Thesis.pdf
file_size: 1523935
relation: main_file
success: 1
- access_level: closed
checksum: 39efcd789f0ad859ff15652cb7afc412
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-16T14:14:38Z
date_updated: 2021-11-17T13:46:55Z
file_id: '10296'
file_name: 2016_Tarrach_Thesispdfa.pdf
file_size: 1306068
relation: main_file
file_date_updated: 2021-11-17T13:46:55Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf
month: '07'
oa: 1
oa_version: Published Version
page: '151'
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6230'
related_material:
record:
- id: '1729'
relation: part_of_dissertation
status: public
- id: '2218'
relation: part_of_dissertation
status: public
- id: '2445'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
title: Automatic synthesis of synchronisation primitives for concurrent programs
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2016'
...
---
_id: '1134'
abstract:
- lang: eng
text: 'Hybrid systems have both continuous and discrete dynamics and are useful
for modeling a variety of control systems, from air traffic control protocols
to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools
for analyzing hybrid systems have emerged. Several of these tools implement automated
formal methods for mathematically proving a system meets a specification. This
tutorial session will present three recent hybrid systems tools: C2E2, HyST, and
TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses
validated numerical solvers and bloating of simulation traces to verify systems
meet specifications. HyST is a hybrid systems model transformation and translation
tool, and uses a canonical intermediate representation to support most of the
recent verification tools, as well as automated sound abstractions that simplify
verification of a given hybrid system. TuLiP is a controller synthesis tool for
hybrid systems, where given a temporal logic specification to be satisfied for
a system (plant) model, TuLiP will find a controller that meets a given specification.
© 2016 IEEE.'
article_number: '7587948'
author:
- first_name: Parasara
full_name: Duggirala, Parasara
last_name: Duggirala
- first_name: Chuchu
full_name: Fan, Chuchu
last_name: Fan
- first_name: Matthew
full_name: Potok, Matthew
last_name: Potok
- first_name: Bolun
full_name: Qi, Bolun
last_name: Qi
- first_name: Sayan
full_name: Mitra, Sayan
last_name: Mitra
- first_name: Mahesh
full_name: Viswanathan, Mahesh
last_name: Viswanathan
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Luan
full_name: Nguyen, Luan
last_name: Nguyen
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Andrew
full_name: Sogokon, Andrew
last_name: Sogokon
- first_name: Hoang
full_name: Tran, Hoang
last_name: Tran
- first_name: Weiming
full_name: Xiang, Weiming
last_name: Xiang
citation:
ama: 'Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems
verification transformation and synthesis C2E2 HyST and TuLiP. In: 2016 IEEE
Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948'
apa: 'Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang,
W. (2016). Tutorial: Software tools for hybrid systems verification transformation
and synthesis C2E2 HyST and TuLiP. In 2016 IEEE Conference on Control Applications.
Buenos Aires, Argentina : IEEE. https://doi.org/10.1109/CCA.2016.7587948'
chicago: 'Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra,
Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems
Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In 2016 IEEE
Conference on Control Applications. IEEE, 2016. https://doi.org/10.1109/CCA.2016.7587948.'
ieee: 'P. Duggirala et al., “Tutorial: Software tools for hybrid systems
verification transformation and synthesis C2E2 HyST and TuLiP,” in 2016 IEEE
Conference on Control Applications, Buenos Aires, Argentina , 2016.'
ista: 'Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov
S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial:
Software tools for hybrid systems verification transformation and synthesis C2E2
HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications
, 7587948.'
mla: 'Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification
Transformation and Synthesis C2E2 HyST and TuLiP.” 2016 IEEE Conference on
Control Applications, 7587948, IEEE, 2016, doi:10.1109/CCA.2016.7587948.'
short: P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak,
S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang,
in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.
conference:
end_date: 2016-09-22
location: 'Buenos Aires, Argentina '
name: 'CCA: Control Applications '
start_date: 2016-09-19
date_created: 2018-12-11T11:50:20Z
date_published: 2016-10-10T00:00:00Z
date_updated: 2021-01-12T06:48:32Z
day: '10'
department:
- _id: ToHe
doi: 10.1109/CCA.2016.7587948
language:
- iso: eng
month: '10'
oa_version: None
publication: 2016 IEEE Conference on Control Applications
publication_status: published
publisher: IEEE
publist_id: '6224'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Tutorial: Software tools for hybrid systems verification transformation and
synthesis C2E2 HyST and TuLiP'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1135'
abstract:
- lang: eng
text: 'Time-triggered (TT) switched networks are a deterministic communication infrastructure
used by real-time distributed embedded systems. These networks rely on the notion
of globally discretized time (i.e. time slots) and a static TT schedule that prescribes
which message is sent through which link at every time slot, such that all messages
reach their destination before a global timeout. These schedules are generated
offline, assuming a static network with fault-free links, and entrusting all error-handling
functions to the end user. Assuming the network is static is an over-optimistic
view, and indeed links tend to fail in practice. We study synthesis of TT schedules
on a network in which links fail over time and we assume the switches run a very
simple error-recovery protocol once they detect a crashed link. We address the
problem of finding a pk; qresistant schedule; namely, one that, assuming the switches
run a fixed error-recovery protocol, guarantees that the number of messages that
arrive at their destination by the timeout is at least no matter what sequence
of at most k links fail. Thus, we maintain the simplicity of the switches while
giving a guarantee on the number of messages that meet the timeout. We show how
a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a
schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing
fault sequence to generate a constraint that is added to the program. The newly
added constraint disallows the schedule to be regenerated in a future iteration
while also eliminating several other schedules that are not pk; q-resistant. We
illustrate the applicability of our approach using an SMT-based implementation.
© 2016 ACM.'
article_number: '26'
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Shibashis
full_name: Guha, Shibashis
last_name: Guha
- first_name: Guillermo
full_name: Rodríguez Navas, Guillermo
last_name: Rodríguez Navas
citation:
ama: 'Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for
switched networks with faulty links. In: Proceedings of the 13th International
Conference on Embedded Software . ACM; 2016. doi:10.1145/2968478.2968499'
apa: 'Avni, G., Guha, S., & Rodríguez Navas, G. (2016). Synthesizing time triggered
schedules for switched networks with faulty links. In Proceedings of the 13th
International Conference on Embedded Software . Pittsburgh, PA, USA: ACM.
https://doi.org/10.1145/2968478.2968499'
chicago: Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing
Time Triggered Schedules for Switched Networks with Faulty Links.” In Proceedings
of the 13th International Conference on Embedded Software . ACM, 2016. https://doi.org/10.1145/2968478.2968499.
ieee: G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules
for switched networks with faulty links,” in Proceedings of the 13th International
Conference on Embedded Software , Pittsburgh, PA, USA, 2016.
ista: 'Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules
for switched networks with faulty links. Proceedings of the 13th International
Conference on Embedded Software . EMSOFT: Embedded Software , 26.'
mla: Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks
with Faulty Links.” Proceedings of the 13th International Conference on Embedded
Software , 26, ACM, 2016, doi:10.1145/2968478.2968499.
short: G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International
Conference on Embedded Software , ACM, 2016.
conference:
end_date: 2016-10-07
location: Pittsburgh, PA, USA
name: 'EMSOFT: Embedded Software '
start_date: 2016-10-01
date_created: 2018-12-11T11:50:20Z
date_published: 2016-10-01T00:00:00Z
date_updated: 2021-01-12T06:48:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/2968478.2968499
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:31Z
date_updated: 2018-12-12T10:09:31Z
file_id: '4755'
file_name: IST-2016-644-v1+1_emsoft-no-format.pdf
file_size: 279240
relation: main_file
file_date_updated: 2018-12-12T10:09:31Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted 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: The Wittgenstein Prize
publication: 'Proceedings of the 13th International Conference on Embedded Software '
publication_status: published
publisher: ACM
publist_id: '6223'
pubrep_id: '644'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synthesizing time triggered schedules for switched networks with faulty links
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1138'
abstract:
- lang: eng
text: Automata with monitor counters, where the transitions do not depend on counter
values, and nested weighted automata are two expressive automata-theoretic frameworks
for quantitative properties. For a well-studied and wide class of quantitative
functions, we establish that automata with monitor counters and nested weighted
automata are equivalent. We study for the first time such quantitative automata
under probabilistic semantics. We show that several problems that are undecidable
for the classical questions of emptiness and universality become decidable under
the probabilistic semantics. We present a complete picture of decidability for
such automata, and even an almost-complete picture of computational complexity,
for the probabilistic questions we consider. © 2016 ACM.
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 (Wittgenstein Award), FWF Grant No P23499-
N23, FWF NFN Grant No S114
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 automata under probabilistic
semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE;
2016:76-85. doi:10.1145/2933575.2933588'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata
under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium
(pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual
ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under
probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium,
New York, NY, USA, 2016, pp. 76–85.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic
semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer
Science, 76–85.'
mla: Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.”
Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85,
doi:10.1145/2933575.2933588.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual
ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.
conference:
end_date: 2016-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2016-07-05
date_created: 2018-12-11T11:50:21Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:48:34Z
day: '05'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/2933575.2933588
ec_funded: 1
external_id:
arxiv:
- '1604.06764'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '07'
oa: 1
oa_version: Preprint
page: 76 - 85
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st Annual ACM/IEEE Symposium
publication_status: published
publisher: IEEE
publist_id: '6220'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative automata under probabilistic semantics
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1148'
abstract:
- lang: eng
text: Continuous-time Markov chain (CTMC) models have become a central tool for
understanding the dynamics of complex reaction networks and the importance of
stochasticity in the underlying biochemical processes. When such models are employed
to answer questions in applications, in order to ensure that the model provides
a sufficiently accurate representation of the real system, it is of vital importance
that the model parameters are inferred from real measured data. This, however,
is often a formidable task and all of the existing methods fail in one case or
the other, usually because the underlying CTMC model is high-dimensional and computationally
difficult to analyze. The parameter inference methods that tend to scale best
in the dimension of the CTMC are based on so-called moment closure approximations.
However, there exists a large number of different moment closure approximations
and it is typically hard to say a priori which of the approximations is the most
suitable for the inference procedure. Here, we propose a moment-based parameter
inference method that automatically chooses the most appropriate moment closure
method. Accordingly, contrary to existing methods, the user is not required to
be experienced in moment closure techniques. In addition to that, our method adaptively
changes the approximation during the parameter inference to ensure that always
the best approximation is used, even in cases where different approximations are
best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd
acknowledgement: This work is based on the CMSB 2015 paper “Adaptive moment closure
for parameter inference of biochemical reaction networks” (Bogomolov et al., 2015).
The work was partly supported by the German Research Foundation (DFG) as part of
the Transregional Collaborative Research Center “Automatic Verification and Analysis
of Complex Systems” (SFB/TR 14 AVACS1), 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). J.R. acknowledges support from the People
Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme
(FP7/2007-2013) under REA grant agreement no. 291734.
author:
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
citation:
ama: Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. Adaptive moment
closure for parameter inference of biochemical reaction networks. Biosystems.
2016;149:15-25. doi:10.1016/j.biosystems.2016.07.005
apa: Schilling, C., Bogomolov, S., Henzinger, T. A., Podelski, A., & Ruess,
J. (2016). Adaptive moment closure for parameter inference of biochemical reaction
networks. Biosystems. Elsevier. https://doi.org/10.1016/j.biosystems.2016.07.005
chicago: Schilling, Christian, Sergiy Bogomolov, Thomas A Henzinger, Andreas Podelski,
and Jakob Ruess. “Adaptive Moment Closure for Parameter Inference of Biochemical
Reaction Networks.” Biosystems. Elsevier, 2016. https://doi.org/10.1016/j.biosystems.2016.07.005.
ieee: C. Schilling, S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess, “Adaptive
moment closure for parameter inference of biochemical reaction networks,” Biosystems,
vol. 149. Elsevier, pp. 15–25, 2016.
ista: Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. 2016. Adaptive
moment closure for parameter inference of biochemical reaction networks. Biosystems.
149, 15–25.
mla: Schilling, Christian, et al. “Adaptive Moment Closure for Parameter Inference
of Biochemical Reaction Networks.” Biosystems, vol. 149, Elsevier, 2016,
pp. 15–25, doi:10.1016/j.biosystems.2016.07.005.
short: C. Schilling, S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, Biosystems
149 (2016) 15–25.
date_created: 2018-12-11T11:50:24Z
date_published: 2016-11-01T00:00:00Z
date_updated: 2023-02-23T10:08:46Z
day: '01'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1016/j.biosystems.2016.07.005
ec_funded: 1
intvolume: ' 149'
language:
- iso: eng
month: '11'
oa_version: None
page: 15 - 25
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Biosystems
publication_status: published
publisher: Elsevier
publist_id: '6210'
quality_controlled: '1'
related_material:
record:
- id: '1658'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Adaptive moment closure for parameter inference of biochemical reaction networks
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 149
year: '2016'
...
---
_id: '1166'
abstract:
- lang: eng
text: POMDPs are standard models for probabilistic planning problems, where an agent
interacts with an uncertain environment. We study the problem of almost-sure reachability,
where given a set of target states, the question is to decide whether there is
a policy to ensure that the target set is reached with probability 1 (almost-surely).
While in general the problem is EXPTIMEcomplete, in many practical cases policies
with a small amount of memory suffice. Moreover, the existing solution to the
problem is explicit, which first requires to construct explicitly an exponential
reduction to a belief-support MDP. In this work, we first study the existence
of observation-stationary strategies, which is NP-complete, and then small-memory
strategies. We present a symbolic algorithm by an efficient encoding to SAT and
using a SAT solver for the problem. We report experimental results demonstrating
the scalability of our symbolic (SAT-based) approach. © 2016, Association for
the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
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: Jessica
full_name: Davies, Jessica
id: 378E0060-F248-11E8-B48F-1D18A9856A87
last_name: Davies
citation:
ama: 'Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost
sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth
AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.'
apa: 'Chatterjee, K., Chmelik, M., & Davies, J. (2016). A symbolic SAT based
algorithm for almost sure reachability with small strategies in pomdps. In Proceedings
of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp.
3225–3232). Phoenix, AZ, USA: AAAI Press.'
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic
SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.”
In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence,
2016:3225–32. AAAI Press, 2016.
ieee: K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm
for almost sure reachability with small strategies in pomdps,” in Proceedings
of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ,
USA, 2016, vol. 2016, pp. 3225–3232.
ista: 'Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for
almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 2016, 3225–3232.'
mla: Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure
Reachability with Small Strategies in Pomdps.” Proceedings of the Thirtieth
AAAI Conference on Artificial Intelligence, vol. 2016, AAAI Press, 2016, pp.
3225–32.
short: K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI
Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.
conference:
end_date: 2016-02-17
location: Phoenix, AZ, USA
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2016-02-12
date_created: 2018-12-11T11:50:30Z
date_published: 2016-12-02T00:00:00Z
date_updated: 2023-02-23T12:26:41Z
day: '02'
department:
- _id: KrCh
- _id: ToHe
ec_funded: 1
intvolume: ' 2016'
language:
- iso: eng
month: '12'
oa_version: None
page: 3225 - 3232
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'
publication: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '6191'
quality_controlled: '1'
related_material:
link:
- relation: table_of_contents
url: https://dl.acm.org/citation.cfm?id=3016355
record:
- id: '5443'
relation: earlier_version
status: public
status: public
title: A symbolic SAT based algorithm for almost sure reachability with small strategies
in pomdps
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2016
year: '2016'
...
---
_id: '1205'
abstract:
- lang: eng
text: In this paper, we present a formal model-driven engineering approach to establishing
a safety-assured implementation of Multifunction vehicle bus controller (MVBC)
based on the generic reference models and requirements described in the International
Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models
described in IEC-61375 are translated into a network of timed automata, and some
safety requirements tested in IEC-61375 are formalized as timed computation tree
logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the
timed automata satisfy the formulas or not. Within this step, several logic inconsistencies
in the original standard are detected and corrected. Then, we apply the tool Times
to generate C code from the verified model, which was later synthesized into a
real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify
some safety requirements at the implementation level. We set up a real platform
with worldwide mostly used MVBC D113, and verify the correctness and the scalability
of the synthesized MVBC chip more comprehensively. The errors in the standard
has been confirmed and the resulted MVBC has been deployed in real train communication
network.
acknowledgement: "This research is sponsored in part by NSFC Program (No. 91218302,
No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101),
Tsinghua University Initiative Scientific Research Program (20131089331), MIIT IT
funds (Research and application of TCN key technologies) of China, and the National
Key Technology R&D Program (No. 2015BAG14B01-02), Austrian Science Fund (FWF) under
grants S11402-N23 (RiSE/SHiNE) and Z211-N23.\r\n"
alternative_title:
- LNCS
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Houbing
full_name: Song, Houbing
last_name: Song
- 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, Liu H, Song H, et al. Safety assured formal model driven design of
the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763.
doi:10.1007/978-3-319-48989-6_47'
apa: 'Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., & Sha, L. (2016).
Safety assured formal model driven design of the multifunction vehicle bus controller
(Vol. 9995, pp. 757–763). Presented at the FM: International Symposium on Formal
Methods, Limassol, Cyprus: Springer. https://doi.org/10.1007/978-3-319-48989-6_47'
chicago: Jiang, Yu, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, and
Lui Sha. “Safety Assured Formal Model Driven Design of the Multifunction Vehicle
Bus Controller,” 9995:757–63. Springer, 2016. https://doi.org/10.1007/978-3-319-48989-6_47.
ieee: 'Y. Jiang et al., “Safety assured formal model driven design of the
multifunction vehicle bus controller,” presented at the FM: International Symposium
on Formal Methods, Limassol, Cyprus, 2016, vol. 9995, pp. 757–763.'
ista: 'Jiang Y, Liu H, Song H, Kong H, Gu M, Sun J, Sha L. 2016. Safety assured
formal model driven design of the multifunction vehicle bus controller. FM: International
Symposium on Formal Methods, LNCS, vol. 9995, 757–763.'
mla: Jiang, Yu, et al. Safety Assured Formal Model Driven Design of the Multifunction
Vehicle Bus Controller. Vol. 9995, Springer, 2016, pp. 757–63, doi:10.1007/978-3-319-48989-6_47.
short: Y. Jiang, H. Liu, H. Song, H. Kong, M. Gu, J. Sun, L. Sha, in:, Springer,
2016, pp. 757–763.
conference:
end_date: 2016-11-11
location: Limassol, Cyprus
name: 'FM: International Symposium on Formal Methods'
start_date: 2016-11-09
date_created: 2018-12-11T11:50:42Z
date_published: 2016-11-08T00:00:00Z
date_updated: 2023-09-18T08:12:48Z
day: '08'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-319-48989-6_47
file:
- access_level: open_access
checksum: fea0b3fae9a2a42e8bfec59840e30d8c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:13Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4673'
file_name: IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf
file_size: 281501
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 9995'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 757 - 763
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: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '6144'
pubrep_id: '783'
quality_controlled: '1'
related_material:
record:
- id: '434'
relation: later_version
status: public
scopus_import: 1
status: public
title: Safety assured formal model driven design of the multifunction vehicle bus
controller
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9995
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
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: 2021-01-12T08:00:55Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2889160.2889233
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
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
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2020-08-11T10:09:14Z
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: The Wittgenstein Prize
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: 2021-01-12T06:51:10Z
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: The Wittgenstein Prize
- _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).'
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.
date_created: 2018-12-11T11:52:23Z
date_published: 2015-10-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10703-015-0235-2
ec_funded: 1
intvolume: ' 47'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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 '
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: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2737166.2737175
ec_funded: 1
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'
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: The Wittgenstein Prize
- _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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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). '
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: 2021-01-12T06:51:27Z
day: '30'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1073/pnas.1423947112
ec_funded: 1
external_id:
pmid:
- '26085136'
intvolume: ' 112'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 112
year: '2015'
...