Superposition as a Decision Procedure for Timed Automata (Extended Abstract)

摘要：

The success of superposition-based theorem proving in first-order logic relies in particular on the fact that the superposition calculus is able to decide well-known classical decidable fragments of first-order logic and has been successful in identifying new decidable classes. In this paper, we extend this story to the hierarchic combination of linear arithmetic and first-order superposition. We show that decidability of reachability in timed automata can be obtained by instantiation of an abstract termination result for SUP(LA), the hierarchic combination of linear arithmetic and first-order superposition.

作者: Arnaud Fietzke Christoph Weidenbach

作者单位: Max-Planck-Institut für Informatik, Saarbrücken, Germany Saarland University -Computer Science, Saarbrücken, Germany

会议类型: 国际会议

会议名称: The Fourth International Conference on Mathematical Aspects of Computer and Information Sciences(第四届计算机与信息科学中的数学方法国际会议 MACIS 2011)

会议地点: 北京

会议语种:英文

页码: 52-62

在线出版日期: 2011-10-21（万方平台首次上网日期，不代表论文的发表时间）