### Abstract

We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show that a naive approach to constructing a control flow graph, needed for the analysis, may suffer from an exponential blow-up, and we define an approximate analysis that avoids this problem. The effectiveness of our techniques is evaluated using a number of case studies.

Original language | English |
---|---|

Title of host publication | Automated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014) |

Editors | F. Cassez, J.-F. Raskin |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 219-234 |

ISBN (Print) | 978-3-319-11935-9 |

DOIs | |

Publication status | Published - 2014 |

Event | conference; 12th International Symposium on Automated Technology for Verification and Analysis; 2014-11-03; 2014-11-06 - Duration: 3 Nov 2014 → 6 Nov 2014 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Volume | 8837 |

ISSN (Print) | 0302-9743 |

### Conference

Conference | conference; 12th International Symposium on Automated Technology for Verification and Analysis; 2014-11-03; 2014-11-06 |
---|---|

Period | 3/11/14 → 6/11/14 |

Other | 12th International Symposium on Automated Technology for Verification and Analysis |

## Fingerprint Dive into the research topics of 'Liveness analysis for parameterised Boolean equation systems'. Together they form a unique fingerprint.

## Cite this

Keiren, J. J. A., Wesselink, J. W., & Willemse, T. A. C. (2014). Liveness analysis for parameterised Boolean equation systems. In F. Cassez, & J-F. Raskin (Eds.),

*Automated Technology for Verification and Analysis (12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014)*(pp. 219-234). (Lecture Notes in Computer Science; Vol. 8837). Berlin: Springer. https://doi.org/10.1007/978-3-319-11936-6_16