---
_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: '12854'
abstract:
- lang: eng
text: "The main idea behind BUBAAK is to run multiple program analyses in parallel
and use runtime monitoring and enforcement to observe and control their progress
in real time. The analyses send information about (un)explored states of the program
and discovered invariants to a monitor. The monitor processes the received data
and can force an analysis to stop the search of certain program parts (which have
already been analyzed by other analyses), or to make it utilize a program invariant
found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange
between the monitor and the analyses was not yet completed, which is why BUBAAK
only ran several analyses in parallel, without any coordination. Still, BUBAAK
won the meta-category FalsificationOverall and placed very well in several other
(sub)-categories of the competition."
acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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: 'Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of
program verifiers. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32'
chicago: 'Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of
Program Verifiers.” In Tools and Algorithms for the Construction and Analysis
of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.'
ieee: 'M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,”
in Tools and Algorithms for the Construction and Analysis of Systems, Paris,
France, 2023, vol. 13994, pp. 535–540.'
ista: 'Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers.
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994,
535–540.'
mla: 'Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program
Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.'
short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 535–540.
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-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:02:43Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
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'
...