A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic
Authors: Rüdiger Ehlers and Martin Lange
Paper Information
| Title: | A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic |
| Authors: | Rüdiger Ehlers and Martin Lange |
| Proceedings: | IJCAR 2014 LNCS proceedings |
| Editors: | Stéphane Demri, Deepak Kapur and Christoph Weidenbach |
| Keywords: | temporal logic, decision procedures, SAT solver, tool support, bounded model checking |
| Abstract: | ABSTRACT. Interval Temporal Logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little tool support for automated ITL reasoning is available, possibly also owed to ITL's undecidability. We consider the bounded satisfiability which approximates finite satisfiability and is only NP-complete. We provide an encoding into SAT that makes use of the power of modern incremental SAT solvers and present a tool which tests an ITL specification for finite satisfiability. |
| Pages: | 7 |
| Talk: | Jul 21 15:00 |
| Paper: |  |