TY - JOUR
T1 - Symbolic state space reduction with guarded terms for rewriting modulo SMT
AU - Bae, Kyungmin
AU - Rocha, Camilo
N1 - Publisher Copyright:
© 2019 Elsevier B.V.
PY - 2019/6/1
Y1 - 2019/6/1
N2 - Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a non-deterministic environment, by seamlessly combining rewriting modulo equational theories, SMT solving, and model checking. This paper presents guarded terms, an approach to deal with the symbolic state-space explosion problem for rewriting modulo SMT, one of the main challenges of this technique. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach.
AB - Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a non-deterministic environment, by seamlessly combining rewriting modulo equational theories, SMT solving, and model checking. This paper presents guarded terms, an approach to deal with the symbolic state-space explosion problem for rewriting modulo SMT, one of the main challenges of this technique. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach.
KW - CASH scheduling algorithm
KW - Rewriting logic
KW - Rewriting modulo SMT
KW - State space reduction
KW - Symbolic reachability analysis
UR - http://www.scopus.com/inward/record.url?scp=85063960210&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2019.03.006
DO - 10.1016/j.scico.2019.03.006
M3 - Article
AN - SCOPUS:85063960210
SN - 0167-6423
VL - 178
SP - 20
EP - 42
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -