---
_id: '14242'
abstract:
- lang: eng
text: We study the problem of training and certifying adversarially robust quantized
neural networks (QNNs). Quantization is a technique for making neural networks
more efficient by running them using low-bit integer arithmetic and is therefore
commonly adopted in industry. Recent work has shown that floating-point neural
networks that have been verified to be robust can become vulnerable to adversarial
attacks after quantization, and certification of the quantized representation
is necessary to guarantee robustness. In this work, we present quantization-aware
interval bound propagation (QA-IBP), a novel method for training robust QNNs.
Inspired by advances in robust learning of non-quantized networks, our training
algorithm computes the gradient of an abstract representation of the actual network.
Unlike existing approaches, our method can handle the discrete semantics of QNNs.
Based on QA-IBP, we also develop a complete verification procedure for verifying
the adversarial robustness of QNNs, which is guaranteed to terminate and produce
a correct answer. Compared to existing approaches, the key advantage of our verification
procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate
experimentally that our approach significantly outperforms existing methods and
establish the new state-of-the-art for training and certifying the robustness
of QNNs.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. Research
was sponsored by the United\r\nStates Air Force Research Laboratory and the United
States Air Force Artificial Intelligence Accelerator and was accomplished under
Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained
in this document are those of the authors and should not be interpreted as representing
the official policies, either expressed or implied,\r\nof the United States Air
Force or the U.S. Government. The U.S. Government is authorized to reproduce and
distribute reprints for Government purposes notwithstanding any copyright\r\nnotation
herein. The research was also funded in part by the AI2050 program at Schmidt Futures
(Grant G-22-63172) and Capgemini SE."
article_processing_charge: No
arxiv: 1
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- 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: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973.
doi:10.1609/aaai.v37i12.26747'
apa: 'Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., & Rus, D.
(2023). Quantization-aware interval bound propagation for training certifiably
robust quantized neural networks. In Proceedings of the 37th AAAI Conference
on Artificial Intelligence (Vol. 37, pp. 14964–14973). Washington, DC, United
States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i12.26747'
chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger,
and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks.” In Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 37:14964–73. Association for the Advancement of
Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i12.26747.
ieee: M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks,”
in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.
ista: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference
on Artificial Intelligence vol. 37, 14964–14973.'
mla: Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for
Training Certifiably Robust Quantized Neural Networks.” Proceedings of the
37th AAAI Conference on Artificial Intelligence, vol. 37, no. 12, Association
for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:10.1609/aaai.v37i12.26747.
short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings
of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2023, pp. 14964–14973.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:17Z
date_published: 2023-06-26T00:00:00Z
date_updated: 2025-07-14T09:09:56Z
day: '26'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i12.26747
ec_funded: 1
external_id:
arxiv:
- '2211.16187'
intvolume: ' 37'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2211.16187
month: '06'
oa: 1
oa_version: Preprint
page: 14964-14973
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantization-aware interval bound propagation for training certifiably robust
quantized neural networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14243'
abstract:
- lang: eng
text: 'Two-player zero-sum "graph games" are central in logic, verification, and
multi-agent systems. The game proceeds by placing a token on a vertex of a graph,
and allowing the players to move it to produce an infinite path, which determines
the winner or payoff of the game. Traditionally, the players alternate turns in
moving the token. In "bidding games", however, the players have budgets and in
each turn, an auction (bidding) determines which player moves the token. So far,
bidding games have only been studied as full-information games. In this work we
initiate the study of partial-information bidding games: we study bidding games
in which a player''s initial budget is drawn from a known probability distribution.
We show that while for some bidding mechanisms and objectives, it is straightforward
to adapt the results from the full-information setting to the partial-information
setting, for others, the analysis is significantly more challenging, requires
new techniques, and gives rise to interesting results. Specifically, we study
games with "mean-payoff" objectives in combination with "poorman" bidding. We
construct optimal strategies for a partially-informed player who plays against
a fully-informed adversary. We show that, somewhat surprisingly, the "value" under
pure strategies does not necessarily exist in such games.'
acknowledgement: This research was supported in part by ISF grant no.1679/21, by the
ERC CoG 863818 (ForM-SMArt), and the European Union’s Horizon 2020 research and
innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
article_processing_charge: No
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Ismael R
full_name: Jecker, Ismael R
id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
last_name: Jecker
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable
budgets. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. ; 2023:5464-5471. doi:10.1609/aaai.v37i5.25679'
apa: Avni, G., Jecker, I. R., & Zikelic, D. (2023). Bidding graph games with
partially-observable budgets. In Proceedings of the 37th AAAI Conference on
Artificial Intelligence (Vol. 37, pp. 5464–5471). Washington, DC, United States.
https://doi.org/10.1609/aaai.v37i5.25679
chicago: Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with
Partially-Observable Budgets.” In Proceedings of the 37th AAAI Conference on
Artificial Intelligence, 37:5464–71, 2023. https://doi.org/10.1609/aaai.v37i5.25679.
ieee: G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable
budgets,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.
ista: 'Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable
budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI:
Conference on Artificial Intelligence vol. 37, 5464–5471.'
mla: Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.”
Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol.
37, no. 5, 2023, pp. 5464–71, doi:10.1609/aaai.v37i5.25679.
short: G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 2023, pp. 5464–5471.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:18Z
date_published: 2023-06-27T00:00:00Z
date_updated: 2025-07-14T09:09:56Z
day: '27'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i5.25679
ec_funded: 1
external_id:
arxiv:
- '2211.13626'
intvolume: ' 37'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1609/aaai.v37i5.25679
month: '06'
oa: 1
oa_version: Published Version
page: 5464-5471
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding graph games with partially-observable budgets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14400'
abstract:
- lang: eng
text: "We consider the problem of computing the maximal probability of satisfying
an \r\n-regular specification for stochastic, continuous-state, nonlinear systems
evolving in discrete time. The problem reduces, after automata-theoretic constructions,
to finding the maximal probability of satisfying a parity condition on a (possibly
hybrid) state space. While characterizing the exact satisfaction probability is
open, we show that a lower bound on this probability can be obtained by (I) computing
an under-approximation of the qualitative winning region, i.e., states from which
the parity condition can be enforced almost surely, and (II) computing the maximal
probability of reaching this qualitative winning region.\r\nThe heart of our approach
is a technique to symbolically compute the under-approximation of the qualitative
winning region in step (I) via a finite-state abstraction of the original system
as a \r\n-player parity game. Our abstraction procedure uses only the support
of the probabilistic evolution; it does not use precise numerical transition probabilities.
We prove that the winning set in the abstract -player game induces an under-approximation
of the qualitative winning region in the original synthesis problem, along with
a policy to solve it. By combining these contributions with (a) a symbolic fixpoint
algorithm to solve \r\n-player games and (b) existing techniques for reachability
policy synthesis in stochastic nonlinear systems, we get an abstraction-based
algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe
have implemented the abstraction-based algorithm in Mascot-SDS, where we combined
the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that
solves \r\n-player parity games (through a reduction to Rabin games) more efficiently
than existing algorithms. We evaluated our implementation on the nonlinear model
of a perturbed bistable switch from the literature. We show empirically that the
lower bound on the winning region computed by our approach is precise, by comparing
against an over-approximation of the qualitative winning region. Moreover, our
implementation outperforms a recently proposed tool for solving this problem by
a large margin."
acknowledgement: "We thank Daniel Hausmann and Nir Piterman for their valuable comments
on an earlier version of the manuscript of our other paper [22] where we present,
among other things, the parity fixpoint for 2 1/2-player games (for a slightly more
general class of games) with a different and indirect proof of correctness. Based
on their comments we observed that, unlike the other fixpoints that we present in
[22], the parity fixpoint does not follow the exact same structure as its counterpart
for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini
Raghavan for observing that our symbolic parity fixpoint algorithm can be solved
in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus
expressions. This significantly improved the complexity bounds of our algorithm
in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported
by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded
through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC
project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects:
EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047."
article_number: '101430'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic
systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 2023;51.
doi:10.1016/j.nahs.2023.101430'
apa: 'Majumdar, R., Mallik, K., Schmuck, A. K., & Soudjani, S. (2023). Symbolic
control for stochastic systems via finite parity games. Nonlinear Analysis:
Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2023.101430'
chicago: 'Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani.
“Symbolic Control for Stochastic Systems via Finite Parity Games.” Nonlinear
Analysis: Hybrid Systems. Elsevier, 2023. https://doi.org/10.1016/j.nahs.2023.101430.'
ieee: 'R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control
for stochastic systems via finite parity games,” Nonlinear Analysis: Hybrid
Systems, vol. 51. Elsevier, 2023.'
ista: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2023. Symbolic control for
stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems.
51, 101430.'
mla: 'Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite
Parity Games.” Nonlinear Analysis: Hybrid Systems, vol. 51, 101430, Elsevier,
2023, doi:10.1016/j.nahs.2023.101430.'
short: 'R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid
Systems 51 (2023).'
date_created: 2023-10-08T22:01:15Z
date_published: 2023-09-27T00:00:00Z
date_updated: 2023-12-13T12:58:56Z
day: '27'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2023.101430
ec_funded: 1
external_id:
arxiv:
- '2101.00834'
isi:
- '001093188100001'
intvolume: ' 51'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.nahs.2023.101430
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
issn:
- 1751-570X
publication_status: epub_ahead
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic control for stochastic systems via finite parity games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 51
year: '2023'
...
---
_id: '14405'
abstract:
- lang: eng
text: We introduce hypernode automata as a new specification formalism for hyperproperties
of concurrent systems. They are finite automata with nodes labeled with hypernode
logic formulas and transitions labeled with actions. A hypernode logic formula
specifies relations between sequences of variable values in different system executions.
Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces
by constraining the values and the order of value changes of each variable without
correlating the timing of the changes. Different execution traces are synchronized
solely through the transitions of hypernode automata. Hypernode automata naturally
combine asynchronicity at the node level with synchronicity at the transition
level. We show that the model-checking problem for hypernode automata is decidable
over action-labeled Kripke structures, whose actions induce transitions of the
specification automata. For this reason, hypernode automaton is a suitable formalism
for specifying and verifying asynchronous hyperproperties, such as declassifying
observational determinism in multi-threaded programs.
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)
SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the
ERC Advanced Grant\r\nVAMOS 101020093."
alternative_title:
- LIPIcs
article_number: '21'
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata.
In: 34th International Conference on Concurrency Theory. Vol 279. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.21'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2023). Hypernode automata. In 34th International Conference on Concurrency
Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21'
chicago: Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Hypernode Automata.” In 34th International Conference on Concurrency
Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
https://doi.org/10.4230/LIPIcs.CONCUR.2023.21.
ieee: E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode
automata,” in 34th International Conference on Concurrency Theory, Antwerp,
Belgium, 2023, vol. 279.
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode
automata. 34th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 279, 21.'
mla: Bartocci, Ezio, et al. “Hypernode Automata.” 34th International Conference
on Concurrency Theory, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.21.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th
International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023.
conference:
end_date: 2023-09-22
location: Antwerp, Belgium
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2023-09-19
date_created: 2023-10-08T22:01:16Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2023-10-09T07:43:44Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.21
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 215765e40454d806174ac0a223e8d6fa
content_type: application/pdf
creator: dernst
date_created: 2023-10-09T07:42:45Z
date_updated: 2023-10-09T07:42:45Z
file_id: '14413'
file_name: 2023_LIPcs_Bartocci.pdf
file_size: 795790
relation: main_file
success: 1
file_date_updated: 2023-10-09T07:42:45Z
has_accepted_license: '1'
intvolume: ' 279'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 34th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959772990'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Hypernode automata
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: 279
year: '2023'
...
---
_id: '14411'
abstract:
- lang: eng
text: "Partially specified Boolean networks (PSBNs) represent a promising framework
for the qualitative modelling of biological systems in which the logic of interactions
is not completely known. Phenotype control aims to stabilise the network in states
exhibiting specific traits.\r\nIn this paper, we define the phenotype control
problem in the context of asynchronous PSBNs and propose a novel semi-symbolic
algorithm for solving this problem with permanent variable perturbations."
acknowledgement: This work was supported by the Czech Foundation grant No. GA22-10845S,
Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European
Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie
Grant Agreement No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
- first_name: Eva
full_name: Šmijáková, Eva
last_name: Šmijáková
citation:
ama: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially
specified boolean networks. In: 21st International Conference on Computational
Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2'
apa: 'Beneš, N., Brim, L., Pastva, S., Šafránek, D., & Šmijáková, E. (2023).
Phenotype control of partially specified boolean networks. In 21st International
Conference on Computational Methods in Systems Biology (Vol. 14137, pp. 18–35).
Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-42697-1_2'
chicago: Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková.
“Phenotype Control of Partially Specified Boolean Networks.” In 21st International
Conference on Computational Methods in Systems Biology, 14137:18–35. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-42697-1_2.
ieee: N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control
of partially specified boolean networks,” in 21st International Conference
on Computational Methods in Systems Biology, Luxembourg City, Luxembourg,
2023, vol. 14137, pp. 18–35.
ista: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control
of partially specified boolean networks. 21st International Conference on Computational
Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI,
vol. 14137, 18–35.'
mla: Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.”
21st International Conference on Computational Methods in Systems Biology,
vol. 14137, Springer Nature, 2023, pp. 18–35, doi:10.1007/978-3-031-42697-1_2.
short: N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International
Conference on Computational Methods in Systems Biology, Springer Nature, 2023,
pp. 18–35.
conference:
end_date: 2023-09-15
location: Luxembourg City, Luxembourg
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2023-09-13
date_created: 2023-10-08T22:01:18Z
date_published: 2023-09-09T00:00:00Z
date_updated: 2024-02-20T09:02:04Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-42697-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: 6f71bdaedb770b52380222fd9f4d7937
content_type: application/pdf
creator: spastva
date_created: 2024-02-16T08:26:32Z
date_updated: 2024-02-16T08:26:32Z
file_id: '14997'
file_name: cmsb2023.pdf
file_size: 691582
relation: main_file
success: 1
file_date_updated: 2024-02-16T08:26:32Z
has_accepted_license: '1'
intvolume: ' 14137'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 18-35
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 21st International Conference on Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031426964'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Phenotype control of partially specified boolean networks
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: 14137
year: '2023'
...
---
_id: '14454'
abstract:
- lang: eng
text: As AI and machine-learned software are used increasingly for making decisions
that affect humans, it is imperative that they remain fair and unbiased in their
decisions. To complement design-time bias mitigation measures, runtime verification
techniques have been introduced recently to monitor the algorithmic fairness of
deployed systems. Previous monitoring techniques assume full observability of
the states of the (unknown) monitored system. Moreover, they can monitor only
fairness properties that are specified as arithmetic expressions over the probabilities
of different events. In this work, we extend fairness monitoring to systems modeled
as partially observed Markov chains (POMC), and to specifications containing arithmetic
expressions over the expected values of numerical functions on event sequences.
The only assumptions we make are that the underlying POMC is aperiodic and starts
in the stationary distribution, with a bound on its mixing time being known. These
assumptions enable us to estimate a given property for the entire distribution
of possible executions of the monitored POMC, by observing only a single execution.
Our monitors observe a long run of the system and, after each new observation,
output updated PAC-estimates of how fair or biased the system is. The monitors
are computationally lightweight and, using a prototype implementation, we demonstrate
their effectiveness on several real-world examples.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under
partial observations. In: 23rd International Conference on Runtime Verification.
Vol 14245. Springer Nature; 2023:291-311. doi:10.1007/978-3-031-44267-4_15'
apa: 'Henzinger, T. A., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic
fairness under partial observations. In 23rd International Conference on Runtime
Verification (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature.
https://doi.org/10.1007/978-3-031-44267-4_15'
chicago: Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring
Algorithmic Fairness under Partial Observations.” In 23rd International Conference
on Runtime Verification, 14245:291–311. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_15.
ieee: T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness
under partial observations,” in 23rd International Conference on Runtime Verification,
Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311.
ista: 'Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness
under partial observations. 23rd International Conference on Runtime Verification.
RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial
Observations.” 23rd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 291–311, doi:10.1007/978-3-031-44267-4_15.
short: T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference
on Runtime Verification, Springer Nature, 2023, pp. 291–311.
conference:
end_date: 2023-10-06
location: Thessaloniki, Greece
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-03
date_created: 2023-10-29T23:01:15Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2023-10-31T11:48:20Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_15
ec_funded: 1
external_id:
arxiv:
- '2308.00341'
intvolume: ' 14245'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2308.00341
month: '10'
oa: 1
oa_version: Preprint
page: 291-311
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23rd International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031442667'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring algorithmic fairness under partial observations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14245
year: '2023'
...
---
_id: '14518'
abstract:
- lang: eng
text: We consider bidding games, a class of two-player zero-sum graph games. The
game proceeds as follows. Both players have bounded budgets. A token is placed
on a vertex of a graph, in each turn the players simultaneously submit bids, and
the higher bidder moves the token, where we break bidding ties in favor of Player
1. Player 1 wins the game iff the token visits a designated target vertex. We
consider, for the first time, poorman discrete-bidding in which the granularity
of the bids is restricted and the higher bid is paid to the bank. Previous work
either did not impose granularity restrictions or considered Richman bidding (bids
are paid to the opponent). While the latter mechanisms are technically more accessible,
the former is more appealing from a practical standpoint. Our study focuses on
threshold budgets, which is the necessary and sufficient initial budget required
for Player 1 to ensure winning against a given Player 2 budget. We first show
existence of thresholds. In DAGs, we show that threshold budgets can be approximated
with error bounds by thresholds under continuous-bidding and that they exhibit
a periodic behavior. We identify closed-form solutions in special cases. We implement
and experiment with an algorithm to find threshold budgets.
acknowledgement: This research was supported in part by ISF grant no. 1679/21, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie SkłodowskaCurie Grant Agreement No. 665385.
article_processing_charge: No
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Suman
full_name: Sadhukhan, Suman
last_name: Sadhukhan
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. Reachability poorman
discrete-bidding games. In: Frontiers in Artificial Intelligence and Applications.
Vol 372. IOS Press; 2023:141-148. doi:10.3233/FAIA230264'
apa: 'Avni, G., Meggendorfer, T., Sadhukhan, S., Tkadlec, J., & Zikelic, D.
(2023). Reachability poorman discrete-bidding games. In Frontiers in Artificial
Intelligence and Applications (Vol. 372, pp. 141–148). Krakow, Poland: IOS
Press. https://doi.org/10.3233/FAIA230264'
chicago: Avni, Guy, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, and Dorde
Zikelic. “Reachability Poorman Discrete-Bidding Games.” In Frontiers in Artificial
Intelligence and Applications, 372:141–48. IOS Press, 2023. https://doi.org/10.3233/FAIA230264.
ieee: G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, and D. Zikelic, “Reachability
poorman discrete-bidding games,” in Frontiers in Artificial Intelligence and
Applications, Krakow, Poland, 2023, vol. 372, pp. 141–148.
ista: 'Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability
poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications.
ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.'
mla: Avni, Guy, et al. “Reachability Poorman Discrete-Bidding Games.” Frontiers
in Artificial Intelligence and Applications, vol. 372, IOS Press, 2023, pp.
141–48, doi:10.3233/FAIA230264.
short: G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, D. Zikelic, in:, Frontiers
in Artificial Intelligence and Applications, IOS Press, 2023, pp. 141–148.
conference:
end_date: 2023-10-04
location: Krakow, Poland
name: 'ECAI: European Conference on Artificial Intelligence'
start_date: 2023-09-30
date_created: 2023-11-12T23:00:56Z
date_published: 2023-09-28T00:00:00Z
date_updated: 2025-07-14T09:09:57Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.3233/FAIA230264
ec_funded: 1
external_id:
arxiv:
- '2307.15218'
file:
- access_level: open_access
checksum: 1390ca38480fa4cf286b0f1a42e8c12f
content_type: application/pdf
creator: dernst
date_created: 2023-11-13T10:16:10Z
date_updated: 2023-11-13T10:16:10Z
file_id: '14529'
file_name: 2023_FAIA_Avni.pdf
file_size: 501011
relation: main_file
success: 1
file_date_updated: 2023-11-13T10:16:10Z
has_accepted_license: '1'
intvolume: ' 372'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 141-148
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Frontiers in Artificial Intelligence and Applications
publication_identifier:
isbn:
- '9781643684369'
issn:
- 0922-6389
publication_status: published
publisher: IOS Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reachability poorman discrete-bidding games
tmp:
image: /images/cc_by_nc.png
legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
short: CC BY-NC (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 372
year: '2023'
...
---
_id: '14559'
abstract:
- lang: eng
text: We consider the problem of learning control policies in discrete-time stochastic
systems which guarantee that the system stabilizes within some specified stabilization
region with probability 1. Our approach is based on the novel notion of stabilizing
ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome
the limitation of methods proposed in previous works whose applicability is restricted
to systems in which the stabilizing region cannot be left once entered under any
control policy. We present a learning procedure that learns a control policy together
with an sRSM that formally certifies probability 1 stability, both learned as
neural networks. We show that this procedure can also be adapted to formally verifying
that, under a given Lipschitz continuous control policy, the stochastic system
stabilizes within some stabilizing region with probability 1. Our experimental
evaluation shows that our learning procedure can successfully learn provably stabilizing
policies in practice.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Matin
full_name: Ansaripour, Matin
last_name: Ansaripour
- 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: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably
stabilizing neural controllers for discrete-time stochastic systems. In: 21st
International Symposium on Automated Technology for Verification and Analysis.
Vol 14215. Springer Nature; 2023:357-379. doi:10.1007/978-3-031-45329-8_17'
apa: 'Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic,
D. (2023). Learning provably stabilizing neural controllers for discrete-time
stochastic systems. In 21st International Symposium on Automated Technology
for Verification and Analysis (Vol. 14215, pp. 357–379). Singapore, Singapore:
Springer Nature. https://doi.org/10.1007/978-3-031-45329-8_17'
chicago: Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner,
and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time
Stochastic Systems.” In 21st International Symposium on Automated Technology
for Verification and Analysis, 14215:357–79. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-45329-8_17.
ieee: M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic,
“Learning provably stabilizing neural controllers for discrete-time stochastic
systems,” in 21st International Symposium on Automated Technology for Verification
and Analysis, Singapore, Singapore, 2023, vol. 14215, pp. 357–379.
ista: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning
provably stabilizing neural controllers for discrete-time stochastic systems.
21st International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.'
mla: Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers
for Discrete-Time Stochastic Systems.” 21st International Symposium on Automated
Technology for Verification and Analysis, vol. 14215, Springer Nature, 2023,
pp. 357–79, doi:10.1007/978-3-031-45329-8_17.
short: M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:,
21st International Symposium on Automated Technology for Verification and Analysis,
Springer Nature, 2023, pp. 357–379.
conference:
end_date: 2023-10-27
location: Singapore, Singapore
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2023-10-24
date_created: 2023-11-19T23:00:56Z
date_published: 2023-10-22T00:00:00Z
date_updated: 2025-07-14T09:09:59Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-031-45329-8_17
ec_funded: 1
intvolume: ' 14215'
language:
- iso: eng
month: '10'
oa_version: None
page: 357-379
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 21st International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031453281'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning provably stabilizing neural controllers for discrete-time stochastic
systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14215
year: '2023'
...
---
_id: '14718'
abstract:
- lang: eng
text: 'Binary decision diagrams (BDDs) are one of the fundamental data structures
in formal methods and computer science in general. However, the performance of
BDD-based algorithms greatly depends on memory latency due to the reliance on
large hash tables and thus, by extension, on the speed of random memory access.
This hinders the full utilisation of resources available on modern CPUs, since
the absolute memory latency has not improved significantly for at least a decade.
In this paper, we explore several implementation techniques that improve the performance
of BDD manipulation either through enhanced memory locality or by partially eliminating
random memory access. On a benchmark suite of 600+ BDDs derived from real-world
applications, we demonstrate runtime that is comparable or better than parallelising
the same operations on eight CPU cores. '
acknowledgement: "This work was supported by the European Union’s Horizon 2020 research
and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413
and the\r\n“VAMOS” grant ERC-2020-AdG 101020093."
article_processing_charge: No
author:
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: Proceedings
of the 23rd Conference on Formal Methods in Computer-Aided Design. TU Vienna
Academic Press; 2023:122-131. doi:10.34727/2023/isbn.978-3-85448-060-0_20'
apa: 'Pastva, S., & Henzinger, T. A. (2023). Binary decision diagrams on modern
hardware. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20'
chicago: Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern
Hardware.” In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design, 122–31. TU Vienna Academic Press, 2023. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20.
ieee: S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,”
in Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design,
Ames, IA, United States, 2023, pp. 122–131.
ista: 'Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware.
Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design.
FMCAD: Conference on Formal Methods in Computer-aided design, 122–131.'
mla: Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern
Hardware.” Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design, TU Vienna Academic Press, 2023, pp. 122–31, doi:10.34727/2023/isbn.978-3-85448-060-0_20.
short: S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal
Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131.
conference:
end_date: 2023-10-27
location: Ames, IA, United States
name: 'FMCAD: Conference on Formal Methods in Computer-aided design'
start_date: 2023-10-25
date_created: 2023-12-31T23:01:03Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2024-01-02T08:16:28Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2023/isbn.978-3-85448-060-0_20
ec_funded: 1
file:
- access_level: open_access
checksum: 818d6e13dd508f3a04f0941081022e5d
content_type: application/pdf
creator: dernst
date_created: 2024-01-02T08:14:23Z
date_updated: 2024-01-02T08:14:23Z
file_id: '14721'
file_name: 2023_FMCAD_Pastva.pdf
file_size: 524321
relation: main_file
success: 1
file_date_updated: 2024-01-02T08:14:23Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 122-131
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design
publication_identifier:
isbn:
- '9783854480600'
publication_status: published
publisher: TU Vienna Academic Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Binary decision diagrams on modern hardware
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
year: '2023'
...
---
_id: '14758'
abstract:
- lang: eng
text: 'We present a flexible and efficient toolchain to symbolically solve (standard)
Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin
games. To our best knowledge, our tools are the first ones to be able to solve
these problems. Furthermore, using these flexible game solvers as a back-end,
we implemented a tool for computing correct-by-construction controllers for stochastic
dynamical systems under LTL specifications. Our implementations use the recent
theoretical result that all of these games can be solved using the same symbolic
fixpoint algorithm but utilizing different, domain specific calculations of the
involved predecessor operators. The main feature of our toolchain is the utilization
of two programming abstractions: one to separate the symbolic fixpoint computations
from the predecessor calculations, and another one to allow the integration of
different BDD libraries as back-ends. In particular, we employ a multi-threaded
execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan,
which leads to enormous computational savings.'
acknowledgement: 'Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are
partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally
funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project
ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1.
S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802,
and ERC 101089047.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Mateusz
full_name: Rychlicki, Mateusz
last_name: Rychlicki
- first_name: Anne-Kathrin
full_name: Schmuck, Anne-Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain
for symbolic rabin games under fair and stochastic uncertainties. In: 35th
International Conference on Computer Aided Verification. Vol 13966. Springer
Nature; 2023:3-15. doi:10.1007/978-3-031-37709-9_1'
apa: 'Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., & Soudjani, S.
(2023). A flexible toolchain for symbolic rabin games under fair and stochastic
uncertainties. In 35th International Conference on Computer Aided Verification
(Vol. 13966, pp. 3–15). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_1'
chicago: Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck,
and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair
and Stochastic Uncertainties.” In 35th International Conference on Computer
Aided Verification, 13966:3–15. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_1.
ieee: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible
toolchain for symbolic rabin games under fair and stochastic uncertainties,” in
35th International Conference on Computer Aided Verification, Paris, France,
2023, vol. 13966, pp. 3–15.
ista: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible
toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th
International Conference on Computer Aided Verification. CAV: Computer Aided Verification,
LNCS, vol. 13966, 3–15.'
mla: Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under
Fair and Stochastic Uncertainties.” 35th International Conference on Computer
Aided Verification, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:10.1007/978-3-031-37709-9_1.
short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th
International Conference on Computer Aided Verification, Springer Nature, 2023,
pp. 3–15.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2024-01-08T13:18:00Z
date_published: 2023-07-16T00:00:00Z
date_updated: 2024-02-27T07:39:51Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-37709-9_1
ec_funded: 1
file:
- access_level: open_access
checksum: 1a361d83db0244fd32c03b544c294b5a
content_type: application/pdf
creator: dernst
date_created: 2024-01-09T10:01:07Z
date_updated: 2024-01-09T10:01:07Z
file_id: '14765'
file_name: 2023_LNCSCAV_Majumdar.pdf
file_size: 405147
relation: main_file
success: 1
file_date_updated: 2024-01-09T10:01:07Z
has_accepted_license: '1'
intvolume: ' 13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 3-15
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 35th International Conference on Computer Aided Verification
publication_identifier:
eisbn:
- '9783031377099'
eissn:
- 1611-3349
isbn:
- '9783031377082'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14994'
relation: research_data
status: public
scopus_import: '1'
status: public
title: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties
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: 13966
year: '2023'
...
---
_id: '12171'
abstract:
- lang: eng
text: 'We propose an algorithmic approach for synthesizing linear hybrid automata
from time-series data. Unlike existing approaches, our approach provides a whole
family of models with the same discrete structure but different dynamics. Each
model in the family is guaranteed to capture the input data up to a precision
error ε, in the following sense: For each time series, the model contains an execution
that is ε-close to the data points. Our construction allows to effectively choose
a model from this family with minimal precision error ε. We demonstrate the algorithm’s
efficiency and its ability to find precise models in two case studies.'
acknowledgement: This work was supported in part by the European Union’s Horizon 2020
research and innovation programme under the Marie Skłodowska-Curie grant agreement
no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark,
and by the Villum Investigator Grant S4OS.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000-0003-2936-5719
- 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: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata
from time series. In: 20th International Symposium on Automated Technology
for Verification and Analysis. Vol 13505. Springer Nature; 2022:337-353. doi:10.1007/978-3-031-19992-9_22'
apa: 'Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2022). Synthesis of parametric
hybrid automata from time series. In 20th International Symposium on Automated
Technology for Verification and Analysis (Vol. 13505, pp. 337–353). Virtual:
Springer Nature. https://doi.org/10.1007/978-3-031-19992-9_22'
chicago: Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
of Parametric Hybrid Automata from Time Series.” In 20th International Symposium
on Automated Technology for Verification and Analysis, 13505:337–53. Springer
Nature, 2022. https://doi.org/10.1007/978-3-031-19992-9_22.
ieee: M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric
hybrid automata from time series,” in 20th International Symposium on Automated
Technology for Verification and Analysis, Virtual, 2022, vol. 13505, pp. 337–353.
ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid
automata from time series. 20th International Symposium on Automated Technology
for Verification and Analysis. ATVA: Automated Technology for Verification and
Analysis, LNCS, vol. 13505, 337–353.'
mla: Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time
Series.” 20th International Symposium on Automated Technology for Verification
and Analysis, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:10.1007/978-3-031-19992-9_22.
short: M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium
on Automated Technology for Verification and Analysis, Springer Nature, 2022,
pp. 337–353.
conference:
end_date: 2022-10-28
location: Virtual
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2022-10-25
date_created: 2023-01-12T12:11:16Z
date_published: 2022-10-21T00:00:00Z
date_updated: 2023-02-13T09:27:55Z
day: '21'
department:
- _id: ToHe
doi: 10.1007/978-3-031-19992-9_22
ec_funded: 1
external_id:
arxiv:
- '2208.06383'
intvolume: ' 13505'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2208.06383
month: '10'
oa: 1
oa_version: Preprint
page: 337-353
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 20th International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eisbn:
- '9783031199929'
eissn:
- 1611-3349
isbn:
- '9783031199912'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of parametric hybrid automata from time series
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13505
year: '2022'
...
---
_id: '12175'
abstract:
- lang: eng
text: An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic
choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied
this in the context of Timed Automata [9], where it was conjectured that the class
of timed ω-languages recognised by HD-timed automata strictly extends that of
deterministic ones. We provide a proof for this fact.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, the
EPSRC project EP/V025848/1, and the EPSRC project EP/X017796/1.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sougata
full_name: Bose, Sougata
last_name: Bose
- 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: Karoliina
full_name: Lehtinen, Karoliina
last_name: Lehtinen
- first_name: Sven
full_name: Schewe, Sven
last_name: Schewe
- first_name: Patrick
full_name: Totzke, Patrick
last_name: Totzke
citation:
ama: 'Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic
timed automata are not determinizable. In: 16th International Conference on
Reachability Problems. Vol 13608. Springer Nature; 2022:67-76. doi:10.1007/978-3-031-19135-0_5'
apa: 'Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., & Totzke, P. (2022).
History-deterministic timed automata are not determinizable. In 16th International
Conference on Reachability Problems (Vol. 13608, pp. 67–76). Kaiserslautern,
Germany: Springer Nature. https://doi.org/10.1007/978-3-031-19135-0_5'
chicago: Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and
Patrick Totzke. “History-Deterministic Timed Automata Are Not Determinizable.”
In 16th International Conference on Reachability Problems, 13608:67–76.
Springer Nature, 2022. https://doi.org/10.1007/978-3-031-19135-0_5.
ieee: S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic
timed automata are not determinizable,” in 16th International Conference on
Reachability Problems, Kaiserslautern, Germany, 2022, vol. 13608, pp. 67–76.
ista: 'Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2022. History-deterministic
timed automata are not determinizable. 16th International Conference on Reachability
Problems. RC: Reachability Problems, LNCS, vol. 13608, 67–76.'
mla: Bose, Sougata, et al. “History-Deterministic Timed Automata Are Not Determinizable.”
16th International Conference on Reachability Problems, vol. 13608, Springer
Nature, 2022, pp. 67–76, doi:10.1007/978-3-031-19135-0_5.
short: S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, in:, 16th International
Conference on Reachability Problems, Springer Nature, 2022, pp. 67–76.
conference:
end_date: 2022-10-21
location: Kaiserslautern, Germany
name: 'RC: Reachability Problems'
start_date: 2022-10-17
date_created: 2023-01-12T12:11:57Z
date_published: 2022-10-12T00:00:00Z
date_updated: 2023-09-05T15:12:08Z
day: '12'
department:
- _id: ToHe
doi: 10.1007/978-3-031-19135-0_5
ec_funded: 1
intvolume: ' 13608'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://hal.science/hal-03849398/
month: '10'
oa: 1
oa_version: Preprint
page: 67-76
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 16th International Conference on Reachability Problems
publication_identifier:
eisbn:
- '9783031191350'
eissn:
- 1611-3349
isbn:
- '9783031191343'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: History-deterministic timed automata are not determinizable
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13608
year: '2022'
...
---
_id: '12302'
abstract:
- lang: eng
text: 'We propose a novel algorithm to decide the language inclusion between (nondeterministic)
Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage
a notion of quasiorder to prune the search for a counterexample by discarding
candidates which are subsumed by others for the quasiorder. Discarded candidates
are guaranteed to not compromise the completeness of the algorithm. The novelty
of our work lies in the quasiorder used to discard candidates. We introduce FORQs
(family of right quasiorders) that we obtain by adapting the notion of family
of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based
inclusion algorithm which we prove correct and instantiate it for a specific FORQ,
called the structural FORQ, induced by the Büchi automaton to the right of the
inclusion sign. The resulting implementation, called FORKLIFT, scales up better
than the state-of-the-art on a variety of benchmarks including benchmarks from
program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870'
acknowledgement: This work was partially funded by the ESF Investing in your future,
the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00
BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Kyveli
full_name: Doveri, Kyveli
last_name: Doveri
- first_name: Pierre
full_name: Ganty, Pierre
last_name: Ganty
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
citation:
ama: 'Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing.
In: Computer Aided Verification. Vol 13372. Springer Nature; 2022:109-129.
doi:10.1007/978-3-031-13188-2_6'
apa: 'Doveri, K., Ganty, P., & Mazzocchi, N. A. (2022). FORQ-based language
inclusion formal testing. In Computer Aided Verification (Vol. 13372, pp.
109–129). Haifa, Israel: Springer Nature. https://doi.org/10.1007/978-3-031-13188-2_6'
chicago: Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based
Language Inclusion Formal Testing.” In Computer Aided Verification, 13372:109–29.
Springer Nature, 2022. https://doi.org/10.1007/978-3-031-13188-2_6.
ieee: K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal
testing,” in Computer Aided Verification, Haifa, Israel, 2022, vol. 13372,
pp. 109–129.
ista: 'Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal
testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13372, 109–129.'
mla: Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” Computer
Aided Verification, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:10.1007/978-3-031-13188-2_6.
short: K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer
Nature, 2022, pp. 109–129.
conference:
end_date: 2022-08-10
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 2022-08-07
date_created: 2023-01-16T10:06:31Z
date_published: 2022-08-06T00:00:00Z
date_updated: 2023-09-05T15:13:36Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-13188-2_6
ec_funded: 1
external_id:
arxiv:
- '2207.13549'
isi:
- '000870310500006'
file:
- access_level: open_access
checksum: edc363b1be5447a09063e115c247918a
content_type: application/pdf
creator: dernst
date_created: 2023-01-30T12:51:02Z
date_updated: 2023-01-30T12:51:02Z
file_id: '12465'
file_name: 2022_LNCS_Doveri.pdf
file_size: 497682
relation: main_file
success: 1
file_date_updated: 2023-01-30T12:51:02Z
has_accepted_license: '1'
intvolume: ' 13372'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 109-129
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783031131882'
eissn:
- 1611-3349
isbn:
- '9783031131875'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: FORQ-based language inclusion formal testing
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13372
year: '2022'
...
---
_id: '12508'
abstract:
- lang: eng
text: "We explore the notion of history-determinism in the context of timed automata
(TA). History-deterministic automata are those in which nondeterminism can be
resolved on the fly, based on the run constructed thus far. History-determinism
is a robust property that admits different game-based characterisations, and history-deterministic
specifications allow for game-based verification without an expensive determinization
step.\r\nWe show yet another characterisation of history-determinism in terms
of fair simulation, at the general level of labelled transition systems: a system
is history-deterministic precisely if and only if it fairly simulates all language
smaller systems.\r\nFor timed automata over infinite timed words it is known that
universality is undecidable for Büchi TA. We show that for history-deterministic
TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis
all remain decidable and are ExpTime-complete.\r\nFor the subclass of TA with
safety or reachability acceptance, we show that checking whether such an automaton
is history-deterministic is decidable (in ExpTime), and history-deterministic
TA with safety acceptance are effectively determinizable without introducing new
automata states."
acknowledgement: "Thomas A. Henzinger: This work was supported in part by the ERC-2020-AdG
101020093.\r\nPatrick Totzke: acknowledges support from the EPSRC, project no. EP/V025848/1.\r\n"
alternative_title:
- LIPIcs
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Karoliina
full_name: Lehtinen, Karoliina
last_name: Lehtinen
- first_name: Patrick
full_name: Totzke, Patrick
last_name: Totzke
citation:
ama: 'Henzinger TA, Lehtinen K, Totzke P. History-deterministic timed automata.
In: 33rd International Conference on Concurrency Theory. Vol 243. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2022:14:1-14:21. doi:10.4230/LIPIcs.CONCUR.2022.14'
apa: 'Henzinger, T. A., Lehtinen, K., & Totzke, P. (2022). History-deterministic
timed automata. In 33rd International Conference on Concurrency Theory
(Vol. 243, p. 14:1-14:21). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14'
chicago: Henzinger, Thomas A, Karoliina Lehtinen, and Patrick Totzke. “History-Deterministic
Timed Automata.” In 33rd International Conference on Concurrency Theory,
243:14:1-14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14.
ieee: T. A. Henzinger, K. Lehtinen, and P. Totzke, “History-deterministic timed
automata,” in 33rd International Conference on Concurrency Theory, Warsaw,
Poland, 2022, vol. 243, p. 14:1-14:21.
ista: 'Henzinger TA, Lehtinen K, Totzke P. 2022. History-deterministic timed automata.
33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency
Theory, LIPIcs, vol. 243, 14:1-14:21.'
mla: Henzinger, Thomas A., et al. “History-Deterministic Timed Automata.” 33rd
International Conference on Concurrency Theory, vol. 243, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2022, p. 14:1-14:21, doi:10.4230/LIPIcs.CONCUR.2022.14.
short: T.A. Henzinger, K. Lehtinen, P. Totzke, in:, 33rd International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022,
p. 14:1-14:21.
conference:
end_date: 2022-09-16
location: Warsaw, Poland
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2022-09-13
date_created: 2023-02-05T17:24:23Z
date_published: 2022-09-06T00:00:00Z
date_updated: 2023-02-06T09:23:31Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2022.14
ec_funded: 1
file:
- access_level: open_access
checksum: 9e97e15628f66b2ad77f535bb0327dee
content_type: application/pdf
creator: dernst
date_created: 2023-02-06T09:21:09Z
date_updated: 2023-02-06T09:21:09Z
file_id: '12520'
file_name: 2022_LIPICs_Henzinger2.pdf
file_size: 717940
relation: main_file
success: 1
file_date_updated: 2023-02-06T09:21:09Z
has_accepted_license: '1'
intvolume: ' 243'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 14:1-14:21
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 33rd International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959772464'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: History-deterministic timed automata
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: 243
year: '2022'
...
---
_id: '12509'
abstract:
- lang: eng
text: A graph game is a two-player zero-sum game in which the players move a token
throughout a graph to produce an infinite path, which determines the winner or
payoff of the game. In bidding games, both players have budgets, and in each turn,
we hold an "auction" (bidding) to determine which player moves the token. In this
survey, we consider several bidding mechanisms and their effect on the properties
of the game. Specifically, bidding games, and in particular bidding games of infinite
duration, have an intriguing equivalence with random-turn games in which in each
turn, the player who moves is chosen randomly. We summarize how minor changes
in the bidding mechanism lead to unexpected differences in the equivalence with
random-turn games.
acknowledgement: "Guy Avni: Work partially supported by the Israel Science Foundation,
ISF grant agreement\r\nno 1679/21.\r\nThomas A. Henzinger: This work was supported
in part by the ERC-2020-AdG 101020093.\r\nWe would like to thank all our collaborators
Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný,
Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful
for you as it was for us."
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Avni G, Henzinger TA. An updated survey of bidding games on graphs. In: 47th
International Symposium on Mathematical Foundations of Computer Science. Vol
241. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:3:1-3:6. doi:10.4230/LIPIcs.MFCS.2022.3'
apa: 'Avni, G., & Henzinger, T. A. (2022). An updated survey of bidding games
on graphs. In 47th International Symposium on Mathematical Foundations of Computer
Science (Vol. 241, p. 3:1-3:6). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.3'
chicago: 'Avni, Guy, and Thomas A Henzinger. “An Updated Survey of Bidding Games
on Graphs.” In 47th International Symposium on Mathematical Foundations of
Computer Science, 241:3:1-3:6. Leibniz International Proceedings in Informatics
(LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022. https://doi.org/10.4230/LIPIcs.MFCS.2022.3.'
ieee: G. Avni and T. A. Henzinger, “An updated survey of bidding games on graphs,”
in 47th International Symposium on Mathematical Foundations of Computer Science,
Vienna, Austria, 2022, vol. 241, p. 3:1-3:6.
ista: 'Avni G, Henzinger TA. 2022. An updated survey of bidding games on graphs.
47th International Symposium on Mathematical Foundations of Computer Science.
MFCS: Symposium on Mathematical Foundations of Computer ScienceLeibniz International
Proceedings in Informatics (LIPIcs) vol. 241, 3:1-3:6.'
mla: Avni, Guy, and Thomas A. Henzinger. “An Updated Survey of Bidding Games on
Graphs.” 47th International Symposium on Mathematical Foundations of Computer
Science, vol. 241, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022,
p. 3:1-3:6, doi:10.4230/LIPIcs.MFCS.2022.3.
short: G. Avni, T.A. Henzinger, in:, 47th International Symposium on Mathematical
Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
Dagstuhl, Germany, 2022, p. 3:1-3:6.
conference:
end_date: 2022-08-26
location: Vienna, Austria
name: 'MFCS: Symposium on Mathematical Foundations of Computer Science'
start_date: 2022-08-22
date_created: 2023-02-05T17:26:01Z
date_published: 2022-08-22T00:00:00Z
date_updated: 2023-02-06T09:16:54Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2022.3
ec_funded: 1
file:
- access_level: open_access
checksum: 1888ec9421622f9526fbec2de035f132
content_type: application/pdf
creator: dernst
date_created: 2023-02-06T09:13:04Z
date_updated: 2023-02-06T09:13:04Z
file_id: '12519'
file_name: 2022_LIPICs_Avni.pdf
file_size: 624586
relation: main_file
success: 1
file_date_updated: 2023-02-06T09:13:04Z
has_accepted_license: '1'
intvolume: ' 241'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 3:1-3:6
place: Dagstuhl, Germany
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 47th International Symposium on Mathematical Foundations of Computer
Science
publication_identifier:
isbn:
- '9783959772563'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
series_title: Leibniz International Proceedings in Informatics (LIPIcs)
status: public
title: An updated survey of bidding games on graphs
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: 241
year: '2022'
...
---
_id: '12510'
abstract:
- lang: eng
text: "We introduce a new statistical verification algorithm that formally quantifies
the behavioral robustness of any time-continuous process formulated as a continuous-depth
model. Our algorithm solves a set of global optimization (Go) problems over a
given time horizon to construct a tight enclosure (Tube) of the set of all process
executions starting from a ball of initial states. We call our algorithm GoTube.
Through its construction, GoTube ensures that the bounding tube is conservative
up to a desired probability and up to a desired tightness.\r\n GoTube is implemented
in JAX and optimized to scale to complex continuous-depth neural network models.
Compared to advanced reachability analysis tools for time-continuous neural networks,
GoTube does not accumulate overapproximation errors between time steps and avoids
the infamous wrapping effect inherent in symbolic techniques. We show that GoTube
substantially outperforms state-of-the-art verification tools in terms of the
size of the initial ball, speed, time-horizon, task completion, and scalability
on a large set of experiments.\r\n GoTube is stable and sets the state-of-the-art
in terms of its ability to scale to time horizons well beyond what has been previously
possible."
acknowledgement: SG is funded by the Austrian Science Fund (FWF) project number W1255-N23.
ML and TH are supported in part by FWF under grant Z211-N23 (Wittgenstein Award)
and the ERC-2020-AdG 101020093. SS is supported by NSF awards DCL-2040599, CCF-1918225,
and CPS-1446832. RH and DR are partially supported by Boeing. RG is partially supported
by Horizon-2020 ECSEL Project grant No. 783163 (iDev40).
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Sophie A.
full_name: Gruenbacher, Sophie A.
last_name: Gruenbacher
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- 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: Scott A.
full_name: Smolka, Scott A.
last_name: Smolka
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Gruenbacher SA, Lechner M, Hasani R, et al. GoTube: Scalable statistical verification
of continuous-depth models. Proceedings of the AAAI Conference on Artificial
Intelligence. 2022;36(6):6755-6764. doi:10.1609/aaai.v36i6.20631'
apa: 'Gruenbacher, S. A., Lechner, M., Hasani, R., Rus, D., Henzinger, T. A., Smolka,
S. A., & Grosu, R. (2022). GoTube: Scalable statistical verification of continuous-depth
models. Proceedings of the AAAI Conference on Artificial Intelligence.
Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v36i6.20631'
chicago: 'Gruenbacher, Sophie A., Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas
A Henzinger, Scott A. Smolka, and Radu Grosu. “GoTube: Scalable Statistical Verification
of Continuous-Depth Models.” Proceedings of the AAAI Conference on Artificial
Intelligence. Association for the Advancement of Artificial Intelligence,
2022. https://doi.org/10.1609/aaai.v36i6.20631.'
ieee: 'S. A. Gruenbacher et al., “GoTube: Scalable statistical verification
of continuous-depth models,” Proceedings of the AAAI Conference on Artificial
Intelligence, vol. 36, no. 6. Association for the Advancement of Artificial
Intelligence, pp. 6755–6764, 2022.'
ista: 'Gruenbacher SA, Lechner M, Hasani R, Rus D, Henzinger TA, Smolka SA, Grosu
R. 2022. GoTube: Scalable statistical verification of continuous-depth models.
Proceedings of the AAAI Conference on Artificial Intelligence. 36(6), 6755–6764.'
mla: 'Gruenbacher, Sophie A., et al. “GoTube: Scalable Statistical Verification
of Continuous-Depth Models.” Proceedings of the AAAI Conference on Artificial
Intelligence, vol. 36, no. 6, Association for the Advancement of Artificial
Intelligence, 2022, pp. 6755–64, doi:10.1609/aaai.v36i6.20631.'
short: S.A. Gruenbacher, M. Lechner, R. Hasani, D. Rus, T.A. Henzinger, S.A. Smolka,
R. Grosu, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022)
6755–6764.
date_created: 2023-02-05T17:27:42Z
date_published: 2022-06-28T00:00:00Z
date_updated: 2023-09-26T10:46:59Z
day: '28'
department:
- _id: ToHe
doi: 10.1609/aaai.v36i6.20631
ec_funded: 1
external_id:
arxiv:
- '2107.08467'
intvolume: ' 36'
issue: '6'
keyword:
- General Medicine
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2107.08467
month: '06'
oa: 1
oa_version: Preprint
page: 6755-6764
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '978577358350'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'GoTube: Scalable statistical verification of continuous-depth models'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 36
year: '2022'
...
---
_id: '12511'
abstract:
- lang: eng
text: "We consider the problem of formally verifying almost-sure (a.s.) asymptotic
stability in discrete-time nonlinear stochastic control systems. While verifying
stability in deterministic control systems is extensively studied in the literature,
verifying stability in stochastic control systems is an open problem. The few
existing works on this topic either consider only specialized forms of stochasticity
or make restrictive assumptions on the system, rendering them inapplicable to
learning algorithms with neural network policies. \r\n In this work, we present
an approach for general nonlinear stochastic control problems with two novel aspects:
(a) instead of classical stochastic extensions of Lyapunov functions, we use ranking
supermartingales (RSMs) to certify a.s. asymptotic stability, and (b) we present
a method for learning neural network RSMs. \r\n We prove that our approach guarantees
a.s. asymptotic stability of the system and\r\n provides the first method to obtain
bounds on the stabilization time, which stochastic Lyapunov functions do not.\r\n
Finally, we validate our approach experimentally on a set of nonlinear stochastic
reinforcement learning environments with neural network policies."
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme\r\nunder the Marie Skłodowska-Curie Grant Agreement No. 665385."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Lechner M, Zikelic D, Chatterjee K, Henzinger TA. Stability verification in
stochastic control systems via neural network supermartingales. Proceedings
of the AAAI Conference on Artificial Intelligence. 2022;36(7):7326-7336. doi:10.1609/aaai.v36i7.20695
apa: Lechner, M., Zikelic, D., Chatterjee, K., & Henzinger, T. A. (2022). Stability
verification in stochastic control systems via neural network supermartingales.
Proceedings of the AAAI Conference on Artificial Intelligence. Association
for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v36i7.20695
chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A Henzinger.
“Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.”
Proceedings of the AAAI Conference on Artificial Intelligence. Association
for the Advancement of Artificial Intelligence, 2022. https://doi.org/10.1609/aaai.v36i7.20695.
ieee: M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger, “Stability verification
in stochastic control systems via neural network supermartingales,” Proceedings
of the AAAI Conference on Artificial Intelligence, vol. 36, no. 7. Association
for the Advancement of Artificial Intelligence, pp. 7326–7336, 2022.
ista: Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification
in stochastic control systems via neural network supermartingales. Proceedings
of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336.
mla: Lechner, Mathias, et al. “Stability Verification in Stochastic Control Systems
via Neural Network Supermartingales.” Proceedings of the AAAI Conference on
Artificial Intelligence, vol. 36, no. 7, Association for the Advancement of
Artificial Intelligence, 2022, pp. 7326–36, doi:10.1609/aaai.v36i7.20695.
short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, Proceedings of the
AAAI Conference on Artificial Intelligence 36 (2022) 7326–7336.
date_created: 2023-02-05T17:29:50Z
date_published: 2022-06-28T00:00:00Z
date_updated: 2025-07-14T09:09:58Z
day: '28'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v36i7.20695
ec_funded: 1
external_id:
arxiv:
- '2112.09495'
intvolume: ' 36'
issue: '7'
keyword:
- General Medicine
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2112.09495
month: '06'
oa: 1
oa_version: Preprint
page: 7326-7336
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '9781577358350'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Stability verification in stochastic control systems via neural network supermartingales
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 36
year: '2022'
...
---
_id: '14600'
abstract:
- lang: eng
text: We study the problem of learning controllers for discrete-time non-linear
stochastic dynamical systems with formal reach-avoid guarantees. This work presents
the first method for providing formal reach-avoid guarantees, which combine and
generalize stability and safety guarantees, with a tolerable probability threshold
$p\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine
learning literature and it represents formal certificates as neural networks.
In particular, we learn a certificate in the form of a reach-avoid supermartingale
(RASM), a novel notion that we introduce in this work. Our RASMs provide reachability
and avoidance guarantees by imposing constraints on what can be viewed as a stochastic
extension of level sets of Lyapunov functions for deterministic systems. Our approach
solves several important problems -- it can be used to learn a control policy
from scratch, to verify a reach-avoid specification for a fixed control policy,
or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification.
We validate our approach on $3$ stochastic non-linear reinforcement learning tasks.
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- 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: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv. doi:10.48550/ARXIV.2210.05308
apa: Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (n.d.). Learning
control policies for stochastic systems with reach-avoid guarantees. arXiv.
https://doi.org/10.48550/ARXIV.2210.05308
chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee.
“Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.”
ArXiv, n.d. https://doi.org/10.48550/ARXIV.2210.05308.
ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control
policies for stochastic systems with reach-avoid guarantees,” arXiv. .
ista: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv, 10.48550/ARXIV.2210.05308.
mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with
Reach-Avoid Guarantees.” ArXiv, doi:10.48550/ARXIV.2210.05308.
short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).
date_created: 2023-11-24T13:10:09Z
date_published: 2022-11-29T00:00:00Z
date_updated: 2025-07-14T09:10:02Z
day: '29'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/ARXIV.2210.05308
ec_funded: 1
external_id:
arxiv:
- '2210.05308'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2210.05308
month: '11'
oa: 1
oa_version: Preprint
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
- id: '14830'
relation: later_version
status: public
status: public
title: Learning control policies for stochastic systems with reach-avoid guarantees
tmp:
image: /images/cc_by_sa.png
legal_code_url: https://creativecommons.org/licenses/by-sa/4.0/legalcode
name: Creative Commons Attribution-ShareAlike 4.0 International Public License (CC
BY-SA 4.0)
short: CC BY-SA (4.0)
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '14601'
abstract:
- lang: eng
text: "In this work, we address the problem of learning provably stable neural\r\nnetwork
policies for stochastic control systems. While recent work has\r\ndemonstrated
the feasibility of certifying given policies using martingale\r\ntheory, the problem
of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness
of jointly learning a policy together with a martingale\r\ncertificate that proves
its stability using a single learning algorithm. We\r\nobserve that the joint
optimization problem becomes easily stuck in local\r\nminima when starting from
a randomly initialized policy. Our results suggest\r\nthat some form of pre-training
of the policy is required for the joint\r\noptimization to repair and verify the
policy successfully."
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv. doi:10.48550/arXiv.2205.11991
apa: Zikelic, D., Lechner, M., Chatterjee, K., & Henzinger, T. A. (n.d.). Learning
stabilizing policies in stochastic control systems. arXiv. https://doi.org/10.48550/arXiv.2205.11991
chicago: Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger.
“Learning Stabilizing Policies in Stochastic Control Systems.” ArXiv, n.d.
https://doi.org/10.48550/arXiv.2205.11991.
ieee: D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing
policies in stochastic control systems,” arXiv. .
ista: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv, 10.48550/arXiv.2205.11991.
mla: Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control
Systems.” ArXiv, doi:10.48550/arXiv.2205.11991.
short: D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).
date_created: 2023-11-24T13:22:30Z
date_published: 2022-05-24T00:00:00Z
date_updated: 2025-07-14T09:10:00Z
day: '24'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/arXiv.2205.11991
ec_funded: 1
external_id:
arxiv:
- '2205.11991'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2205.11991
month: '05'
oa: 1
oa_version: Preprint
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
status: public
title: Learning stabilizing policies in stochastic control systems
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '10774'
abstract:
- lang: eng
text: We study the problem of specifying sequential information-flow properties
of systems. Information-flow properties are hyperproperties, as they compare different
traces of a system. Sequential information-flow properties can express changes,
over time, in the information-flow constraints. For example, information-flow
constraints during an initialization phase of a system may be different from information-flow
constraints that are required during the operation phase. We formalize several
variants of interpreting sequential information-flow constraints, which arise
from different assumptions about what can be observed of the system. For this
purpose, we introduce a first-order logic, called Hypertrace Logic, with both
trace and time quantifiers for specifying linear-time hyperproperties. We prove
that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted
quantifier prefixes, cannot specify the majority of the studied variants of sequential
information flow, including all variants in which the transition between sequential
phases (such as initialization and operation) happens asynchronously. Our results
rely on new equivalences between sets of traces that cannot be distinguished by
certain classes of formulas from Hypertrace Logic. This presents a new approach
to proving inexpressiveness results for HyperLTL.
acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of
the Austrian Science Fund (FWF) and by the FWF project W1255-N23.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential
information flow. In: Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Flavors of sequential information flow,” in Lecture Notes in Computer Science
(including subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp.
1–19.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors
of sequential information flow. Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182,
1–19.'
mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp.
1–19, doi:10.1007/978-3-030-94583-1_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp.
1–19.
conference:
end_date: 2022-01-18
location: Philadelphia, PA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2022-01-16
date_created: 2022-02-20T23:01:34Z
date_published: 2022-01-14T00:00:00Z
date_updated: 2022-08-05T09:02:56Z
day: '14'
department:
- _id: ToHe
doi: 10.1007/978-3-030-94583-1_1
external_id:
arxiv:
- '2105.02013'
intvolume: ' 13182'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2105.02013'
month: '01'
oa: 1
oa_version: Preprint
page: 1-19
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030945824'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of sequential information flow
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13182
year: '2022'
...