Creating Büchi automata for multi-valued model checking

Stefan J.J. Vijzelaar*, Wan J. Fokkink

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publicationFormal 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
PublisherSpringer/Verlag
Pages210-224
Number of pages15
Volume10321 LNCS
ISBN (Print)9783319602240
DOIs
Publication statusPublished - 2017
Event37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017 - Neuchatel, Switzerland
Duration: 19 Jun 201722 Jun 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10321 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017
CountrySwitzerland
CityNeuchatel
Period19/06/1722/06/17

Fingerprint Dive into the research topics of 'Creating Büchi automata for multi-valued model checking'. Together they form a unique fingerprint.

Cite this