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
SN - 0167-6423
VL - 188
JO - Science of Computer Programming
JF - Science of Computer Programming
M1 - 102389
ER -