---
_id: '141'
abstract:
- lang: eng
text: 'Given a model and a specification, the fundamental model-checking problem
asks for algorithmic verification of whether the model satisfies the specification.
We consider graphs and Markov decision processes (MDPs), which are fundamental
models for reactive systems. One of the very basic specifications that arise in
verification of reactive systems is the strong fairness (aka Streett) objective.
Given different types of requests and corresponding grants, the objective requires
that for each type, if the request event happens infinitely often, then the corresponding
grant event must also happen infinitely often. All ω -regular objectives can be
expressed as Streett objectives and hence they are canonical in verification.
To handle the state-space explosion, symbolic algorithms are required that operate
on a succinct implicit representation of the system rather than explicitly accessing
the system. While explicit algorithms for graphs and MDPs with Streett objectives
have been widely studied, there has been no improvement of the basic symbolic
algorithms. The worst-case numbers of symbolic steps required for the basic symbolic
algorithms are as follows: quadratic for graphs and cubic for MDPs. In this work
we present the first sub-quadratic symbolic algorithm for graphs with Streett
objectives, and our algorithm is sub-quadratic even for MDPs. Based on our algorithmic
insights we present an implementation of the new symbolic approach and show that
it improves the existing approach on several academic benchmark examples.'
acknowledgement: 'Acknowledgements. K. C. and M. H. are partially supported by the
Vienna Science and Technology Fund (WWTF) grant ICT15-003. K. C. is partially supported
by the Austrian Science Fund (FWF): S11407-N23 (RiSE/SHiNE), and an ERC Start Grant
(279307: Graph Games). V. T. is partially supported by the European Union’s Horizon
2020 research and innovation programme under the Marie Sk lodowska-Curie Grant Agreement
No. 665385.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
- first_name: Simin
full_name: Oraee, Simin
last_name: Oraee
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Chatterjee K, Henzinger MH, Loitzenbauer V, Oraee S, Toman V. Symbolic algorithms
for graphs and Markov decision processes with fairness objectives. In: Vol 10982.
Springer; 2018:178-197. doi:10.1007/978-3-319-96142-2_13'
apa: 'Chatterjee, K., Henzinger, M. H., Loitzenbauer, V., Oraee, S., & Toman,
V. (2018). Symbolic algorithms for graphs and Markov decision processes with fairness
objectives (Vol. 10982, pp. 178–197). Presented at the CAV: Computer Aided Verification,
Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96142-2_13'
chicago: Chatterjee, Krishnendu, Monika H Henzinger, Veronika Loitzenbauer, Simin
Oraee, and Viktor Toman. “Symbolic Algorithms for Graphs and Markov Decision Processes
with Fairness Objectives,” 10982:178–97. Springer, 2018. https://doi.org/10.1007/978-3-319-96142-2_13.
ieee: 'K. Chatterjee, M. H. Henzinger, V. Loitzenbauer, S. Oraee, and V. Toman,
“Symbolic algorithms for graphs and Markov decision processes with fairness objectives,”
presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018,
vol. 10982, pp. 178–197.'
ista: 'Chatterjee K, Henzinger MH, Loitzenbauer V, Oraee S, Toman V. 2018. Symbolic
algorithms for graphs and Markov decision processes with fairness objectives.
CAV: Computer Aided Verification, LNCS, vol. 10982, 178–197.'
mla: Chatterjee, Krishnendu, et al. Symbolic Algorithms for Graphs and Markov
Decision Processes with Fairness Objectives. Vol. 10982, Springer, 2018, pp.
178–97, doi:10.1007/978-3-319-96142-2_13.
short: K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, S. Oraee, V. Toman, in:,
Springer, 2018, pp. 178–197.
conference:
end_date: 2018-07-17
location: Oxford, United Kingdom
name: 'CAV: Computer Aided Verification'
start_date: 2018-07-14
date_created: 2018-12-11T11:44:51Z
date_published: 2018-07-18T00:00:00Z
date_updated: 2023-09-19T09:59:55Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-319-96142-2_13
ec_funded: 1
external_id:
isi:
- '000491469700013'
file:
- access_level: open_access
checksum: 1a6ffa4febe8bb8ac28be3adb3eafebc
content_type: application/pdf
creator: dernst
date_created: 2018-12-18T08:52:38Z
date_updated: 2020-07-14T12:44:53Z
file_id: '5737'
file_name: 2018_LNCS_Chatterjee.pdf
file_size: 675606
relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: ' 10982'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '07'
oa: 1
oa_version: Published Version
page: 178-197
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication_status: published
publisher: Springer
publist_id: '7782'
quality_controlled: '1'
related_material:
record:
- id: '10199'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Symbolic algorithms for graphs and Markov decision processes with fairness
objectives
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: 10982
year: '2018'
...