Creating Büchi automata for multi-valued model checking

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

Model checking
Model Checking
Automata
Logic
Kripke Models
Linear Temporal Logic
Temporal logic
Proposition
Counterexample
State Space
Abstraction
Model

Cite this

Vijzelaar, S. J. J., & Fokkink, W. J. (2017). Creating Büchi automata for multi-valued model checking. In 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 (Vol. 10321 LNCS, pp. 210-224). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10321 LNCS). Springer/Verlag. https://doi.org/10.1007/978-3-319-60225-7_15
Vijzelaar, Stefan J.J. ; Fokkink, Wan J. / Creating Büchi automata for multi-valued model checking. 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. Vol. 10321 LNCS Springer/Verlag, 2017. pp. 210-224 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{b760e7a846c44be4a59b78b1dbd2fcb5,
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 = "Vijzelaar, {Stefan J.J.} and Fokkink, {Wan J.}",
year = "2017",
doi = "10.1007/978-3-319-60225-7_15",
language = "English",
isbn = "9783319602240",
volume = "10321 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer/Verlag",
pages = "210--224",
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",

}

Vijzelaar, SJJ & Fokkink, WJ 2017, Creating Büchi automata for multi-valued model checking. in 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. vol. 10321 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10321 LNCS, Springer/Verlag, pp. 210-224, 37th 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, 19/06/17. https://doi.org/10.1007/978-3-319-60225-7_15

Creating Büchi automata for multi-valued model checking. / Vijzelaar, Stefan J.J.; Fokkink, Wan J.

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. Vol. 10321 LNCS Springer/Verlag, 2017. p. 210-224 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10321 LNCS).

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

TY - GEN

T1 - Creating Büchi automata for multi-valued model checking

AU - Vijzelaar, Stefan J.J.

AU - Fokkink, Wan J.

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85020493118&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85020493118&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-60225-7_15

DO - 10.1007/978-3-319-60225-7_15

M3 - Conference contribution

SN - 9783319602240

VL - 10321 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 210

EP - 224

BT - 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

PB - Springer/Verlag

ER -

Vijzelaar SJJ, Fokkink WJ. Creating Büchi automata for multi-valued model checking. In 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. Vol. 10321 LNCS. Springer/Verlag. 2017. p. 210-224. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-60225-7_15