全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...

Model Checking Constraint LTL over Trees

Full-Text   Cite this paper   Add to My Lib

Abstract:

Constraint automata are an adaptation of B\"uchi-automata that process data words where the data comes from some relational structure S. Every transition of such an automaton comes with constraints in terms of the relations of S. A transition can only be fired if the current and the next data values satisfy all constraints of this transition. These automata have been used in the setting where S is a linear order for deciding constraint LTL with constraints over S. In this paper, S is the infinitely branching infinite order tree T. We provide a PSPACE algorithm for emptiness of T-constraint automata. This result implies PSPACE-completeness of the satisfiability and the model checking problem for constraint LTL with constraints over T.

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133