@inproceedings{c165558127ce41ba816acac5152ad20e,
title = "Creating B{\"u}chi automata for multi-valued model checking",
abstract = "In explicit state model checking of linear temporal logic properties, a B{\"u}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{\"u}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.",
author = "S.J.J. Vijzelaar and W.J. Fokkink",
year = "2017",
doi = "10.1007/978-3-319-60225-7\_15",
language = "English",
isbn = "978-3-319-60224-0",
series = "Lecture Notes in Computer Science ",
publisher = "Springer",
pages = "210--224",
editor = "\{Bouajjani \}, \{A. \} and A. Silva",
booktitle = "Formal techniques for distributed objects, components, and systems - 37th IFIP WG 6.1 International Conference, FORTE 2017 Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Proceedings",
address = "Germany",
note = "37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2017) ; Conference date: 19-06-2017 Through 22-06-2017",
}