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.
Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau
GIGANTE, Nicola;MONTANARI, Angelo;
2016-01-01
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
ijcai2016.pdf
accesso aperto
Tipologia:
Documento in Pre-print
Licenza:
Creative commons
Dimensione
217.55 kB
Formato
Adobe PDF
|
217.55 kB | Adobe PDF | Visualizza/Apri |
|
139.pdf
accesso aperto
Tipologia:
Versione Editoriale (PDF)
Licenza:
Creative commons
Dimensione
592.09 kB
Formato
Adobe PDF
|
592.09 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
