Using SMT for solving fragments of parameterised Boolean equation systems

R.P.J. Koolen, T.A.C. Willemse, H. Zantema

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

5 Citations (Scopus)
5 Downloads (Pure)

Abstract

Fixpoint logics such as parameterised Boolean equation systems (PBESs) provide a unifying framework in which a number of practical decision problems can be encoded. Efficient evaluation methods (solving methods in the terminology of PBESs) are needed to solve the encoded decision problems. We present a sound pseudo-decision procedure that uses SMT solvers for solving conjunctive and disjunctive PBESs. These are important fragments, allowing to encode typical verification problems and planning problems. Our experiments, conducted with a prototype implementation, show that the new solving procedure is complementary to existing techniques for solving PBESs.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015)
EditorsB. Finkbeiner, G. Pu, L. Zhang
PublisherSpringer
Pages14-30
ISBN (Print)978-3-319-24952-0
DOIs
Publication statusPublished - 2015
Event13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China - Shanghai, China
Duration: 12 Oct 201515 Oct 2015
http://atva2015.ios.ac.cn/

Publication series

NameLecture Notes in Computer Science
Volume9364
ISSN (Print)0302-9743

Conference

Conference13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China
Abbreviated titleATVA 2015
CountryChina
CityShanghai
Period12/10/1515/10/15
Internet address

Fingerprint Dive into the research topics of 'Using SMT for solving fragments of parameterised Boolean equation systems'. Together they form a unique fingerprint.

Cite this