# Creating Büchi Automata for Multi-valued Model Checking

Abstract : In explicit state model checking of linear temporal logic properties, a Büchi automaton encodes a temporal property. It interleaves with a Kripke model to form a state space, which is searched for counterexamples. Multi-valued model checking considers additional truth values beyond the Boolean $true$ and $false$; these values add extra information to the model, e.g. for the purpose of abstraction or execution steering. This paper presents a method to create Büchi automata for multi-valued model checking using quasi-Boolean logics. It allows for multi-valued propositions as well as multi-valued transitions. A logic for the purpose of execution steering and abstraction is presented as an application.
Type de document :
Communication dans un congrès
Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.210-224, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_15〉
Domaine :

Littérature citée [13 références]

https://hal.inria.fr/hal-01658422
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 décembre 2017 - 15:49:05
Dernière modification le : jeudi 7 décembre 2017 - 15:50:47

### Fichier

##### Accès restreint
Fichier visible le : 2020-01-01

Connectez-vous pour demander l'accès au fichier

### Citation

Stefan Vijzelaar, Wan Fokkink. Creating Büchi Automata for Multi-valued Model Checking. Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.210-224, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_15〉. 〈hal-01658422〉

### Métriques

Consultations de la notice