---
_id: '13292'
abstract:
- lang: eng
text: The operator precedence languages (OPLs) represent the largest known subclass
of the context-free languages which enjoys all desirable closure and decidability
properties. This includes the decidability of language inclusion, which is the
ultimate verification problem. Operator precedence grammars, automata, and logics
have been investigated and used, for example, to verify programs with arithmetic
expressions and exceptions (both of which are deterministic pushdown but lie outside
the scope of the visibly pushdown languages). In this paper, we complete the picture
and give, for the first time, an algebraic characterization of the class of OPLs
in the form of a syntactic congruence that has finitely many equivalence classes
exactly for the operator precedence languages. This is a generalization of the
celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of
the consequences, we show that universality and language inclusion for nondeterministic
operator precedence automata can be solved by an antichain algorithm. Antichain
algorithms avoid determinization and complementation through an explicit subset
construction, by leveraging a quasi-order on words, which allows the pruning of
the search space for counterexample words without sacrificing completeness. Antichain
algorithms can be implemented symbolically, and these implementations are today
the best-performing algorithms in practice for the inclusion of finite automata.
We give a generic construction of the quasi-order needed for antichain algorithms
from a finite syntactic congruence. This yields the first antichain algorithm
for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem
for OPLs in exponential time.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe
thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful
comments.\r\n"
alternative_title:
- LIPIcs
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Pavol
full_name: Kebis, Pavol
last_name: Kebis
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator
precedence languages. In: 50th International Colloquium on Automata, Languages,
and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129'
apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023).
Regular methods for operator precedence languages. In 50th International Colloquium
on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129'
chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International
Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129.
ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods
for operator precedence languages,” in 50th International Colloquium on Automata,
Languages, and Programming, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.
ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for
operator precedence languages. 50th International Colloquium on Automata, Languages,
and Programming. ICALP: Automata, Languages and Programming, LIPIcs, vol. 261,
129:1--129:20.'
mla: Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.”
50th International Colloquium on Automata, Languages, and Programming,
vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20,
doi:10.4230/LIPIcs.ICALP.2023.129.
short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International
Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023, p. 129:1--129:20.
conference:
end_date: 2023-07-14
location: Paderborn, Germany
name: 'ICALP: Automata, Languages and Programming'
start_date: 2023-07-10
corr_author: '1'
date_created: 2023-07-24T15:11:41Z
date_published: 2023-07-05T00:00:00Z
date_updated: 2025-07-10T11:50:41Z
day: '05'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.ICALP.2023.129
ec_funded: 1
external_id:
arxiv:
- '2305.03447'
file:
- access_level: open_access
checksum: 5d4c8932ef3450615a53b9bb15d92eb2
content_type: application/pdf
creator: esarac
date_created: 2023-07-24T15:11:05Z
date_updated: 2023-07-24T15:11:05Z
file_id: '13293'
file_name: icalp23.pdf
file_size: 859379
relation: main_file
success: 1
file_date_updated: 2023-07-24T15:11:05Z
has_accepted_license: '1'
intvolume: ' 261'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 129:1--129:20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 50th International Colloquium on Automata, Languages, and Programming
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959772785'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Regular methods for operator precedence languages
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: 261
year: '2023'
...