TY - GEN
T1 - State space reduction for model checking agent programs
AU - Jongmans, Sung Shik T.Q.
AU - Hindriks, Koen V.
AU - Van Riemsdijk, M. Birna
PY - 2012/8/15
Y1 - 2012/8/15
N2 - State space reduction techniques have been developed to increase the efficiency of model checking in the context of imperative programming languages. Unfortunately, these techniques cannot straightforwardly be applied to agents: the nature of states in the two programming paradigms differs too much for this to be possible. To resolve this, we adapt core definitions on which existing reduction algorithms are based to agents. Moreover, the framework that we introduce is such that different reduction algorithms can be defined in terms of the same relations. This is beneficial because it enables the reuse of code and reduces computation time when different techniques are used simultaneously. Specifically, we adapt and combine two known techniques: property-based slicing and partial order reduction. We exemplify our work with the Goal agent programming language, and implement the theory that we present for Goal. Several experiments with this implementation show that performance is in line with known results from traditional model checking.
AB - State space reduction techniques have been developed to increase the efficiency of model checking in the context of imperative programming languages. Unfortunately, these techniques cannot straightforwardly be applied to agents: the nature of states in the two programming paradigms differs too much for this to be possible. To resolve this, we adapt core definitions on which existing reduction algorithms are based to agents. Moreover, the framework that we introduce is such that different reduction algorithms can be defined in terms of the same relations. This is beneficial because it enables the reuse of code and reduces computation time when different techniques are used simultaneously. Specifically, we adapt and combine two known techniques: property-based slicing and partial order reduction. We exemplify our work with the Goal agent programming language, and implement the theory that we present for Goal. Several experiments with this implementation show that performance is in line with known results from traditional model checking.
UR - http://www.scopus.com/inward/record.url?scp=84864851745&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84864851745&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-31915-0_8
DO - 10.1007/978-3-642-31915-0_8
M3 - Conference contribution
AN - SCOPUS:84864851745
SN - 9783642319143
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 133
EP - 154
BT - Programming Multi-Agent Systems - 9th International Workshop, ProMAS 2011, Revised Selected Papers
T2 - 9th International Workshop on ProgrammingMulti-Agent Systems, ProMAS 2011
Y2 - 3 May 2011 through 3 May 2011
ER -