Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints

Andreas Teucke 1, 2 Christoph Weidenbach 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01657026
Contributor : Stephan Merz <>
Submitted on : Wednesday, December 6, 2017 - 11:48:16 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM

File

authorcopy.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Andreas Teucke, Christoph Weidenbach. Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. CADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.202-219, ⟨10.1007/978-3-319-63046-5_13⟩. ⟨hal-01657026⟩

Share

Metrics

Record views

327

Files downloads

98