On the complexity of the Bernays-Schönfinkel class with datalog
作者： Witold Charatonik , Piotr Witkowski
DOI: 10.1007/978-3-642-16242-8_14
关键词:
摘要: The Bernays-Schonfinkel class with Datalog is a 2-variable fragment of the extended least fixed points expressible by certain monadic programs. It was used in bounded model checking procedure for programs manipulating dynamically allocated pointer structures, where problem reduced to satisfiability formulas this logic. best known upper bound on complexity logic 2NEXPTIME. In paper we extend more expressive -- two-variable counting quantifiers same kind points. We prove that both and entailment new are decidable NEXPTIME give matching lower original logic, which establishes NEXPTIME-completeness problems them. Our algorithm based translation quantifiers.
springer.com
uni.wroc.pl 参考文章(36)
Gianluigi Zavattaro, Mario Bravetti, Concur 2009 - Concurrency Theory ,(2009)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Kshitij Bansal, Rémi Brochenin, Etienne Lozes, Beyond Shapes: Lists with Ordered Data joint european conferences on theory and practice of software. pp. 425- 439 ,(2009) , 10.1007/978-3-642-00596-1_30
Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, Greta Yorsh, None, The Boundary Between Decidability and Undecidability for Transitive-Closure Logics computer science logic. ,vol. 3210, pp. 160- 174 ,(2004) , 10.1007/978-3-540-30124-0_15
Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Mihaela Sighireanu, A Logic-Based Framework for Reasoning about Composite Data Structures international conference on concurrency theory. pp. 178- 195 ,(2009) , 10.1007/978-3-642-04081-8_13
Ittai Balaban, Amir Pnueli, Lenore D. Zuck, Shape Analysis of Single-Parent Heaps Lecture Notes in Computer Science. pp. 91- 105 ,(2007) , 10.1007/978-3-540-69738-1_7
Martin Fürer, The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems) Logic and Machines: Decision Problems and Complexity. pp. 312- 319 ,(1984) , 10.1007/3-540-13331-3_48
Niel Immerman, Alexander Rabinovich, Thomas W. Reps, Mooly Sagiv, Great Yorsh, Verification via Structure Simulation Computer Aided Verification. ,vol. 3114, pp. 281- 294 ,(2004) , 10.1007/978-3-540-27813-9_22
G. Yorsh, Thomas Reps, Mooly Sagiv, Symbolically Computing Most-Precise Abstract Operations for Shape Analysis tools and algorithms for construction and analysis of systems. pp. 530- 545 ,(2004) , 10.1007/978-3-540-24730-2_39
Erich Grädel, Martin Otto, Eric Rosen, Undecidability Results on Two-Variable Logics symposium on theoretical aspects of computer science. pp. 249- 260 ,(1997) , 10.1007/BFB0023464