(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

We investigate the simplification of parameterised Boolean equation systems (PBESs), a first-order fixpoint logic, by means of quantifier manipulation. Whereas the occurrence of quantifiers in a PBES can significantly increase the effort required to solve a PBES, i.e., compute its semantics, existing syntactic transformations have little to no support for quantifiers. We resolve this, by proposing a static analysis algorithm that identifies which quantifiers may be moved between equations such that their scope is reduced. This syntactic transformation can drastically reduce the effort required to solve a PBES. Additionally, we identify an improvement to the computation of guards, which can be used to strengthen our static analysis.

Original languageEnglish
Title of host publicationProceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022)
Pages64-80
Number of pages17
Publication statusPublished - 2022
Event4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2022 - Haifa, Israel
Duration: 11 Aug 2022 → …

Publication series

NameCEUR Workshop Proceedings
Volume3326
ISSN (Print)1613-0073

Conference

Conference4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2022
Country/TerritoryIsrael
CityHaifa
Period11/08/22 → …

Bibliographical note

Publisher Copyright:
© 2022 Copyright for this paper by its authors.

Fingerprint

Dive into the research topics of '(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems'. Together they form a unique fingerprint.

Cite this