---
_id: '10877'
abstract:
- lang: eng
  text: 'This report presents the results of a friendly competition for formal verification
    of continuous and hybrid systems with piecewise constant dynamics. The friendly
    competition took place as part of the workshop Applied Verification for Continuous
    and Hybrid Systems (ARCH) in 2019. In this third edition, six tools have been
    applied to solve five different benchmark problems in the category for piecewise
    constant dynamics: BACH, Lyse, Hy- COMP, PHAVer/SX, PHAVerLite, and VeriSiMPL.
    Compared to last year, a new tool has participated (HyCOMP) and PHAVerLite has
    replaced PHAVer-lite. The result is a snap- shot of the current landscape of tools
    and the types of benchmarks they are particularly suited for. Due to the diversity
    of problems, we are not ranking tools, yet the presented results probably provide
    the most complete assessment of tools for the safety verification of continuous
    and hybrid systems with piecewise constant dynamics up to this date.'
acknowledgement: "The authors gratefully acknowledge \fnancial support by the European
  Commission project\r\nUnCoVerCPS under grant number 643921. Lei Bu is supported
  by the National Natural Science\r\nFoundation of China (No.61572249)."
alternative_title:
- EPiC Series in Computing
article_processing_charge: No
author:
- first_name: Goran
  full_name: Frehse, Goran
  last_name: Frehse
- first_name: Alessandro
  full_name: Abate, Alessandro
  last_name: Abate
- first_name: Dieky
  full_name: Adzkiya, Dieky
  last_name: Adzkiya
- first_name: Anna
  full_name: Becchi, Anna
  last_name: Becchi
- first_name: Lei
  full_name: Bu, Lei
  last_name: Bu
- first_name: Alessandro
  full_name: Cimatti, Alessandro
  last_name: Cimatti
- first_name: Mirco
  full_name: Giacobbe, Mirco
  id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
  last_name: Giacobbe
  orcid: 0000-0001-8180-0904
- first_name: Alberto
  full_name: Griggio, Alberto
  last_name: Griggio
- first_name: Sergio
  full_name: Mover, Sergio
  last_name: Mover
- first_name: Muhammad Syifa'ul
  full_name: Mufid, Muhammad Syifa'ul
  last_name: Mufid
- first_name: Idriss
  full_name: Riouak, Idriss
  last_name: Riouak
- first_name: Stefano
  full_name: Tonetta, Stefano
  last_name: Tonetta
- first_name: Enea
  full_name: Zaffanella, Enea
  last_name: Zaffanella
citation:
  ama: 'Frehse G, Abate A, Adzkiya D, et al. ARCH-COMP19 Category Report: Hybrid systems
    with piecewise constant dynamics. In: Frehse G, Althoff M, eds. <i>ARCH19. 6th
    International Workshop on Applied Verification of Continuous and Hybrid Systems</i>.
    Vol 61. EasyChair; 2019:1-13. doi:<a href="https://doi.org/10.29007/rjwn">10.29007/rjwn</a>'
  apa: 'Frehse, G., Abate, A., Adzkiya, D., Becchi, A., Bu, L., Cimatti, A., … Zaffanella,
    E. (2019). ARCH-COMP19 Category Report: Hybrid systems with piecewise constant
    dynamics. In G. Frehse &#38; M. Althoff (Eds.), <i>ARCH19. 6th International Workshop
    on Applied Verification of Continuous and Hybrid Systems</i> (Vol. 61, pp. 1–13).
    Montreal, Canada: EasyChair. <a href="https://doi.org/10.29007/rjwn">https://doi.org/10.29007/rjwn</a>'
  chicago: 'Frehse, Goran, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro
    Cimatti, Mirco Giacobbe, et al. “ARCH-COMP19 Category Report: Hybrid Systems with
    Piecewise Constant Dynamics.” In <i>ARCH19. 6th International Workshop on Applied
    Verification of Continuous and Hybrid Systems</i>, edited by Goran Frehse and
    Matthias Althoff, 61:1–13. EasyChair, 2019. <a href="https://doi.org/10.29007/rjwn">https://doi.org/10.29007/rjwn</a>.'
  ieee: 'G. Frehse <i>et al.</i>, “ARCH-COMP19 Category Report: Hybrid systems with
    piecewise constant dynamics,” in <i>ARCH19. 6th International Workshop on Applied
    Verification of Continuous and Hybrid Systems</i>, Montreal, Canada, 2019, vol.
    61, pp. 1–13.'
  ista: 'Frehse G, Abate A, Adzkiya D, Becchi A, Bu L, Cimatti A, Giacobbe M, Griggio
    A, Mover S, Mufid MS, Riouak I, Tonetta S, Zaffanella E. 2019. ARCH-COMP19 Category
    Report: Hybrid systems with piecewise constant dynamics. ARCH19. 6th International
    Workshop on Applied Verification of Continuous and Hybrid Systems. ARCH: International
    Workshop on Applied Verification on Continuous and Hybrid Systems, EPiC Series
    in Computing, vol. 61, 1–13.'
  mla: 'Frehse, Goran, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise
    Constant Dynamics.” <i>ARCH19. 6th International Workshop on Applied Verification
    of Continuous and Hybrid Systems</i>, edited by Goran Frehse and Matthias Althoff,
    vol. 61, EasyChair, 2019, pp. 1–13, doi:<a href="https://doi.org/10.29007/rjwn">10.29007/rjwn</a>.'
  short: G. Frehse, A. Abate, D. Adzkiya, A. Becchi, L. Bu, A. Cimatti, M. Giacobbe,
    A. Griggio, S. Mover, M.S. Mufid, I. Riouak, S. Tonetta, E. Zaffanella, in:, G.
    Frehse, M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification
    of Continuous and Hybrid Systems, EasyChair, 2019, pp. 1–13.
conference:
  end_date: 2019-04-15
  location: Montreal, Canada
  name: 'ARCH: International Workshop on Applied Verification on Continuous and Hybrid
    Systems'
  start_date: 2019-04-15
date_created: 2022-03-18T12:29:23Z
date_published: 2019-05-25T00:00:00Z
date_updated: 2022-05-17T07:09:47Z
day: '25'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.29007/rjwn
editor:
- first_name: Goran
  full_name: Frehse, Goran
  last_name: Frehse
- first_name: Matthias
  full_name: Althoff, Matthias
  last_name: Althoff
file:
- access_level: open_access
  checksum: 4b92e333db7b4e2349501a804dfede69
  content_type: application/pdf
  creator: dernst
  date_created: 2022-05-17T06:55:49Z
  date_updated: 2022-05-17T06:55:49Z
  file_id: '11391'
  file_name: 2019_EPiCs_Frehse.pdf
  file_size: 346415
  relation: main_file
  success: 1
file_date_updated: 2022-05-17T06:55:49Z
has_accepted_license: '1'
intvolume: '        61'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 1-13
publication: ARCH19. 6th International Workshop on Applied Verification of Continuous
  and Hybrid Systems
publication_identifier:
  issn:
  - 2398-7340
publication_status: published
publisher: EasyChair
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 61
year: '2019'
...
---
_id: '10883'
abstract:
- lang: eng
  text: 'Solving parity games, which are equivalent to modal μ-calculus model checking,
    is a central algorithmic problem in formal methods, with applications in reactive
    synthesis, program repair, verification of branching-time properties, etc. Besides
    the standard compu- tation model with the explicit representation of games, another
    important theoretical model of computation is that of set-based symbolic algorithms.
    Set-based symbolic algorithms use basic set operations and one-step predecessor
    operations on the implicit description of games, rather than the explicit representation.
    The significance of symbolic algorithms is that they provide scalable algorithms
    for large finite-state systems, as well as for infinite-state systems with finite
    quotient. Consider parity games on graphs with n vertices and parity conditions
    with d priorities. While there is a rich literature of explicit algorithms for
    parity games, the main results for set-based symbolic algorithms are as follows:
    (a) the basic algorithm that requires O(nd) symbolic operations and O(d) symbolic
    space; and (b) an improved algorithm that requires O(nd/3+1) symbolic operations
    and O(n) symbolic space. In this work, our contributions are as follows: (1) We
    present a black-box set-based symbolic algorithm based on the explicit progress
    measure algorithm. Two important consequences of our algorithm are as follows:
    (a) a set-based symbolic algorithm for parity games that requires quasi-polynomially
    many symbolic operations and O(n) symbolic space; and (b) any future improvement
    in progress measure based explicit algorithms immediately imply an efficiency
    improvement in our set-based symbolic algorithm for parity games. (2) We present
    a set-based symbolic algorithm that requires quasi-polynomially many symbolic
    operations and O(d · log n) symbolic space. Moreover, for the important special
    case of d ≤ log n, our algorithm requires only polynomially many symbolic operations
    and poly-logarithmic symbolic space.'
acknowledgement: 'A. S. is fully supported by the Vienna Science and Technology Fund
  (WWTF) through project ICT15-003. K.C. is supported by the Austrian Science Fund
  (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Starting grant (279307: Graph
  Games). For M.H the research leading to these results has received funding from
  the European Research Council under the European Union’s Seventh Framework Programme
  (FP/2007-2013) /ERC Grant Agreement no. 340506.'
alternative_title:
- EPiC Series in Computing
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Wolfgang
  full_name: Dvořák, Wolfgang
  last_name: Dvořák
- 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: Alexander
  full_name: Svozil, Alexander
  last_name: Svozil
citation:
  ama: 'Chatterjee K, Dvořák W, Henzinger MH, Svozil A. Quasipolynomial set-based
    symbolic algorithms for parity games. In: <i>22nd International Conference on
    Logic for Programming, Artificial Intelligence and Reasoning</i>. Vol 57. EasyChair;
    2018:233-253. doi:<a href="https://doi.org/10.29007/5z5k">10.29007/5z5k</a>'
  apa: 'Chatterjee, K., Dvořák, W., Henzinger, M. H., &#38; Svozil, A. (2018). Quasipolynomial
    set-based symbolic algorithms for parity games. In <i>22nd International Conference
    on Logic for Programming, Artificial Intelligence and Reasoning</i> (Vol. 57,
    pp. 233–253). Awassa, Ethiopia: EasyChair. <a href="https://doi.org/10.29007/5z5k">https://doi.org/10.29007/5z5k</a>'
  chicago: Chatterjee, Krishnendu, Wolfgang Dvořák, Monika H Henzinger, and Alexander
    Svozil. “Quasipolynomial Set-Based Symbolic Algorithms for Parity Games.” In <i>22nd
    International Conference on Logic for Programming, Artificial Intelligence and
    Reasoning</i>, 57:233–53. EasyChair, 2018. <a href="https://doi.org/10.29007/5z5k">https://doi.org/10.29007/5z5k</a>.
  ieee: K. Chatterjee, W. Dvořák, M. H. Henzinger, and A. Svozil, “Quasipolynomial
    set-based symbolic algorithms for parity games,” in <i>22nd International Conference
    on Logic for Programming, Artificial Intelligence and Reasoning</i>, Awassa, Ethiopia,
    2018, vol. 57, pp. 233–253.
  ista: 'Chatterjee K, Dvořák W, Henzinger MH, Svozil A. 2018. Quasipolynomial set-based
    symbolic algorithms for parity games. 22nd International Conference on Logic for
    Programming, Artificial Intelligence and Reasoning. LPAR: Conference on Logic
    for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing,
    vol. 57, 233–253.'
  mla: Chatterjee, Krishnendu, et al. “Quasipolynomial Set-Based Symbolic Algorithms
    for Parity Games.” <i>22nd International Conference on Logic for Programming,
    Artificial Intelligence and Reasoning</i>, vol. 57, EasyChair, 2018, pp. 233–53,
    doi:<a href="https://doi.org/10.29007/5z5k">10.29007/5z5k</a>.
  short: K. Chatterjee, W. Dvořák, M.H. Henzinger, A. Svozil, in:, 22nd International
    Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair,
    2018, pp. 233–253.
conference:
  end_date: 2018-11-21
  location: Awassa, Ethiopia
  name: 'LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning'
  start_date: 2018-11-17
date_created: 2022-03-18T12:46:32Z
date_published: 2018-10-23T00:00:00Z
date_updated: 2022-07-29T09:24:31Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.29007/5z5k
ec_funded: 1
external_id:
  arxiv:
  - '1909.04983'
file:
- access_level: open_access
  checksum: 1229aa8640bd6db610c85decf2265480
  content_type: application/pdf
  creator: dernst
  date_created: 2022-05-17T07:51:08Z
  date_updated: 2022-05-17T07:51:08Z
  file_id: '11392'
  file_name: 2018_EPiCs_Chatterjee.pdf
  file_size: 720893
  relation: main_file
  success: 1
file_date_updated: 2022-05-17T07:51:08Z
has_accepted_license: '1'
intvolume: '        57'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 233-253
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: 22nd International Conference on Logic for Programming, Artificial Intelligence
  and Reasoning
publication_identifier:
  issn:
  - 2398-7340
publication_status: published
publisher: EasyChair
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quasipolynomial set-based symbolic algorithms for parity games
type: conference
user_id: 72615eeb-f1f3-11ec-aa25-d4573ddc34fd
volume: 57
year: '2018'
...