---
title: "Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau"
authors:
  - "Matteo Bertello"
  - "Nicola Gigante"
  - "Angelo Montanari"
  - "Mark Reynolds"
doi: ""
url: "https://ijcai.org/proceedings/2016/139"
pdf: "https://ijcai.org/proceedings/2016/0139.pdf"
venue: "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence"
year: 2016
pages: "950-955"
track: ""
keywords:
---

# Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau

Matteo Bertello, Nicola Gigante, Angelo Montanari, Mark Reynolds

*Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence*, pages 950-955.

## Abstract

The paper presents Leviathan, an LTL satisfiability checking tool based on a novel one-pass, tree-like tableau system, which is way simpler than existing solutions. Despite the simplicity of the algorithm, the tool has performance comparable in speed and memory consumption with other tools on a number of standard benchmark sets, and, in various cases, it outperforms the other tableau-based tools.