| Autor: |
Delmas, Rémi, Garion, Christophe, Giet, Josselin |
| Přispěvatelé: |
Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE), Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE), Ecole Normale Supérieure de Paris - ENS Paris (FRANCE), Département d'Ingénierie des Systèmes Complexes - DISC (Toulouse, France) |
| Jazyk: |
angličtina |
| Rok vydání: |
2018 |
| Předmět: |
|
| Popis: |
Cet article présente MOLOSS, un solveur pour la satisfiabilité en logique modale. MOLOSS implémente et étend le travail théorique d'Aceres et al. dans lequel les auteurs définissent une procédure de décision basée SMT pour les logiques modales. Cette procédure traduit classiquement une formule de la logique modale en une formule du premier ordre et instancie les quantificateurs de la formule résultante pour vérifier sa satifaisabilité en utilisant un solveur SAT. Notre implémantation permet de comparer la procédure d'Aceres et al. avec une autre dans laquelle les quantificateurs de la formule du premier ordre sont gérés directement par le solveur SMT utilisé. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
