Título: Symbolic Regression for Non-Deterministic Actions
Autores: Menezes, Maria Viviane de; Barros, Leliane Nunes de; Pereira, Silvio do Lago
Resumo: Model checking (MC) is a widely used approach for verifying if a formal model of a system satisfies a particular temporal logic formula. Symbolic model checking has been largely applied to solve non-deterministic planning problems, an area called planning as model checking. In this approach, the planning domain is the system to be verified and the planning goal is the formula that must be satisfied. In general, the planning domain is given by a set of action specifications given in terms of preconditions and effects formulas and the MC pre-image computation performs some kind of translation of the actions specification into a symbolic representation of the whole state-transition space. However, the symbolic representation of the entire state transition space is a very expensive operation and, in some cases, even using the symbolic representation it is impossible to come up with a plan for large problems. In order to overcome this limitation, one can compute the pre-image of X by using directly the action specification, without representing the whole state-transition space, an operation called symbolic regression. In this paper, we propose new symbolic non-deterministic regression operations based on Quantified Boolean Formulas (QBF) inference, as an extension of previous work on deterministic symbolic planning. In addition, we prove that the regression operations are equivalent to existing pre-image operations.
Palavras-chave: Model Checking; Automated Planning; Non-Deterministic Actions; Temporal Logic
Páginas: 17
Código DOI: 10.21528/lmln-vol12-no2-art3
Artigo em PDF: vol12-no2-art3.pdf
Arquivo BibTex: vol12-no2-art3.bib