Computing unsatisfiable cores for LTLf specifications
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2022
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910491488550912 |
|---|---|
| author | Roveri, Marco Di Ciccio, Claudio Di Francescomarino, Chiara Ghidini, Chiara |
| author_facet | Roveri, Marco Di Ciccio, Claudio Di Francescomarino, Chiara Ghidini, Chiara |
| contents | Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2203_04834 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Computing unsatisfiable cores for LTLf specifications Roveri, Marco Di Ciccio, Claudio Di Francescomarino, Chiara Ghidini, Chiara Logic in Computer Science Artificial Intelligence Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools. |
| title | Computing unsatisfiable cores for LTLf specifications |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2203.04834 |