---
_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: '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: '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: '14920'
abstract:
- lang: eng
text: "We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular
winning conditions, where the environment is constrained by a strong transition
fairness assumption. Strong transition fairness is a widely occurring special
case of strong fairness, which requires that any execution is strongly fair with
respect to a specified set of live edges: whenever the\r\nsource vertex of a live
edge is visited infinitely often along a play, the edge itself is traversed infinitely
often along the play as well. We show that, surprisingly, strong transition fairness
retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular
games -- the new algorithms have the same alternation depth as the classical algorithms
but invoke a new type of predecessor operator. For Rabin games with $k$ pairs,
the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is
independent of the number of live edges in the strong transition fairness assumption.
Further, we show that GR(1) specifications with strong transition fairness assumptions
can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm.
In contrast, strong fairness necessarily requires increasing the alternation depth
depending on the number of fairness assumptions. We get symbolic algorithms for
(generalized) Rabin, parity and GR(1) objectives under strong transition fairness
assumptions as well as a direct symbolic algorithm for qualitative winning in
stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps,
improving the state of the art. Finally, we have implemented a BDD-based synthesis
engine based on our algorithm. We show on a set of synthetic and real benchmarks
that our algorithm is scalable, parallelizable, and outperforms previous algorithms
by orders of magnitude."
acknowledgement: A previous version of this paper has appeared in TACAS 2022. Authors
ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research
was conducted. 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.
article_number: '4'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Tamajit
full_name: Banerjee, Tamajit
last_name: Banerjee
- 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: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms
for mega-regular games under strong transition fairness. TheoretiCS. 2023;2.
doi:10.46298/theoretics.23.4
apa: Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., & Soudjani, S.
(2023). Fast symbolic algorithms for mega-regular games under strong transition
fairness. TheoretiCS. EPI Sciences. https://doi.org/10.46298/theoretics.23.4
chicago: Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck,
and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong
Transition Fairness.” TheoretiCS. EPI Sciences, 2023. https://doi.org/10.46298/theoretics.23.4.
ieee: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast
symbolic algorithms for mega-regular games under strong transition fairness,”
TheoretiCS, vol. 2. EPI Sciences, 2023.
ista: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic
algorithms for mega-regular games under strong transition fairness. TheoretiCS.
2, 4.
mla: Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games
under Strong Transition Fairness.” TheoretiCS, vol. 2, 4, EPI Sciences,
2023, doi:10.46298/theoretics.23.4.
short: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS
2 (2023).
date_created: 2024-01-31T13:40:49Z
date_published: 2023-02-24T00:00:00Z
date_updated: 2024-02-05T10:21:51Z
day: '24'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.46298/theoretics.23.4
ec_funded: 1
external_id:
arxiv:
- '2202.07480'
file:
- access_level: open_access
checksum: 2972d531122a6f15727b396110fb3f5c
content_type: application/pdf
creator: dernst
date_created: 2024-02-05T10:19:35Z
date_updated: 2024-02-05T10:19:35Z
file_id: '14940'
file_name: 2023_TheoretiCS_Banerjee.pdf
file_size: 917076
relation: main_file
success: 1
file_date_updated: 2024-02-05T10:19:35Z
has_accepted_license: '1'
intvolume: ' 2'
language:
- iso: eng
month: '02'
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: TheoretiCS
publication_identifier:
issn:
- 2751-4838
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
status: public
title: Fast symbolic algorithms for mega-regular games under strong transition fairness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2023'
...
---
_id: '14994'
abstract:
- lang: eng
text: This resource contains the artifacts for reproducing the experimental results
presented in the paper titled "A Flexible Toolchain for Symbolic Rabin Games under
Fair and Stochastic Uncertainties" that has been submitted in CAV 2023.
article_processing_charge: No
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. 2023. doi:10.5281/ZENODO.7877790
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. Zenodo. https://doi.org/10.5281/ZENODO.7877790
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.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.7877790.
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.” Zenodo,
2023.
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, Zenodo,
10.5281/ZENODO.7877790.
mla: Majumdar, Rupak, et al. A Flexible Toolchain for Symbolic Rabin Games under
Fair and Stochastic Uncertainties. Zenodo, 2023, doi:10.5281/ZENODO.7877790.
short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).
date_created: 2024-02-14T15:13:00Z
date_published: 2023-04-28T00:00:00Z
date_updated: 2024-02-27T07:39:51Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.5281/ZENODO.7877790
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/zenodo.7877790
month: '04'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '14758'
relation: used_in_publication
status: public
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: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '13141'
abstract:
- lang: eng
text: "We automatically compute a new class of environment assumptions in two-player
turn-based finite graph games which characterize an “adequate cooperation” needed
from the environment to allow the system player to win. Given an ω-regular winning
condition Φ for the system player, we compute an ω-regular assumption Ψ for the
environment player, such that (i) every environment strategy compliant with Ψ
allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the
environment for every strategy of the system (implementability), and (iii) Ψ does
not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games,
which are canonical representations of ω-regular games, we present a polynomial-time
algorithm for the symbolic computation of adequately permissive assumptions and
show that our algorithm runs faster and produces better assumptions than existing
approaches—both theoretically and empirically. To the best of our knowledge, for
ω\r\n-regular games, we provide the first algorithm to compute sufficient and
implementable environment assumptions that are also permissive."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ashwani
full_name: Anand, Ashwani
last_name: Anand
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Satya Prakash
full_name: Nayak, Satya Prakash
last_name: Nayak
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
citation:
ama: 'Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions
for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and
Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15'
apa: 'Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing
adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15'
chicago: 'Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin
Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.'
ieee: 'A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately
permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994,
pp. 211–228.'
ista: 'Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive
assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 13994, 211–228.'
mla: 'Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.'
short: 'A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and
Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023,
pp. 211–228.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-06-19T08:49:46Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_15
file:
- access_level: open_access
checksum: 60dcafc1b4f6f070be43bad3fe877974
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:43:21Z
date_updated: 2023-06-19T08:43:21Z
file_id: '13151'
file_name: 2023_LNCS_Anand.pdf
file_size: 521425
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:43:21Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 211-228
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing adequately permissive assumptions for synthesis
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: 13994
year: '2023'
...
---
_id: '13228'
abstract:
- lang: eng
text: A machine-learned system that is fair in static decision-making tasks may
have biased societal impacts in the long-run. This may happen when the system
interacts with humans and feedback patterns emerge, reinforcing old biases in
the system and creating new biases. While existing works try to identify and mitigate
long-run biases through smart system design, we introduce techniques for monitoring
fairness in real time. Our goal is to build and deploy a monitor that will continuously
observe a long sequence of events generated by the system in the wild, and will
output, with each event, a verdict on how fair the system is at the current point
in time. The advantages of monitoring are two-fold. Firstly, fairness is evaluated
at run-time, which is important because unfair behaviors may not be eliminated
a priori, at design-time, due to partial knowledge about the system and the environment,
as well as uncertainties and dynamic changes in the system and the environment,
such as the unpredictability of human behavior. Secondly, monitors are by design
oblivious to how the monitored system is constructed, which makes them suitable
to be used as trusted third-party fairness watchdogs. They function as computationally
lightweight statistical estimators, and their correctness proofs rely on the rigorous
analysis of the stochastic process that models the assumptions about the underlying
dynamics of the system. We show, both in theory and experiments, how monitors
can warn us (1) if a bank’s credit policy over time has created an unfair distribution
of credit scores among the population, and (2) if a resource allocator’s allocation
policy over time has made unfair allocations. Our experiments demonstrate that
the monitors introduce very low overhead. We believe that runtime monitoring is
an important and mathematically rigorous new addition to the fairness toolbox.
acknowledgement: 'The authors would like to thank the anonymous reviewers for their
valuable comments and helpful suggestions. This work is supported by the European
Research Council under Grant No.: ERC-2020-AdG 101020093.'
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: Mahyar
full_name: Karimi, Mahyar
last_name: Karimi
- 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, Karimi M, Kueffner K, Mallik K. Runtime monitoring of dynamic
fairness properties. In: FAccT ’23: Proceedings of the 2023 ACM Conference
on Fairness, Accountability, and Transparency. Association for Computing Machinery;
2023:604-614. doi:10.1145/3593013.3594028'
apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Runtime
monitoring of dynamic fairness properties. In FAccT ’23: Proceedings of the
2023 ACM Conference on Fairness, Accountability, and Transparency (pp. 604–614).
Chicago, IL, United States: Association for Computing Machinery. https://doi.org/10.1145/3593013.3594028'
chicago: 'Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik.
“Runtime Monitoring of Dynamic Fairness Properties.” In FAccT ’23: Proceedings
of the 2023 ACM Conference on Fairness, Accountability, and Transparency,
604–14. Association for Computing Machinery, 2023. https://doi.org/10.1145/3593013.3594028.'
ieee: 'T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Runtime monitoring
of dynamic fairness properties,” in FAccT ’23: Proceedings of the 2023 ACM
Conference on Fairness, Accountability, and Transparency, Chicago, IL, United
States, 2023, pp. 604–614.'
ista: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Runtime monitoring of
dynamic fairness properties. FAccT ’23: Proceedings of the 2023 ACM Conference
on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness,
Accountability and Transparency, 604–614.'
mla: 'Henzinger, Thomas A., et al. “Runtime Monitoring of Dynamic Fairness Properties.”
FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability,
and Transparency, Association for Computing Machinery, 2023, pp. 604–14, doi:10.1145/3593013.3594028.'
short: 'T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, FAccT ’23: Proceedings
of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Association
for Computing Machinery, 2023, pp. 604–614.'
conference:
end_date: 2023-06-15
location: Chicago, IL, United States
name: 'FAccT: Conference on Fairness, Accountability and Transparency'
start_date: 2023-06-12
date_created: 2023-07-16T22:01:09Z
date_published: 2023-06-12T00:00:00Z
date_updated: 2023-12-13T11:30:31Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3593013.3594028
ec_funded: 1
external_id:
arxiv:
- '2305.04699'
isi:
- '001062819300057'
file:
- access_level: open_access
checksum: 96c759db9cdf94b81e37871a66a6ff48
content_type: application/pdf
creator: dernst
date_created: 2023-07-18T07:43:10Z
date_updated: 2023-07-18T07:43:10Z
file_id: '13245'
file_name: 2023_ACM_HenzingerT.pdf
file_size: 4100596
relation: main_file
success: 1
file_date_updated: 2023-07-18T07:43:10Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 604-614
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 'FAccT ''23: Proceedings of the 2023 ACM Conference on Fairness, Accountability,
and Transparency'
publication_identifier:
isbn:
- '9781450372527'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Runtime monitoring of dynamic fairness properties
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: '13310'
abstract:
- lang: eng
text: Machine-learned systems are in widespread use for making decisions about humans,
and it is important that they are fair, i.e., not biased against individuals based
on sensitive attributes. We present runtime verification of algorithmic fairness
for systems whose models are unknown, but are assumed to have a Markov chain structure.
We introduce a specification language that can model many common algorithmic fairness
properties, such as demographic parity, equal opportunity, and social burden.
We build monitors that observe a long sequence of events as generated by a given
system, and output, after each observation, a quantitative estimate of how fair
or biased the system was on that run until that point in time. The estimate is
proven to be correct modulo a variable error bound and a given confidence level,
where the error bound gets tighter as the observed sequence gets longer. Our monitors
are of two types, and use, respectively, frequentist and Bayesian statistical
inference techniques. While the frequentist monitors compute estimates that are
objectively correct with respect to the ground truth, the Bayesian monitors compute
estimates that are correct subject to a given prior belief about the system’s
model. Using a prototype implementation, we show how we can monitor if a bank
is fair in giving loans to applicants from different social backgrounds, and if
a college is fair in admitting students while maintaining a reasonable financial
burden on the society. Although they exhibit different theoretical complexities
in certain cases, in our experiments, both frequentist and Bayesian monitors took
less than a millisecond to update their verdicts after each observation.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG101020093.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
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: Mahyar
full_name: Karimi, Mahyar
id: f1dedef5-2f78-11ee-989a-c4c97bccf506
last_name: Karimi
orcid: 0009-0005-0820-1696
- 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, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness.
In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382.
doi:10.1007/978-3-031-37703-7_17'
apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Monitoring
algorithmic fairness. In Computer Aided Verification (Vol. 13965, pp. 358–382).
Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37703-7_17'
chicago: Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik.
“Monitoring Algorithmic Fairness.” In Computer Aided Verification, 13965:358–382.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37703-7_17.
ieee: T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic
fairness,” in Computer Aided Verification, Paris, France, 2023, vol. 13965,
pp. 358–382.
ista: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic
fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13965, 358–382.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” Computer
Aided Verification, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:10.1007/978-3-031-37703-7_17.
short: T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification,
Springer Nature, 2023, pp. 358–382.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-07-25T18:32:40Z
date_published: 2023-07-18T00:00:00Z
date_updated: 2023-09-05T15:14:00Z
day: '18'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-37703-7_17
ec_funded: 1
external_id:
arxiv:
- '2305.15979'
file:
- access_level: open_access
checksum: ccaf94bf7d658ba012c016e11869b54c
content_type: application/pdf
creator: dernst
date_created: 2023-07-31T08:11:20Z
date_updated: 2023-07-31T08:11:20Z
file_id: '13327'
file_name: 2023_LNCS_CAV_HenzingerT.pdf
file_size: 647760
relation: main_file
success: 1
file_date_updated: 2023-07-31T08:11:20Z
has_accepted_license: '1'
intvolume: ' 13965'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 358–382
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:
- '9783031377037'
eissn:
- 1611-3349
isbn:
- '9783031377020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring algorithmic fairness
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: 13965
year: '2023'
...
---
_id: '12529'
abstract:
- lang: eng
text: "We consider turn-based stochastic 2-player games on graphs with ω-regular
winning conditions. We provide a direct symbolic algorithm for solving such games
when the winning condition is formulated as a Rabin condition. For a stochastic
Rabin game with k pairs over a game graph with n vertices, our algorithm runs
in O(nk+2k!) symbolic steps, which improves the state of the art.\r\nWe have implemented
our symbolic algorithm, along with performance optimizations including parallellization
and acceleration, in a BDD-based synthesis tool called Fairsyn. We demonstrate
the superiority of Fairsyn compared to the state of the art on a set of synthetic
benchmarks derived from the VLTS benchmark suite and on a control system benchmark
from the literature. In our experiments, Fairsyn performed significantly faster
with up to two orders of magnitude improvement in computation time."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tamajit
full_name: Banerjee, Tamajit
last_name: Banerjee
- 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: 'Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. A direct symbolic
algorithm for solving stochastic rabin games. In: 28th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems. Vol
13244. Springer Nature; 2022:81-98. doi:10.1007/978-3-030-99527-0_5'
apa: 'Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., & Soudjani, S.
(2022). A direct symbolic algorithm for solving stochastic rabin games. In 28th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13244, pp. 81–98). Munich, Germany: Springer Nature. https://doi.org/10.1007/978-3-030-99527-0_5'
chicago: Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck,
and Sadegh Soudjani. “A Direct Symbolic Algorithm for Solving Stochastic Rabin
Games.” In 28th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 13244:81–98. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-99527-0_5.
ieee: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “A direct
symbolic algorithm for solving stochastic rabin games,” in 28th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Munich, Germany, 2022, vol. 13244, pp. 81–98.
ista: 'Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2022. A direct
symbolic algorithm for solving stochastic rabin games. 28th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13244,
81–98.'
mla: Banerjee, Tamajit, et al. “A Direct Symbolic Algorithm for Solving Stochastic
Rabin Games.” 28th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, vol. 13244, Springer Nature, 2022, pp.
81–98, doi:10.1007/978-3-030-99527-0_5.
short: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, in:, 28th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Springer Nature, 2022, pp. 81–98.
conference:
end_date: 2022-04-07
location: Munich, Germany
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2022-04-02
date_created: 2023-02-08T11:43:34Z
date_published: 2022-03-29T00:00:00Z
date_updated: 2023-02-09T08:58:48Z
day: '29'
doi: 10.1007/978-3-030-99527-0_5
extern: '1'
intvolume: ' 13244'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/978-3-030-99527-0_5
month: '03'
oa: 1
oa_version: Published Version
page: 81-98
publication: 28th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eisbn:
- '9783030995270'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: A direct symbolic algorithm for solving stochastic rabin games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13244
year: '2022'
...
---
_id: '12530'
abstract:
- lang: eng
text: We present BOCoSy, a tool for Bounded symbolic Output-feedback Controller
Synthesis. Given a specification, BOCoSy synthesizes symbolic output-feedback
controllers which interact with a given plant via a pre-defined finite symbolic
interface. BOCoSy solves this problem by a new lazy abstraction-refinement technique
which starts with a very coarse abstraction of the external trace semantics of
the given plant and iteratively removes non-admissible behavior from this abstract
model until a controller is found. BOCoSy steers the search for controllers towards
small and concise state space representations by utilizing ideas from bounded
synthesis. As a result, BOCoSy returns small and explainable controllers that
are still powerful enough to solve the given synthesis problem. We show that BOCoSy
is able to synthesize small, human readable symbolic controllers quickly on a
set of benchmarks.
article_processing_charge: No
author:
- first_name: Bernd
full_name: Finkbeiner, Bernd
last_name: Finkbeiner
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Noemi
full_name: Passing, Noemi
last_name: Passing
- first_name: Malte
full_name: Schledjewski, Malte
last_name: Schledjewski
- first_name: Anne-Kathrin
full_name: Schmuck, Anne-Kathrin
last_name: Schmuck
citation:
ama: 'Finkbeiner B, Mallik K, Passing N, Schledjewski M, Schmuck A-K. BOCoSy: Small
but powerful symbolic output-feedback control. In: 25th ACM International Conference
on Hybrid Systems: Computation and Control. ACM; 2022:24:1-24:11. doi:10.1145/3501710.3519535'
apa: 'Finkbeiner, B., Mallik, K., Passing, N., Schledjewski, M., & Schmuck,
A.-K. (2022). BOCoSy: Small but powerful symbolic output-feedback control. In
25th ACM International Conference on Hybrid Systems: Computation and Control
(p. 24:1-24:11). Milan, Italy: ACM. https://doi.org/10.1145/3501710.3519535'
chicago: 'Finkbeiner, Bernd, Kaushik Mallik, Noemi Passing, Malte Schledjewski,
and Anne-Kathrin Schmuck. “BOCoSy: Small but Powerful Symbolic Output-Feedback
Control.” In 25th ACM International Conference on Hybrid Systems: Computation
and Control, 24:1-24:11. ACM, 2022. https://doi.org/10.1145/3501710.3519535.'
ieee: 'B. Finkbeiner, K. Mallik, N. Passing, M. Schledjewski, and A.-K. Schmuck,
“BOCoSy: Small but powerful symbolic output-feedback control,” in 25th ACM
International Conference on Hybrid Systems: Computation and Control, Milan,
Italy, 2022, p. 24:1-24:11.'
ista: 'Finkbeiner B, Mallik K, Passing N, Schledjewski M, Schmuck A-K. 2022. BOCoSy:
Small but powerful symbolic output-feedback control. 25th ACM International Conference
on Hybrid Systems: Computation and Control. HSCC: International Conference on
Hybrid Systems Computation and Control, 24:1-24:11.'
mla: 'Finkbeiner, Bernd, et al. “BOCoSy: Small but Powerful Symbolic Output-Feedback
Control.” 25th ACM International Conference on Hybrid Systems: Computation
and Control, ACM, 2022, p. 24:1-24:11, doi:10.1145/3501710.3519535.'
short: 'B. Finkbeiner, K. Mallik, N. Passing, M. Schledjewski, A.-K. Schmuck, in:,
25th ACM International Conference on Hybrid Systems: Computation and Control,
ACM, 2022, p. 24:1-24:11.'
conference:
end_date: 2022-05-06
location: Milan, Italy
name: 'HSCC: International Conference on Hybrid Systems Computation and Control'
start_date: 2022-05-04
date_created: 2023-02-08T11:43:50Z
date_published: 2022-05-01T00:00:00Z
date_updated: 2023-02-09T08:53:13Z
day: '01'
doi: 10.1145/3501710.3519535
extern: '1'
language:
- iso: eng
month: '05'
oa_version: None
page: 24:1-24:11
publication: '25th ACM International Conference on Hybrid Systems: Computation and
Control'
publication_identifier:
isbn:
- '9781450391962'
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BOCoSy: Small but powerful symbolic output-feedback control'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...