| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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.
Cited literature [13 references]
https://hal.inria.fr/hal-01658422
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, December 7, 2017 - 3:49:05 PM
Last modification on : Friday, January 7, 2022 - 12:00:02 PM
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, December 7, 2017 - 3:49:05 PM
Last modification on : Friday, January 7, 2022 - 12:00:02 PM
File
446833_1_En_15_Chapter.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License