Using SMT for solving fragments of parameterised Boolean equation systems

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

doi:10.1007/978-3-319-24953-7_3

Using SMT for solving fragments of parameterised Boolean equation systems

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

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015)
Editors	B. Finkbeiner, G. Pu, L. Zhang
Publisher	Springer
Pages	14-30
ISBN (Print)	978-3-319-24952-0
DOIs	https://doi.org/10.1007/978-3-319-24953-7_3
Publication status	Published - 2015
Event	13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China - Shanghai, China Duration: 12 Oct 2015 → 15 Oct 2015 http://atva2015.ios.ac.cn/

Publication series

Name	Lecture Notes in Computer Science
Volume	9364
ISSN (Print)	0302-9743

Conference

Conference	13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China
Abbreviated title	ATVA 2015
Country/Territory	China
City	Shanghai
Period	12/10/15 → 15/10/15
Internet address	http://atva2015.ios.ac.cn/

Access to Document

10.1007/978-3-319-24953-7_3

Cite this

Koolen, R. P. J., Willemse, T. A. C., & Zantema, H. (2015). Using SMT for solving fragments of parameterised Boolean equation systems. In B. Finkbeiner, G. Pu, & L. Zhang (Eds.), Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015) (pp. 14-30). (Lecture Notes in Computer Science; Vol. 9364). Springer. https://doi.org/10.1007/978-3-319-24953-7_3

@inproceedings{e95d0585b1df48668bbdec9fabfb8799,

title = "Using SMT for solving fragments of parameterised Boolean equation systems",

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.",

author = "R.P.J. Koolen and T.A.C. Willemse and H. Zantema",

year = "2015",

doi = "10.1007/978-3-319-24953-7_3",

language = "English",

isbn = "978-3-319-24952-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "14--30",

editor = "B. Finkbeiner and G. Pu and L. Zhang",

booktitle = "Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015)",

address = "Germany",

note = "13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China, ATVA 2015 ; Conference date: 12-10-2015 Through 15-10-2015",

url = "http://atva2015.ios.ac.cn/",

}

Koolen, RPJ, Willemse, TAC & Zantema, H 2015, Using SMT for solving fragments of parameterised Boolean equation systems. in B Finkbeiner, G Pu & L Zhang (eds), Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015). Lecture Notes in Computer Science, vol. 9364, Springer, pp. 14-30, 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China, Shanghai, China, 12/10/15. https://doi.org/10.1007/978-3-319-24953-7_3

Using SMT for solving fragments of parameterised Boolean equation systems. / Koolen, R.P.J.; Willemse, T.A.C.; Zantema, H.
Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015). ed. / B. Finkbeiner; G. Pu; L. Zhang. Springer, 2015. p. 14-30 (Lecture Notes in Computer Science; Vol. 9364).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Using SMT for solving fragments of parameterised Boolean equation systems

AU - Koolen, R.P.J.

AU - Willemse, T.A.C.

AU - Zantema, H.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-24953-7_3

DO - 10.1007/978-3-319-24953-7_3

M3 - Conference contribution

SN - 978-3-319-24952-0

T3 - Lecture Notes in Computer Science

SP - 14

EP - 30

BT - Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015)

A2 - Finkbeiner, B.

A2 - Pu, G.

A2 - Zhang, L.

PB - Springer

T2 - 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China

Y2 - 12 October 2015 through 15 October 2015

ER -

Koolen RPJ, Willemse TAC , Zantema H. Using SMT for solving fragments of parameterised Boolean equation systems. In Finkbeiner B, Pu G, Zhang L, editors, Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015). Springer. 2015. p. 14-30. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-24953-7_3

Using SMT for solving fragments of parameterised Boolean equation systems

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this