Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance
LTL is frequently used to express specifications in many domains such as embedded systems or business processes. Witnesses can help to understand why an LTL specification is satisfiable, and a number of approaches exist to make understanding a witness easier. In the case of unsatisfiable specificati...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-06-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1306.2694v1 |
| _version_ | 1819138091350228992 |
|---|---|
| author | Viktor Schuppan |
| author_facet | Viktor Schuppan |
| author_sort | Viktor Schuppan |
| collection | DOAJ |
| description | LTL is frequently used to express specifications in many domains such as embedded systems or business processes. Witnesses can help to understand why an LTL specification is satisfiable, and a number of approaches exist to make understanding a witness easier. In the case of unsatisfiable specifications unsatisfiable cores (UCs), i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, are a well established means for debugging. However, little work has been done to help understanding a UC of an unsatisfiable LTL formula. In this paper we suggest to enhance a UC of an unsatisfiable LTL formula with additional information about the time points at which the subformulas of the UC are relevant for unsatisfiability. For example, in "(G p) and (X not p)" the first occurrence of "p" is really only "relevant" for unsatisfiability at time point 1 (time starts at time point 0). We present a method to extract such information from the resolution graph of a temporal resolution proof of unsatisfiability of an LTL formula. We implement our method in TRP++, and we experimentally evaluate it. Source code of our tool is available. |
| first_indexed | 2024-12-22T11:01:15Z |
| format | Article |
| id | doaj.art-3fe460d832b44aef8eba37f5ef649383 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-22T11:01:15Z |
| publishDate | 2013-06-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-3fe460d832b44aef8eba37f5ef6493832022-12-21T18:28:29ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-06-01117Proc. QAPL 2013496510.4204/EPTCS.117.4Enhancing Unsatisfiable Cores for LTL with Information on Temporal RelevanceViktor SchuppanLTL is frequently used to express specifications in many domains such as embedded systems or business processes. Witnesses can help to understand why an LTL specification is satisfiable, and a number of approaches exist to make understanding a witness easier. In the case of unsatisfiable specifications unsatisfiable cores (UCs), i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, are a well established means for debugging. However, little work has been done to help understanding a UC of an unsatisfiable LTL formula. In this paper we suggest to enhance a UC of an unsatisfiable LTL formula with additional information about the time points at which the subformulas of the UC are relevant for unsatisfiability. For example, in "(G p) and (X not p)" the first occurrence of "p" is really only "relevant" for unsatisfiability at time point 1 (time starts at time point 0). We present a method to extract such information from the resolution graph of a temporal resolution proof of unsatisfiability of an LTL formula. We implement our method in TRP++, and we experimentally evaluate it. Source code of our tool is available.http://arxiv.org/pdf/1306.2694v1 |
| spellingShingle | Viktor Schuppan Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance Electronic Proceedings in Theoretical Computer Science |
| title | Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance |
| title_full | Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance |
| title_fullStr | Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance |
| title_full_unstemmed | Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance |
| title_short | Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance |
| title_sort | enhancing unsatisfiable cores for ltl with information on temporal relevance |
| url | http://arxiv.org/pdf/1306.2694v1 |
| work_keys_str_mv | AT viktorschuppan enhancingunsatisfiablecoresforltlwithinformationontemporalrelevance |