%0 Conference Proceedings
%T Creating Büchi Automata for Multi-valued Model Checking
%+ Vrije Universiteit Amsterdam [Amsterdam] (VU)
%A Vijzelaar, Stefan
%A Fokkink, Wan, J.
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Neuchâtel, Switzerland
%Y Ahmed Bouajjani
%Y Alexandra Silva
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-10321
%P 210-224
%8 2017-06-19
%D 2017
%R 10.1007/978-3-319-60225-7_15
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01658422/document
%2 https://inria.hal.science/hal-01658422/file/446833_1_En_15_Chapter.pdf
%L hal-01658422
%U https://inria.hal.science/hal-01658422
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-10321