Safety alternating automata on data words

ACM Transactions on Computational Logic (TOCL)(2011)

引用 18|浏览38
暂无评分
摘要
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown to be ExpSpace-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained for satisfiability and refinement, respectively, for the safety fragment of linear temporal logic with freeze quantification. Dropping the safety restriction, adding past temporal operators, or adding one more register, each causes undecidability.
更多
查看译文
关键词
complexity bound,safety fragment,safety restriction,linear temporal logic,data word,past temporal operator,finite alphabet,causes undecidability,infinite data word,infinite set,satisfiability
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要