Abstract
We investigate the simplification of parameterised Boolean equation systems (PBESs), a firstorder 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 language  English 

Title of host publication  Proceedings of the 4th International Workshop on Automated Reasoning in Quantified NonClassical Logics (ARQNL 2022) 
Pages  6480 
Number of pages  17 
Publication status  Published  2022 
Event  4th International Workshop on Automated Reasoning in Quantified NonClassical Logics, ARQNL 2022  Haifa, Israel Duration: 11 Aug 2022 → … 
Publication series
Name  CEUR Workshop Proceedings 

Volume  3326 
ISSN (Print)  16130073 
Conference
Conference  4th International Workshop on Automated Reasoning in Quantified NonClassical Logics, ARQNL 2022 

Country/Territory  Israel 
City  Haifa 
Period  11/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.Datasets

Experiments for the paper "(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems"
Neele, T. (Creator), Zenodo, 4 Jul 2022
Dataset