---
_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
corr_author: '1'
date_created: 2024-01-08T13:18:00Z
date_published: 2023-07-16T00:00:00Z
date_updated: 2025-09-09T14:16:49Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-37709-9_1
ec_funded: 1
external_id:
isi:
- '001310805600001'
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'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13966
year: '2023'
...