---
_id: '12302'
abstract:
- lang: eng
  text: 'We propose a novel algorithm to decide the language inclusion between (nondeterministic)
    Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage
    a notion of quasiorder to prune the search for a counterexample by discarding
    candidates which are subsumed by others for the quasiorder. Discarded candidates
    are guaranteed to not compromise the completeness of the algorithm. The novelty
    of our work lies in the quasiorder used to discard candidates. We introduce FORQs
    (family of right quasiorders) that we obtain by adapting the notion of family
    of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based
    inclusion algorithm which we prove correct and instantiate it for a specific FORQ,
    called the structural FORQ, induced by the Büchi automaton to the right of the
    inclusion sign. The resulting implementation, called FORKLIFT, scales up better
    than the state-of-the-art on a variety of benchmarks including benchmarks from
    program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870'
acknowledgement: This work was partially funded by the ESF Investing in your future,
  the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00
  BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Kyveli
  full_name: Doveri, Kyveli
  last_name: Doveri
- first_name: Pierre
  full_name: Ganty, Pierre
  last_name: Ganty
- first_name: Nicolas Adrien
  full_name: Mazzocchi, Nicolas Adrien
  id: b26baa86-3308-11ec-87b0-8990f34baa85
  last_name: Mazzocchi
citation:
  ama: 'Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing.
    In: <i>Computer Aided Verification</i>. Vol 13372. Springer Nature; 2022:109-129.
    doi:<a href="https://doi.org/10.1007/978-3-031-13188-2_6">10.1007/978-3-031-13188-2_6</a>'
  apa: 'Doveri, K., Ganty, P., &#38; Mazzocchi, N. A. (2022). FORQ-based language
    inclusion formal testing. In <i>Computer Aided Verification</i> (Vol. 13372, pp.
    109–129). Haifa, Israel: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-13188-2_6">https://doi.org/10.1007/978-3-031-13188-2_6</a>'
  chicago: Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based
    Language Inclusion Formal Testing.” In <i>Computer Aided Verification</i>, 13372:109–29.
    Springer Nature, 2022. <a href="https://doi.org/10.1007/978-3-031-13188-2_6">https://doi.org/10.1007/978-3-031-13188-2_6</a>.
  ieee: K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal
    testing,” in <i>Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13372,
    pp. 109–129.
  ista: 'Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal
    testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
    vol. 13372, 109–129.'
  mla: Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” <i>Computer
    Aided Verification</i>, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:<a
    href="https://doi.org/10.1007/978-3-031-13188-2_6">10.1007/978-3-031-13188-2_6</a>.
  short: K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer
    Nature, 2022, pp. 109–129.
conference:
  end_date: 2022-08-10
  location: Haifa, Israel
  name: 'CAV: Computer Aided Verification'
  start_date: 2022-08-07
date_created: 2023-01-16T10:06:31Z
date_published: 2022-08-06T00:00:00Z
date_updated: 2023-09-05T15:13:36Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-13188-2_6
ec_funded: 1
external_id:
  arxiv:
  - '2207.13549'
  isi:
  - '000870310500006'
file:
- access_level: open_access
  checksum: edc363b1be5447a09063e115c247918a
  content_type: application/pdf
  creator: dernst
  date_created: 2023-01-30T12:51:02Z
  date_updated: 2023-01-30T12:51:02Z
  file_id: '12465'
  file_name: 2022_LNCS_Doveri.pdf
  file_size: 497682
  relation: main_file
  success: 1
file_date_updated: 2023-01-30T12:51:02Z
has_accepted_license: '1'
intvolume: '     13372'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 109-129
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:
  - '9783031131882'
  eissn:
  - 1611-3349
  isbn:
  - '9783031131875'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: FORQ-based language inclusion formal testing
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: 13372
year: '2022'
...