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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

5 Citaten (Scopus)

5 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Titel	Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015)
Redacteuren	B. Finkbeiner, G. Pu, L. Zhang
Uitgeverij	Springer
Pagina's	14-30
ISBN van geprinte versie	978-3-319-24952-0
DOI's	https://doi.org/10.1007/978-3-319-24953-7_3
Status	Gepubliceerd - 2015
Evenement	13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China - Shanghai, China Duur: 12 okt. 2015 → 15 okt. 2015 http://atva2015.ios.ac.cn/

Publicatie series

Naam	Lecture Notes in Computer Science
Volume	9364
ISSN van geprinte versie	0302-9743

Congres

Congres	13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), October 12–15, 2015, Shanghai, China
Verkorte titel	ATVA 2015
Land/Regio	China
Stad	Shanghai
Periode	12/10/15 → 15/10/15
Ander	13th International Symposium on Automated Technology for Verification and Analysis
Internet adres	http://atva2015.ios.ac.cn/

Toegang tot document

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

Citeer dit

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 (editors), Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015) (blz. 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 (uitgave), 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, blz. 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). uitgave / B. Finkbeiner; G. Pu; L. Zhang. Springer, 2015. blz. 14-30 (Lecture Notes in Computer Science; Vol. 9364).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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, redacteurs, Automated Technology for Verification and Analysis (13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015). Springer. 2015. blz. 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

Samenvatting

Publicatie series

Congres

Toegang tot document

Vingerafdruk

Citeer dit