Minimisation of ATL $$^*$$ ∗ Models
| Autor: | Serenella Cerrito, Amélie David |
|---|---|
| Přispěvatelé: | Informatique, Biologie Intégrative et Systèmes Complexes (IBISC), Université d'Évry-Val-d'Essonne (UEVE), Université Paris Descartes - Paris 5 (UPD5) |
| Rok vydání: | 2017 |
| Předmět: |
060201 languages & linguistics
Bisimulation Discrete mathematics Minimisation (psychology) [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] General method [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 06 humanities and the arts 02 engineering and technology Alternating-time Temporal Logic Gas meter prover Alternating-time temporal logic TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Model minimization Tableaux TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science 0602 languages and literature 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319669014 TABLEAUX 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017) 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017), Sep 2017, Brasilia, Brazil. 10501, pp.193--208, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66902-1_12〉 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017), Sep 2017, Brasilia, Brazil. pp.193--208, ⟨10.1007/978-3-319-66902-1_12⟩ |
| DOI: | 10.1007/978-3-319-66902-1_12 |
| Popis: | The aim of this work is to provide a general method to minimize the size (number of states) of a model \(\mathcal {M}\) of an \(\mathsf {ATL^*}\) formula. Our approach is founded on the notion of alternating bisimulation: given a model \(\mathcal {M}\), it is transformed in a stepwise manner into a new model \({\mathcal {M}}\)’ minimal with respect to bisimulation. The method has been implemented and will be integrated into the prover TATL, that constructively decides satifiability of an \(\mathsf {ATL^*}\) formula by building a tableau from which, when open, models of the input formula can be extracted. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|