de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Superposition as a Decision Procedure for Timed Automata

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44415

Fietzke,  Arnaud Luc
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Fietzke, A. L., & Weidenbach, C. (2013). Superposition as a Decision Procedure for Timed Automata. Mathematics in Computer Science, 6(4), 409-425. doi:10.1007/s11786-012-0134-5.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B7C8-A
Abstract
The success of superposition-based theorem proving in first-order logic relies in particular on the fact that the superposition calculus can be turned into a decision procedure for various decidable fragments of first-order logic and has been successfully used to identify 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.