Finding compact proofs for infinite-data parameterised Boolean equation systems

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional techniques to solve PBESs, such as instantiation techniques, cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. We also apply knowledge of intermediate solutions in an early termination heuristic. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Compared to similar procedures that operate on behavioural models, our technique is also more general: it is not restricted to model checking with finite action sets. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.

Original languageEnglish
Article number102389
Number of pages22
JournalScience of Computer Programming
Volume188
DOIs
Publication statusPublished - 1 Mar 2020

Fingerprint

Model checking

Keywords

  • Bisimulation
  • Infinite state system
  • Modal mu-calculus
  • Parameterised Boolean equation system
  • Symbolic model checking

Cite this

@article{9dabd5dd4409496797d0bc35377e1dac,
title = "Finding compact proofs for infinite-data parameterised Boolean equation systems",
abstract = "Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional techniques to solve PBESs, such as instantiation techniques, cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. We also apply knowledge of intermediate solutions in an early termination heuristic. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Compared to similar procedures that operate on behavioural models, our technique is also more general: it is not restricted to model checking with finite action sets. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.",
keywords = "Bisimulation, Infinite state system, Modal mu-calculus, Parameterised Boolean equation system, Symbolic model checking",
author = "Thomas Neele and Willemse, {Tim A.C.} and Groote, {Jan Friso}",
year = "2020",
month = "3",
day = "1",
doi = "10.1016/j.scico.2019.102389",
language = "English",
volume = "188",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",

}

TY - JOUR

T1 - Finding compact proofs for infinite-data parameterised Boolean equation systems

AU - Neele, Thomas

AU - Willemse, Tim A.C.

AU - Groote, Jan Friso

PY - 2020/3/1

Y1 - 2020/3/1

N2 - Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional techniques to solve PBESs, such as instantiation techniques, cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. We also apply knowledge of intermediate solutions in an early termination heuristic. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Compared to similar procedures that operate on behavioural models, our technique is also more general: it is not restricted to model checking with finite action sets. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.

AB - Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional techniques to solve PBESs, such as instantiation techniques, cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. We also apply knowledge of intermediate solutions in an early termination heuristic. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Compared to similar procedures that operate on behavioural models, our technique is also more general: it is not restricted to model checking with finite action sets. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.

KW - Bisimulation

KW - Infinite state system

KW - Modal mu-calculus

KW - Parameterised Boolean equation system

KW - Symbolic model checking

UR - http://www.scopus.com/inward/record.url?scp=85077720320&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2019.102389

DO - 10.1016/j.scico.2019.102389

M3 - Article

AN - SCOPUS:85077720320

VL - 188

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

M1 - 102389

ER -