A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL

10Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.
Get full text

Abstract

A new one-pass and tree-shaped tableau system for satisfiability checking has been recently proposed, where each branch can be explored independently from others and, furthermore, directly corresponds to a potential model of the formula. Despite its simplicity, it proved itself to be effective in practice. In this paper, we provide a SAT-based encoding of such a tableau system, based on the technique of bounded satisfiability checking. Starting with a single-node tableau, i.e., depth k of the tree-shaped tableau equal to zero, we proceed in an incremental fashion. At each iteration, the tableau rules are encoded in a Boolean formula, representing all branches of the tableau up to the current depth k. A typical downside of such bounded techniques is the effort needed to understand when to stop incrementing the bound, to guarantee the completeness of the procedure. In contrast, termination and completeness of the proposed algorithm is guaranteed without computing any upper bound to the length of candidate models, thanks to the Boolean encoding of the rule of the original tableau system. We conclude the paper by describing a tool that implements our procedure, and comparing its performance with other state-of-the-art solvers.

Cite

CITATION STYLE

APA

Geatti, L., Gigante, N., & Montanari, A. (2019). A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11714 LNAI, pp. 3–20). Springer. https://doi.org/10.1007/978-3-030-29026-9_1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free