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.
Titolo: | Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau |
Autori: | |
Data di pubblicazione: | 2016 |
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. |
Handle: | http://hdl.handle.net/11390/1089563 |
ISBN: | 978-1-57735-770-4 978-1-57735-771-1 |
Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
ijcai2016.pdf | Documento in Pre-print | Non pubblico | Accesso ristretto Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.